Merge lp:~verifydtapn-contributers/verifydtapn/NoDefaultGCD into lp:verifydtapn

[Peter Gjøl Jensen]

Made GCD opt in.

[Jiri Srba (srba)]

review: Approve

=== modified file 'src/Core/ArgsParser.cpp'
--- src/Core/ArgsParser.cpp	2013-12-05 13:23:21 +0000
+++ src/Core/ArgsParser.cpp	2014-02-19 08:49:51 +0000
@@ -167,7 +167,7 @@
 
     parsers.push_back(
             boost::make_shared<Switch >("c", GCD,
-            "Disable lowering the guards by the greatest common divisor"));
+            "Enable lowering the guards by the greatest common divisor"));
     
     parsers.push_back(
             boost::make_shared<SwitchWithArg > ("w", WORKFLOW,
@@ -404,11 +404,11 @@
 
         
         assert(map.find(GCD) != map.end());
-        bool disableGCDLowerGuards = boost::lexical_cast<bool>(
+        bool enableGCDLowerGuards = boost::lexical_cast<bool>(
 			map.find(GCD)->second);
         
 	return VerificationOptions(modelFile, queryFile, search, verification, memoptimization, kbound, trace,
-			xml_trace, max_constant, keep_dead, disableGCDLowerGuards, workflow);
+			xml_trace, max_constant, keep_dead, enableGCDLowerGuards, workflow);
 
 }
 }
 
=== modified file 'src/Core/TAPN/TimedArcPetriNet.cpp'
--- src/Core/TAPN/TimedArcPetriNet.cpp	2013-12-05 13:23:21 +0000
+++ src/Core/TAPN/TimedArcPetriNet.cpp	2014-02-19 08:49:51 +0000
@@ -5,11 +5,11 @@
 
 namespace VerifyTAPN {
 	namespace TAPN {
-		void TimedArcPetriNet::initialize(bool useGlobalMaxConstant, bool disableLowerGuards)
+		void TimedArcPetriNet::initialize(bool useGlobalMaxConstant, bool lowerGuardsByGCD)
 		{
                     
                         // start by doing GCD if enabled
-                        if(!disableLowerGuards){
+                        if(lowerGuardsByGCD){
                                 GCDLowerGuards();
                         }
                     
 
=== modified file 'src/Core/VerificationOptions.hpp'
--- src/Core/VerificationOptions.hpp	2013-12-02 14:12:28 +0000
+++ src/Core/VerificationOptions.hpp	2014-02-19 08:49:51 +0000
@@ -44,7 +44,7 @@
                 bool xml_trace,
                 bool useGlobalMaxConstants,
                 bool keepDeadTokens, 
-                bool disableGCDLowerGuards,
+                bool enableGCDLowerGuards,
                 WorkflowMode workflow
                 ) : inputFile(inputFile),
         queryFile(queryFile),
@@ -56,7 +56,7 @@
         xml_trace(xml_trace),
         useGlobalMaxConstants(useGlobalMaxConstants),
         keepDeadTokens(keepDeadTokens), 
-        disableGCDLowerGuards(disableGCDLowerGuards),
+        enableGCDLowerGuards(enableGCDLowerGuards),
         workflow(workflow){
         };
 
@@ -102,8 +102,8 @@
             return keepDeadTokens;
         };
 
-        inline const bool getDisableGCDLowerGuards() const {
-            return disableGCDLowerGuards;
+        inline const bool getGCDLowerGuardsEnabled() const {
+            return enableGCDLowerGuards;
         }
 
         inline const WorkflowMode getWorkflowMode() const {
@@ -125,7 +125,7 @@
         bool xml_trace;
         bool useGlobalMaxConstants;
         bool keepDeadTokens;
-        bool disableGCDLowerGuards;
+        bool enableGCDLowerGuards;
         WorkflowMode workflow;
     };
 
 
=== modified file 'src/DiscreteVerification/DiscreteVerification.cpp'
--- src/DiscreteVerification/DiscreteVerification.cpp	2014-02-17 21:36:41 +0000
+++ src/DiscreteVerification/DiscreteVerification.cpp	2014-02-19 08:49:51 +0000
@@ -97,11 +97,11 @@
             AST::BoolResult containsDeadlock;
             DeadlockVisitor deadlockVisitor = DeadlockVisitor();
             deadlockVisitor.visit(*query, containsDeadlock);
-            if(containsDeadlock.value && options.getDisableGCDLowerGuards() == false){
+            if(containsDeadlock.value && options.getGCDLowerGuardsEnabled()){
                         cout << "Lowering constants by greatest common divisor is unsound for queries containing the deadlock proposition" << endl;
                         exit(1);
             }
-            if((query->getQuantifier() == EG || query->getQuantifier() == AF) && options.getDisableGCDLowerGuards() == false){
+            if((query->getQuantifier() == EG || query->getQuantifier() == AF) && options.getGCDLowerGuardsEnabled()){
                         cout << "Lowering constants by greatest common divisor is unsound for EG and AF queries" << endl;
                         exit(1);
             }
@@ -203,7 +203,7 @@
         template<typename T> void VerifyAndPrint(TAPN::TimedArcPetriNet& tapn, Verification<T>& verifier, VerificationOptions& options, AST::Query* query) {
             bool result = (!options.isWorkflow() && (query->getQuantifier() == AG || query->getQuantifier() == AF)) ? !verifier.verify() : verifier.verify();
 
-            if (!options.getDisableGCDLowerGuards()) {
+            if (options.getGCDLowerGuardsEnabled()) {
                 std::cout << "Lowering all guards by greatest common divisor: " << tapn.getGCD() << std::endl;
             }
             std::cout << std::endl;
 
=== modified file 'src/main.cpp'
--- src/main.cpp	2013-10-02 09:42:37 +0000
+++ src/main.cpp	2014-02-19 08:49:51 +0000
@@ -28,7 +28,7 @@
 		return 1;
 	}
 
-	tapn->initialize(options.getGlobalMaxConstantsEnabled(), options.getDisableGCDLowerGuards());
+	tapn->initialize(options.getGlobalMaxConstantsEnabled(), options.getGCDLowerGuardsEnabled());
 
 	std::vector<int> initialPlacement(modelParser.parseMarking(options.getInputFile(), *tapn));