Merge pull request #12 from TAPAAL/Print-bindings-for-unfolder

Print bindings for unfolder
TAPAAL · Dec 31, 2023 · 0fbaf63 · 0fbaf63
2 parents 752fa17 + ccf7d71
commit 0fbaf63
Show file tree

Hide file tree

Showing 3 changed files with 37 additions and 7 deletions.
diff --git a/README.md b/README.md
@@ -15,8 +15,8 @@ mkdir build && cd  build
 cmake ..
 
 #For mac, one need to enforce that we use the GCC compiler using:
-export CC=gcc-9
-export CXX=g++-9
+export CC=gcc-13
+export CXX=g++-13
 #and point to the correct version of flex and bison by adding
 #-DBISON_EXECUTABLE=/usr/local/opt/bison/bin/bison -DFLEX_EXECUTABLE=/usr/local/opt/flex/bin/flex
 #to cmake call

diff --git a/include/Colored/ColoredPetriNetBuilder.h b/include/Colored/ColoredPetriNetBuilder.h
@@ -10,6 +10,7 @@
 
 #include <vector>
 #include <unordered_map>
+#include <sstream>
 
 #include "ColoredNetStructures.h"
 #include "../TAPNBuilderInterface.h"
@@ -22,7 +23,7 @@ namespace unfoldtacpn {
         typedef std::unordered_map<std::string, std::vector<std::string>> PTTransitionMap;
 
     public:
-        ColoredPetriNetBuilder();
+        ColoredPetriNetBuilder(std::stringstream *output_stream = nullptr);
         ColoredPetriNetBuilder(const ColoredPetriNetBuilder& orig);
         virtual ~ColoredPetriNetBuilder();
         void parseNet(std::istream& istream);
@@ -82,6 +83,7 @@ namespace unfoldtacpn {
             return _pttransitionnames;
         }
 
+
         void unfold(TAPNBuilderInterface& builder);
         void clear() { _sumPlacesNames.clear(); _pttransitionnames.clear(); _ptplacenames.clear(); }
     private:
@@ -99,6 +101,8 @@ namespace unfoldtacpn {
         ColorTypeMap _colors;
         double _time;
 
+        std::stringstream* _output_stream;
+
         std::string arcToString(const Colored::Arc& arc) const;
         const std::string& findSumName(const std::string& id) const;
         const std::string& findSumName(uint32_t id) const { return findSumName(_places[id].name); }

diff --git a/src/Colored/ColoredPetriNetBuilder.cpp b/src/Colored/ColoredPetriNetBuilder.cpp
@@ -7,13 +7,17 @@
 
 #include <chrono>
 #include <tuple>
+#include <sstream>
 
 #include "Colored/ColoredPetriNetBuilder.h"
 #include "PetriParse/PNMLParser.h"
 #include "errorcodes.h"
 
 namespace unfoldtacpn {
-    ColoredPetriNetBuilder::ColoredPetriNetBuilder() {
+    ColoredPetriNetBuilder::ColoredPetriNetBuilder(std::stringstream *output_stream):
+    _output_stream(output_stream)
+    {
+
     }
 
     ColoredPetriNetBuilder::ColoredPetriNetBuilder(const ColoredPetriNetBuilder& orig)
@@ -193,10 +197,19 @@ namespace unfoldtacpn {
             unfoldPlace(builder, place);
         }
 
+        if (_output_stream) {
+            (*_output_stream) << "\nBINDINGS FOR EACH UNFOLDED TRANSITION\n";
+            (*_output_stream) << "<bindings>\n";
+        }
+
         for (auto& transition : _transitions) {
             unfoldTransition(builder, transition);
         }
 
+        if (_output_stream) {
+            (*_output_stream) << "</bindings>\n";
+        }
+
         auto end = std::chrono::high_resolution_clock::now();
         _time = (std::chrono::duration_cast<std::chrono::microseconds>(end - start).count())*0.000001;
     }
@@ -285,9 +298,22 @@ namespace unfoldtacpn {
         auto transitionPos = _transitionlocations[transitionId];
         size_t i = 0;
         for (auto& b : gen) {
+
             std::string name = transition.name;
-            if(!gen.isInitial())
-                name += "__" + std::to_string(i++);
+            //if(!gen.isInitial())
+            name += "__" + std::to_string(i++);
+
+            // Print bindings for each transition if output stream exists
+            if (_output_stream) {     
+                (*_output_stream) << "   <transition id=\"" << name << "\">\n";    
+                for(auto const &var: b) {
+                    (*_output_stream) << "      <variable id=\"" << var.first << "\">\n";
+                    (*_output_stream) << "         <color>" << var.second->getColorName() << "</color>\n";
+                    (*_output_stream) << "      </variable>\n";
+                }
+                (*_output_stream) << "   </transition>\n";
+            }
+
             builder.addTransition(name, transition.player, transition.urgent, std::get<0>(transitionPos), std::get<1>(transitionPos) + offset);
             _pttransitionnames[transition.name].push_back(name);
             for (auto& arc : transition.arcs) {
@@ -464,7 +490,7 @@ namespace unfoldtacpn {
         return !arc.input ? "(" + _transitions[arc.transition].name + ", " + _places[arc.place].name + ")" :
                "(" + _places[arc.place].name + ", " + _transitions[arc.transition].name + ")";
     }
-
+  
     BindingGenerator::Iterator::Iterator(BindingGenerator* generator)
             : _generator(generator)
     {