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

Proposed by Peter Gjøl Jensen
Status: Merged
Approved by: Jiri Srba
Approved revision: 296
Merged at revision: 296
Proposed branch: lp:~verifydtapn-contributers/verifydtapn/NoDefaultGCD
Merge into: lp:verifydtapn
Diff against target: 125 lines (+14/-14)
5 files modified
src/Core/ArgsParser.cpp (+3/-3)
src/Core/TAPN/TimedArcPetriNet.cpp (+2/-2)
src/Core/VerificationOptions.hpp (+5/-5)
src/DiscreteVerification/DiscreteVerification.cpp (+3/-3)
src/main.cpp (+1/-1)
To merge this branch: bzr merge lp:~verifydtapn-contributers/verifydtapn/NoDefaultGCD
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Mathias Grund Sørensen Pending
Jakob Taankvist Pending
Review via email: mp+207112@code.launchpad.net

Description of the change

Made GCD opt in.

To post a comment you must log in.
Revision history for this message
Jiri Srba (srba) :
review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'src/Core/ArgsParser.cpp'
2--- src/Core/ArgsParser.cpp 2013-12-05 13:23:21 +0000
3+++ src/Core/ArgsParser.cpp 2014-02-19 08:49:51 +0000
4@@ -167,7 +167,7 @@
5
6 parsers.push_back(
7 boost::make_shared<Switch >("c", GCD,
8- "Disable lowering the guards by the greatest common divisor"));
9+ "Enable lowering the guards by the greatest common divisor"));
10
11 parsers.push_back(
12 boost::make_shared<SwitchWithArg > ("w", WORKFLOW,
13@@ -404,11 +404,11 @@
14
15
16 assert(map.find(GCD) != map.end());
17- bool disableGCDLowerGuards = boost::lexical_cast<bool>(
18+ bool enableGCDLowerGuards = boost::lexical_cast<bool>(
19 map.find(GCD)->second);
20
21 return VerificationOptions(modelFile, queryFile, search, verification, memoptimization, kbound, trace,
22- xml_trace, max_constant, keep_dead, disableGCDLowerGuards, workflow);
23+ xml_trace, max_constant, keep_dead, enableGCDLowerGuards, workflow);
24
25 }
26 }
27
28=== modified file 'src/Core/TAPN/TimedArcPetriNet.cpp'
29--- src/Core/TAPN/TimedArcPetriNet.cpp 2013-12-05 13:23:21 +0000
30+++ src/Core/TAPN/TimedArcPetriNet.cpp 2014-02-19 08:49:51 +0000
31@@ -5,11 +5,11 @@
32
33 namespace VerifyTAPN {
34 namespace TAPN {
35- void TimedArcPetriNet::initialize(bool useGlobalMaxConstant, bool disableLowerGuards)
36+ void TimedArcPetriNet::initialize(bool useGlobalMaxConstant, bool lowerGuardsByGCD)
37 {
38
39 // start by doing GCD if enabled
40- if(!disableLowerGuards){
41+ if(lowerGuardsByGCD){
42 GCDLowerGuards();
43 }
44
45
46=== modified file 'src/Core/VerificationOptions.hpp'
47--- src/Core/VerificationOptions.hpp 2013-12-02 14:12:28 +0000
48+++ src/Core/VerificationOptions.hpp 2014-02-19 08:49:51 +0000
49@@ -44,7 +44,7 @@
50 bool xml_trace,
51 bool useGlobalMaxConstants,
52 bool keepDeadTokens,
53- bool disableGCDLowerGuards,
54+ bool enableGCDLowerGuards,
55 WorkflowMode workflow
56 ) : inputFile(inputFile),
57 queryFile(queryFile),
58@@ -56,7 +56,7 @@
59 xml_trace(xml_trace),
60 useGlobalMaxConstants(useGlobalMaxConstants),
61 keepDeadTokens(keepDeadTokens),
62- disableGCDLowerGuards(disableGCDLowerGuards),
63+ enableGCDLowerGuards(enableGCDLowerGuards),
64 workflow(workflow){
65 };
66
67@@ -102,8 +102,8 @@
68 return keepDeadTokens;
69 };
70
71- inline const bool getDisableGCDLowerGuards() const {
72- return disableGCDLowerGuards;
73+ inline const bool getGCDLowerGuardsEnabled() const {
74+ return enableGCDLowerGuards;
75 }
76
77 inline const WorkflowMode getWorkflowMode() const {
78@@ -125,7 +125,7 @@
79 bool xml_trace;
80 bool useGlobalMaxConstants;
81 bool keepDeadTokens;
82- bool disableGCDLowerGuards;
83+ bool enableGCDLowerGuards;
84 WorkflowMode workflow;
85 };
86
87
88=== modified file 'src/DiscreteVerification/DiscreteVerification.cpp'
89--- src/DiscreteVerification/DiscreteVerification.cpp 2014-02-17 21:36:41 +0000
90+++ src/DiscreteVerification/DiscreteVerification.cpp 2014-02-19 08:49:51 +0000
91@@ -97,11 +97,11 @@
92 AST::BoolResult containsDeadlock;
93 DeadlockVisitor deadlockVisitor = DeadlockVisitor();
94 deadlockVisitor.visit(*query, containsDeadlock);
95- if(containsDeadlock.value && options.getDisableGCDLowerGuards() == false){
96+ if(containsDeadlock.value && options.getGCDLowerGuardsEnabled()){
97 cout << "Lowering constants by greatest common divisor is unsound for queries containing the deadlock proposition" << endl;
98 exit(1);
99 }
100- if((query->getQuantifier() == EG || query->getQuantifier() == AF) && options.getDisableGCDLowerGuards() == false){
101+ if((query->getQuantifier() == EG || query->getQuantifier() == AF) && options.getGCDLowerGuardsEnabled()){
102 cout << "Lowering constants by greatest common divisor is unsound for EG and AF queries" << endl;
103 exit(1);
104 }
105@@ -203,7 +203,7 @@
106 template<typename T> void VerifyAndPrint(TAPN::TimedArcPetriNet& tapn, Verification<T>& verifier, VerificationOptions& options, AST::Query* query) {
107 bool result = (!options.isWorkflow() && (query->getQuantifier() == AG || query->getQuantifier() == AF)) ? !verifier.verify() : verifier.verify();
108
109- if (!options.getDisableGCDLowerGuards()) {
110+ if (options.getGCDLowerGuardsEnabled()) {
111 std::cout << "Lowering all guards by greatest common divisor: " << tapn.getGCD() << std::endl;
112 }
113 std::cout << std::endl;
114
115=== modified file 'src/main.cpp'
116--- src/main.cpp 2013-10-02 09:42:37 +0000
117+++ src/main.cpp 2014-02-19 08:49:51 +0000
118@@ -28,7 +28,7 @@
119 return 1;
120 }
121
122- tapn->initialize(options.getGlobalMaxConstantsEnabled(), options.getDisableGCDLowerGuards());
123+ tapn->initialize(options.getGlobalMaxConstantsEnabled(), options.getGCDLowerGuardsEnabled());
124
125 std::vector<int> initialPlacement(modelParser.parseMarking(options.getInputFile(), *tapn));
126

Subscribers

People subscribed via source and target branches