Merge pull request #29 from TAPAAL/print-bindings

added the switch -b for printing bindings

CMakeLists.txt

@@ -102,7 +102,7 @@ if (VERIFYTAPN_GetDependencies)
 
     ExternalProject_add(unfoldtacpn-ext
         GIT_REPOSITORY https://github.com/TAPAAL/unfoldTACPN
-        GIT_TAG 7f49fa4544c5a55acd965210e2bd6f702584b969
+        GIT_TAG 0fbaf6371eab965534a693e2dbde23437bff1269
 	    CMAKE_ARGS -DCMAKE_TOOLCHAIN_FILE=${CMAKE_TOOLCHAIN_FILE} -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER}  -DCMAKE_INSTALL_PREFIX=${EXTERNAL_INSTALL_LOCATION} -DBUILD_TESTING=OFF -DCMAKE_BUILD_TYPE=Release -DFLEX_EXECUTABLE=${FLEX_EXECUTABLE} -DBISON_EXECUTABLE=${BISON_EXECUTABLE}
     )
 

src/Core/VerificationOptions.cpp

@@ -83,6 +83,7 @@ namespace VerifyTAPN {
             "Specify the desired trace option.\n"
             " 0: none (default)\n"
             " 1: some")
+             ("bindings,b", "Print bindings to stderr in XML format (only for CPNs, default is not to print)")
             ("global-max-constants", "Use global maximum constant for extrapolation (as opposed to local constants).")
             ("disable-untimed-opt", "Disables the untimed place optimization.")
             ("disable-symmetry", "Disables symmetry reduction.")
@@ -184,6 +185,9 @@ namespace VerifyTAPN {
             if (vm.count("trace"))
                 opts.trace = vm["trace"].as<uint32_t>() == 0 ? NONE : SOME;
 
+             if (vm.count("bindings"))
+                opts.printBindings = true;    
+
             if (vm.count("global-max-constants"))
                 opts.useGlobalMaxConstants = true;
 

src/Core/VerificationOptions.hpp

@@ -23,6 +23,7 @@ namespace VerifyTAPN {
             bool symmetry,
             Trace trace,
             bool xml_trace,
+            bool printBindings,
             bool useUntimedPlaces,
             bool useGlobalMaxConstants,
             Factory factory,
@@ -36,6 +37,7 @@ namespace VerifyTAPN {
             k_bound(k_bound),
             symmetry(symmetry),
             trace(trace),
+            printBindings(printBindings),
             useUntimedPlaces(useUntimedPlaces),
             useGlobalMaxConstants(useGlobalMaxConstants),
             factory(factory),
@@ -50,6 +52,7 @@ namespace VerifyTAPN {
 			const std::string QueryFile() const {return queryFile; }
 			inline const unsigned int GetKBound() const { return k_bound; }
 			inline const Trace GetTrace() const { return trace; };
+            inline const bool GetPrintBindings() const {return printBindings; };
 			inline const bool GetSymmetryEnabled() const { return symmetry; }
 			inline const bool GetUntimedPlacesEnabled() const { return useUntimedPlaces; }
 			inline const bool GetGlobalMaxConstantsEnabled() const { return useGlobalMaxConstants; }
@@ -79,6 +82,7 @@ namespace VerifyTAPN {
 			unsigned int k_bound = 0;
 			bool symmetry = true;
 			Trace trace = NONE;
+            bool printBindings = false;
 			bool useUntimedPlaces = true;
 			bool useGlobalMaxConstants = false;
 			Factory factory = DEFAULT;

src/main.cpp

@@ -115,7 +115,9 @@ int main(int argc, char* argv[])
 
 	VerificationOptions options = VerificationOptions::parse(argc, argv);
 
-    unfoldtacpn::ColoredPetriNetBuilder builder;
+ 	std::unique_ptr<std::stringstream> output_stream = std::make_unique<std::stringstream>();
+    unfoldtacpn::ColoredPetriNetBuilder builder(options.GetPrintBindings() ? output_stream.get() : nullptr);
+
     auto [initialVector, tapn] = parse_net_file(builder, options.GetInputFile());
 
     if(tapn != nullptr)
@@ -223,6 +225,10 @@ int main(int argc, char* argv[])
 		return 1;
 	}
 
+	if (options.GetPrintBindings()) {
+        std::cout << output_stream.get()->str();
+    }
+
 	return 0;
 }