VerifyDTAPN

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

  1. WorkflowOptions
  2. Merge into trunk
Proposed by Peter Gjøl Jensen
Status: Merged
Approved by: Jiri Srba
Approved revision: 308
Merged at revision: 301
Proposed branch: lp:~verifydtapn-contributers/verifydtapn/WorkflowOptions
Merge into: lp:verifydtapn
Diff against target: 1063 lines (+329/-194)
21 files modified
src/Core/ArgsParser.cpp (+58/-28)
src/Core/ArgsParser.hpp (+2/-1)
src/Core/VerificationOptions.cpp (+15/-1)
src/Core/VerificationOptions.hpp (+26/-9)
src/DiscreteVerification/DataStructures/NonStrictMarking.hpp (+24/-0)
src/DiscreteVerification/DiscreteVerification.cpp (+1/-1)
src/DiscreteVerification/SearchStrategies/SearchFactory.h (+9/-1)
src/DiscreteVerification/SuccessorGenerator.hpp (+4/-4)
src/DiscreteVerification/VerificationTypes/AbstractNaiveVerification.hpp (+18/-18)
src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp (+4/-4)
src/DiscreteVerification/VerificationTypes/LivenessSearch.hpp (+1/-1)
src/DiscreteVerification/VerificationTypes/ReachabilitySearch.cpp (+4/-4)
src/DiscreteVerification/VerificationTypes/ReachabilitySearch.hpp (+1/-1)
src/DiscreteVerification/VerificationTypes/Verification.hpp (+9/-9)
src/DiscreteVerification/VerificationTypes/Workflow.cpp (+0/-23)
src/DiscreteVerification/VerificationTypes/Workflow.hpp (+13/-2)
src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp (+11/-10)
src/DiscreteVerification/VerificationTypes/WorkflowSoundness.hpp (+4/-4)
src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.cpp (+79/-57)
src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.hpp (+8/-8)
src/main.cpp (+38/-8)
To merge this branch: bzr merge lp:~verifydtapn-contributers/verifydtapn/WorkflowOptions
Reviewer Review Type Date Requested Status
Mathias Grund Sørensen code Approve
Jakob Taankvist Approve
Jiri Srba Approve
Review via email: mp+221718@code.launchpad.net

Commit message

- Refactoring and improvements to the workflow-part.
 - Removed the need for net-alterations for workflow-analysis.
 - Added error when choosing GCD and workflow

Description of the change

 - Refactoring and improvements to the workflow-part.
 - Removed the need for net-alterations for workflow-analysis.
 - Added error when choosing GCD and workflow

To post a comment you must log in.
Revision history for this message
Jakob Taankvist (jakob-taankvist) wrote :

I have skimmed over the code, and i didn't find anything strange.

The only thing is the addition of the default option for the search strategy. Isn't this redundant to just not specifying the option? Why is this needed?

review: Needs Information
Revision history for this message
Peter Gjøl Jensen (peter-gjoel) wrote :

See inline.

lp:~verifydtapn-contributers/verifydtapn/WorkflowOptions updated
306. By Peter Gjøl Jensen

fixed delay forever trace issue for workflow

307. By Peter Gjøl Jensen

removed possibly redundant code

Revision history for this message
Jiri Srba (srba) wrote :

Finally works on all my workflows.

review: Approve
Revision history for this message
Jakob Taankvist (jakob-taankvist) :
review: Approve
Revision history for this message
Mathias Grund Sørensen (mathias.grund) wrote :

Around line 4385 you say some code MIGHT be redundant and have code in comments. Could you confirm if this code is redundant? Anyway, I would prefer not to have a comment like that or commented code in trunk :-)

review: Needs Information (code)
Revision history for this message
Jiri Srba (srba) wrote :

Yes, the code is not needed. We discussed this before with Peter and I also tested thoroughly
and the control will never get here, so it is a dead-code. I agree, Peter, please, remove it
before we do the merge.

lp:~verifydtapn-contributers/verifydtapn/WorkflowOptions updated
308. By Jiri Srba

removed commented dead code at
src/DiscreteVerification/VerificationTypes/Verification.hpp

Revision history for this message
Mathias Grund Sørensen (mathias.grund) wrote :

Last commit changed some generated stuff as well, but I assume this is fine...

review: Approve (code)

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 2014-02-19 08:42:21 +0000
3+++ src/Core/ArgsParser.cpp 2014-06-11 15:19:00 +0000
4@@ -19,6 +19,7 @@
5 static const std::string LEGACY = "legacy";
6 static const std::string KEEP_DEAD = "keep-dead-tokens";
7 static const std::string WORKFLOW = "workflow";
8+static const std::string STRONG_WORKFLOW_BOUND = "strong-workflow-bound";
9
10 std::ostream& operator<<(std::ostream& out, const Switch& flag) {
11 flag.print(out);
12@@ -137,8 +138,8 @@
13 "Max tokens to use during exploration.", 0));
14 parsers.push_back(
15 boost::make_shared<SwitchWithArg > ("o", SEARCH_OPTION,
16- "Specify the desired search strategy.\n - 0: Breadth-First Search\n - 1: Depth-First Search\n - 2: Random Search\n - 3: Heuristic Search",
17- 3));
18+ "Specify the desired search strategy.\n - 0: Breadth-First Search\n - 1: Depth-First Search\n - 2: Random Search\n - 3: Heuristic Search\n - 4: Default",
19+ 4));
20 parsers.push_back(
21 boost::make_shared<SwitchWithArg > ("m", VERIFICATION_OPTION,
22 "Specify the desired verification method.\n - 0: Default (discrete)\n - 1: Time Darts",
23@@ -173,6 +174,10 @@
24 boost::make_shared<SwitchWithArg > ("w", WORKFLOW,
25 "Workflow mode.\n - 0: Disabled\n - 1: Soundness (and min)\n - 2: Strong Soundness (and max)",
26 0));
27+ parsers.push_back(
28+ boost::make_shared<SwitchWithArg > ("b", STRONG_WORKFLOW_BOUND,
29+ "Maximum delay bound for strong workflow analysis",
30+ 0));
31
32 };
33
34@@ -215,32 +220,14 @@
35 exit(1);
36 }
37
38- std::string model_file(argv[argc - 2]);
39- std::string query_file(argv[argc - 1]);
40-
41- if (boost::iends_with(query_file, ".xml")) {
42- std::cout << "Missing query file." << std::endl;
43- exit(1);
44- }
45-
46- if (!boost::iends_with(model_file, ".xml")) {
47- std::cout << "Invalid model file specified." << std::endl;
48- exit(1);
49- }
50-
51- if (!boost::iends_with(query_file, ".q")) {
52- std::cout << "Invalid query file specified." << std::endl;
53- exit(1);
54- }
55-
56 std::vector<std::string> flags;
57 unsigned int i = 1;
58 unsigned int size = static_cast<unsigned int>(argc);
59- while (i < size - 2) {
60+ while (i < size) {
61 std::string arg(argv[i]);
62 if (boost::istarts_with(arg, "-")) {
63 std::string arg2(argv[i + 1]);
64- if (!boost::istarts_with(arg2, "-") && i + 1 < size - 2) {
65+ if (!boost::istarts_with(arg2, "-") && i + 1 < size) {
66 flags.push_back(arg + " " + arg2);
67 i++;
68 } else {
69@@ -277,7 +264,47 @@
70 }
71 }
72
73- return createVerificationOptions(options, model_file, query_file);
74+ std::string model_file(argv[argc - 2]);
75+ std::string query_file(argv[argc - 1]);
76+
77+ return verifyInputFiles(createVerificationOptions(options), model_file, query_file);
78+}
79+
80+VerificationOptions ArgsParser::verifyInputFiles(VerificationOptions options, std::string model_file, std::string query_file) const {
81+ if(options.getWorkflowMode() != VerificationOptions::WORKFLOW_SOUNDNESS &&
82+ options.getWorkflowMode() != VerificationOptions::WORKFLOW_STRONG_SOUNDNESS) {
83+ if (boost::iends_with(query_file, ".xml")) {
84+ std::cout << "Missing query file." << std::endl;
85+ exit(1);
86+ }
87+
88+ if (!boost::iends_with(model_file, ".xml")) {
89+ std::cout << "Invalid model file specified." << std::endl;
90+ exit(1);
91+ }
92+
93+ if (!boost::iends_with(query_file, ".q")) {
94+ std::cout << "Invalid query file specified." << std::endl;
95+ exit(1);
96+ }
97+ } else {
98+ if (!boost::iends_with(model_file, ".xml")) {
99+ if (boost::iends_with(query_file, ".xml")) {
100+ // last argument is probably xml, no query-file
101+ model_file = query_file;
102+ } else {
103+ // we have no xml-files at all :(
104+ std::cout << "Invalid model file specified." << std::endl;
105+ exit(1);
106+ }
107+ } else {
108+ std::cout << "Ignoring query-file for Workflow-analysis" << std::endl;
109+ }
110+ query_file = "";
111+ }
112+ options.setInputFile(model_file);
113+ options.setQueryFile(query_file);
114+ return options;
115 }
116
117 VerificationOptions::SearchType intToSearchTypeEnum(int i) {
118@@ -290,6 +317,8 @@
119 return VerificationOptions::RANDOM;
120 case 3:
121 return VerificationOptions::COVERMOST;
122+ case 4:
123+ return VerificationOptions::DEFAULT;
124 default:
125 std::cout << "Unknown search strategy specified." << std::endl;
126 exit(1);
127@@ -366,8 +395,7 @@
128 return vec;
129 }
130
131-VerificationOptions ArgsParser::createVerificationOptions(const option_map& map,
132- const std::string& modelFile, const std::string& queryFile) const {
133+VerificationOptions ArgsParser::createVerificationOptions(const option_map& map) const {
134 assert(map.find(KBOUND_OPTION) != map.end());
135 unsigned int kbound = tryParseInt(*map.find(KBOUND_OPTION));
136
137@@ -400,15 +428,17 @@
138 assert(map.find(WORKFLOW) != map.end());
139 VerificationOptions::WorkflowMode workflow = intToWorkflowTypeEnum(
140 tryParseInt(*map.find(WORKFLOW)));
141-
142+
143+ assert(map.find(STRONG_WORKFLOW_BOUND) != map.end());
144+ unsigned int workflowBound = tryParseInt(*map.find(STRONG_WORKFLOW_BOUND));
145
146
147 assert(map.find(GCD) != map.end());
148 bool enableGCDLowerGuards = boost::lexical_cast<bool>(
149 map.find(GCD)->second);
150
151- return VerificationOptions(modelFile, queryFile, search, verification, memoptimization, kbound, trace,
152- xml_trace, max_constant, keep_dead, enableGCDLowerGuards, workflow);
153+ return VerificationOptions(search, verification, memoptimization, kbound, trace,
154+ xml_trace, max_constant, keep_dead, enableGCDLowerGuards, workflow, workflowBound);
155
156 }
157 }
158
159=== modified file 'src/Core/ArgsParser.hpp'
160--- src/Core/ArgsParser.hpp 2014-03-20 21:43:23 +0000
161+++ src/Core/ArgsParser.hpp 2014-06-11 15:19:00 +0000
162@@ -85,7 +85,8 @@
163
164 VerificationOptions parse(int argc, char* argv[]) const;
165 private:
166- VerificationOptions createVerificationOptions(const option_map& map,const std::string& modelFile, const std::string& queryFile) const;
167+ VerificationOptions createVerificationOptions(const option_map& map) const;
168+ VerificationOptions verifyInputFiles(VerificationOptions, std::string model_file, std::string query_file) const;
169 unsigned int tryParseInt(const option& option) const;
170 std::vector<std::string> parseIncPlaces(const std::string& string) const;
171 void initialize();
172
173=== modified file 'src/Core/VerificationOptions.cpp'
174--- src/Core/VerificationOptions.cpp 2013-12-05 13:23:21 +0000
175+++ src/Core/VerificationOptions.cpp 2014-06-11 15:19:00 +0000
176@@ -20,6 +20,10 @@
177 return "Random Search";
178 case VerificationOptions::DEPTHFIRST:
179 return "Depth-First Search";
180+ case VerificationOptions::BREADTHFIRST:
181+ return "Breadth-First Search";
182+ case VerificationOptions::MINDELAYFIRST:
183+ return "Minimum-Delay-First Search";
184 default:
185 return "Breadth-First Search";
186 }
187@@ -54,8 +58,18 @@
188 if (options.getTrace() != VerificationOptions::NO_TRACE) out << " in " << (options.getXmlTrace() ? "xml format" : "human readable format");
189 out << std::endl;
190 out << "Using " << (options.getGlobalMaxConstantsEnabled() ? "global maximum constant" : "local maximum constants") << " for extrapolation" << std::endl;
191+ if(options.isWorkflow()){
192+ out << "Workflow analysis type : ";
193+ if(options.getWorkflowMode() == VerificationOptions::WORKFLOW_SOUNDNESS){
194+ out << "Soundness" << std::endl;
195+ } else {
196+ out << "Strong soundness" << std::endl;
197+ out << "Bound is : " << options.getWorkflowBound() << std::endl;
198+ }
199+ }
200 out << "Model file is: " << options.getInputFile() << std::endl;
201- out << "Query file is: " << options.getQueryFile() << std::endl;
202+ if(options.getQueryFile() != "")
203+ out << "Query file is: " << options.getQueryFile() << std::endl;
204 return out;
205 }
206 }
207
208=== modified file 'src/Core/VerificationOptions.hpp'
209--- src/Core/VerificationOptions.hpp 2014-02-19 08:42:21 +0000
210+++ src/Core/VerificationOptions.hpp 2014-06-11 15:19:00 +0000
211@@ -15,7 +15,7 @@
212 };
213
214 enum SearchType {
215- BREADTHFIRST, DEPTHFIRST, RANDOM, COVERMOST
216+ BREADTHFIRST, DEPTHFIRST, RANDOM, COVERMOST, DEFAULT, MINDELAYFIRST
217 };
218
219 enum VerificationType {
220@@ -34,8 +34,6 @@
221 }
222
223 VerificationOptions(
224- const std::string& inputFile,
225- const std::string& queryFile,
226 SearchType searchType,
227 VerificationType verificationType,
228 MemoryOptimization memOptimization,
229@@ -45,9 +43,10 @@
230 bool useGlobalMaxConstants,
231 bool keepDeadTokens,
232 bool enableGCDLowerGuards,
233- WorkflowMode workflow
234- ) : inputFile(inputFile),
235- queryFile(queryFile),
236+ WorkflowMode workflow,
237+ int workflowBound
238+ ) : inputFile(""),
239+ queryFile(""),
240 searchType(searchType),
241 verificationType(verificationType),
242 memOptimization(memOptimization),
243@@ -57,7 +56,8 @@
244 useGlobalMaxConstants(useGlobalMaxConstants),
245 keepDeadTokens(keepDeadTokens),
246 enableGCDLowerGuards(enableGCDLowerGuards),
247- workflow(workflow){
248+ workflow(workflow),
249+ workflowBound(workflowBound){
250 };
251
252 public: // inspectors
253@@ -66,9 +66,17 @@
254 return inputFile;
255 }
256
257+ void setInputFile(std::string input) {
258+ inputFile = input;
259+ }
260+
261 const std::string getQueryFile() const {
262 return queryFile;
263 }
264+
265+ void setQueryFile(std::string input) {
266+ queryFile = input;
267+ }
268
269 inline const unsigned int getKBound() const {
270 return k_bound;
271@@ -89,6 +97,10 @@
272 inline const SearchType getSearchType() const {
273 return searchType;
274 }
275+
276+ inline void setSearchType(SearchType type){
277+ searchType = type;
278+ }
279
280 inline const VerificationType getVerificationType() const {
281 return verificationType;
282@@ -107,8 +119,12 @@
283 }
284
285 inline const WorkflowMode getWorkflowMode() const {
286- return workflow;
287- };
288+ return workflow;
289+ };
290+
291+ inline const int getWorkflowBound() const {
292+ return workflowBound;
293+ };
294
295 inline bool isWorkflow() const{
296 return workflow != NOT_WORKFLOW;
297@@ -127,6 +143,7 @@
298 bool keepDeadTokens;
299 bool enableGCDLowerGuards;
300 WorkflowMode workflow;
301+ int workflowBound;
302 };
303
304 std::ostream& operator<<(std::ostream& out, const VerificationOptions& options);
305
306=== modified file 'src/DiscreteVerification/DataStructures/NonStrictMarking.hpp'
307--- src/DiscreteVerification/DataStructures/NonStrictMarking.hpp 2014-02-01 22:13:42 +0000
308+++ src/DiscreteVerification/DataStructures/NonStrictMarking.hpp 2014-06-11 15:19:00 +0000
309@@ -61,6 +61,30 @@
310 public:
311 MetaData* meta;
312 };
313+
314+ class NonStrictMarkingWithTotalDelay : public NonStrictMarking {
315+ private:
316+ unsigned int totalDelay;
317+ public:
318+ NonStrictMarkingWithTotalDelay() : NonStrictMarking(), totalDelay(0) {};
319+ NonStrictMarkingWithTotalDelay(const TAPN::TimedArcPetriNet& tapn, const std::vector<int>& v) : NonStrictMarking(tapn, v), totalDelay(0) {};
320+ NonStrictMarkingWithTotalDelay(const NonStrictMarking& nsm) : NonStrictMarking(nsm), totalDelay(0) {};
321+ NonStrictMarkingWithTotalDelay(const NonStrictMarkingWithTotalDelay& nsm) : NonStrictMarking(nsm), totalDelay(nsm.totalDelay) {};
322+
323+ int getTotalDelay() const {
324+ return totalDelay;
325+ }
326+
327+ void setTotalDelay(const int i){
328+ totalDelay = i;
329+ }
330+
331+ void incrementAge()
332+ {
333+ totalDelay += 1;
334+ NonStrictMarking::incrementAge();
335+ }
336+ };
337
338 } /* namespace DiscreteVerification */
339 } /* namespace VerifyTAPN */
340
341=== modified file 'src/DiscreteVerification/DiscreteVerification.cpp'
342--- src/DiscreteVerification/DiscreteVerification.cpp 2014-02-19 08:42:21 +0000
343+++ src/DiscreteVerification/DiscreteVerification.cpp 2014-06-11 15:19:00 +0000
344@@ -29,7 +29,7 @@
345 return -1;
346 }
347
348- NonStrictMarking* initialMarking = new NonStrictMarking(tapn, initialPlacement);
349+ NonStrictMarkingWithTotalDelay* initialMarking = new NonStrictMarkingWithTotalDelay(tapn, initialPlacement);
350
351 std::cout << "MC: " << tapn.getMaxConstant() << std::endl;
352 #if DEBUG
353
354=== modified file 'src/DiscreteVerification/SearchStrategies/SearchFactory.h'
355--- src/DiscreteVerification/SearchStrategies/SearchFactory.h 2013-10-09 18:44:00 +0000
356+++ src/DiscreteVerification/SearchStrategies/SearchFactory.h 2014-06-11 15:19:00 +0000
357@@ -20,7 +20,10 @@
358 if(options.getWorkflowMode() == options.WORKFLOW_SOUNDNESS){
359 WorkflowMinFirst<T> s;
360 strategy = s.createWaitingList(query);
361- } else if(query->getQuantifier() == EG || query->getQuantifier() == AF){
362+ } if(options.getWorkflowMode() == options.WORKFLOW_STRONG_SOUNDNESS){
363+ NonStrictDFS<T> s;
364+ strategy = s.createWaitingList(query);
365+ } else if(query->getQuantifier() == EG || query->getQuantifier() == AF){
366 //Liveness query, force DFS
367 switch(options.getSearchType()){
368 case VerificationOptions::DEPTHFIRST: {
369@@ -66,6 +69,11 @@
370 strategy = s.createWaitingList(query);
371 break;
372 }
373+ default: {
374+ NonStrictHeuristic<T> s;
375+ strategy = s.createWaitingList(query);
376+ break;
377+ }
378 }
379 }
380 return strategy;
381
382=== modified file 'src/DiscreteVerification/SuccessorGenerator.hpp'
383--- src/DiscreteVerification/SuccessorGenerator.hpp 2013-08-26 13:58:01 +0000
384+++ src/DiscreteVerification/SuccessorGenerator.hpp 2014-06-11 15:19:00 +0000
385@@ -130,7 +130,7 @@
386 }
387 };
388
389- enum Result {QUERY_SATISFIED, QUERY_UNSATISFIED, URGENT_ENABLED};
390+ enum Result {ADDTOPW_RETURNED_TRUE, ADDTOPW_RETURNED_FALSE, ADDTOPW_RETURNED_FALSE_URGENTENABLED};
391
392 template<typename T>
393 class SuccessorGenerator {
394@@ -236,12 +236,12 @@
395
396 enabledTransitions.insert(enabledTransitions.end(), allwaysEnabled.begin(), allwaysEnabled.end());
397 if(generateMarkings(marking, enabledTransitions, enabledArcs)){
398- return QUERY_SATISFIED;
399+ return ADDTOPW_RETURNED_TRUE;
400 } else {
401 if(urgentEnabled){
402- return URGENT_ENABLED;
403+ return ADDTOPW_RETURNED_FALSE_URGENTENABLED;
404 } else{
405- return QUERY_UNSATISFIED;
406+ return ADDTOPW_RETURNED_FALSE;
407 }
408 }
409
410
411=== modified file 'src/DiscreteVerification/VerificationTypes/AbstractNaiveVerification.hpp'
412--- src/DiscreteVerification/VerificationTypes/AbstractNaiveVerification.hpp 2013-10-29 09:16:38 +0000
413+++ src/DiscreteVerification/VerificationTypes/AbstractNaiveVerification.hpp 2014-06-11 15:19:00 +0000
414@@ -28,10 +28,10 @@
415 namespace DiscreteVerification {
416 using namespace std;
417
418- template<typename T>
419- class AbstractNaiveVerification : public Verification<NonStrictMarking> {
420+ template<typename T, typename U>
421+ class AbstractNaiveVerification : public Verification<U> {
422 public:
423- AbstractNaiveVerification(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, T* pwList);
424+ AbstractNaiveVerification(TAPN::TimedArcPetriNet& tapn, U& initialMarking, AST::Query* query, VerificationOptions options, T* pwList);
425
426 void printTransitionStatistics() const {
427 successorGenerator.printTransitionStatistics(std::cout);
428@@ -40,14 +40,14 @@
429 void printStats();
430
431 protected:
432- bool isDelayPossible(NonStrictMarking& marking);
433- virtual bool addToPW(NonStrictMarking* marking, NonStrictMarking* parent) = 0;
434+ bool isDelayPossible(U& marking);
435+ virtual bool addToPW(U* marking, U* parent) = 0;
436
437- inline bool addToPW(NonStrictMarking* m) {
438+ inline bool addToPW(U* m) {
439 return addToPW(m, tmpParent);
440 };
441
442- NonStrictMarking* getLastMarking() {
443+ U* getLastMarking() {
444 return lastMarking;
445 }
446
447@@ -56,32 +56,32 @@
448 };
449
450 protected:
451- SuccessorGenerator<NonStrictMarking> successorGenerator;
452- NonStrictMarking* lastMarking;
453- NonStrictMarking* tmpParent;
454+ SuccessorGenerator<U> successorGenerator;
455+ U* lastMarking;
456+ U* tmpParent;
457 T* pwList;
458 };
459
460- template<typename T>
461- AbstractNaiveVerification<T>::AbstractNaiveVerification(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, T* pwList)
462- : Verification<NonStrictMarking>(tapn, initialMarking, query, options), successorGenerator(tapn, *this), pwList(pwList) {
463+ template<typename T,typename U>
464+ AbstractNaiveVerification<T,U>::AbstractNaiveVerification(TAPN::TimedArcPetriNet& tapn, U& initialMarking, AST::Query* query, VerificationOptions options, T* pwList)
465+ : Verification<U>(tapn, initialMarking, query, options), successorGenerator(tapn, *this), pwList(pwList) {
466
467 };
468
469- template<typename T>
470- void AbstractNaiveVerification<T>::printStats() {
471+ template<typename T,typename U>
472+ void AbstractNaiveVerification<T,U>::printStats() {
473 std::cout << " discovered markings:\t" << pwList->discoveredMarkings << std::endl;
474 std::cout << " explored markings:\t" << pwList->size() - pwList->explored() << std::endl;
475 std::cout << " stored markings:\t" << pwList->size() << std::endl;
476 };
477
478- template<typename T>
479- bool AbstractNaiveVerification<T>::isDelayPossible(NonStrictMarking& marking) {
480+ template<typename T,typename U>
481+ bool AbstractNaiveVerification<T,U>::isDelayPossible(U& marking) {
482 const PlaceList& places = marking.getPlaceList();
483 if (places.size() == 0) return true; //Delay always possible in empty markings
484
485 PlaceList::const_iterator markedPlace_iter = places.begin();
486- for (TAPN::TimedPlace::Vector::const_iterator place_iter = tapn.getPlaces().begin(); place_iter != tapn.getPlaces().end(); place_iter++) {
487+ for (TAPN::TimedPlace::Vector::const_iterator place_iter = this->tapn.getPlaces().begin(); place_iter != this->tapn.getPlaces().end(); place_iter++) {
488 int inv = (*place_iter)->getInvariant().getBound();
489 if (**place_iter == *(markedPlace_iter->place)) {
490 if (markedPlace_iter->maxTokenAge() > inv - 1) {
491
492=== modified file 'src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp'
493--- src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp 2013-10-29 09:16:12 +0000
494+++ src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp 2014-06-11 15:19:00 +0000
495@@ -11,12 +11,12 @@
496 namespace DiscreteVerification {
497
498 LivenessSearch::LivenessSearch(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options)
499- : AbstractNaiveVerification<PWListBase>(tapn, initialMarking, query, options, NULL){
500+ : AbstractNaiveVerification<PWListBase,NonStrictMarking>(tapn, initialMarking, query, options, NULL){
501
502 }
503
504 LivenessSearch::LivenessSearch(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking>* waiting_list)
505- : AbstractNaiveVerification<PWListBase>(tapn, initialMarking, query, options, new PWList(waiting_list, true)){
506+ : AbstractNaiveVerification<PWListBase,NonStrictMarking>(tapn, initialMarking, query, options, new PWList(waiting_list, true)){
507
508 }
509
510@@ -39,9 +39,9 @@
511
512 bool noDelay = false;
513 Result res = successorGenerator.generateAndInsertSuccessors(next_marking);
514- if (res == QUERY_SATISFIED) {
515+ if (res == ADDTOPW_RETURNED_TRUE) {
516 return true;
517- } else if (res == URGENT_ENABLED) {
518+ } else if (res == ADDTOPW_RETURNED_FALSE_URGENTENABLED) {
519 noDelay = true;
520 }
521
522
523=== modified file 'src/DiscreteVerification/VerificationTypes/LivenessSearch.hpp'
524--- src/DiscreteVerification/VerificationTypes/LivenessSearch.hpp 2013-12-05 14:33:59 +0000
525+++ src/DiscreteVerification/VerificationTypes/LivenessSearch.hpp 2014-06-11 15:19:00 +0000
526@@ -29,7 +29,7 @@
527 namespace VerifyTAPN {
528 namespace DiscreteVerification {
529
530- class LivenessSearch : public AbstractNaiveVerification<PWListBase> {
531+ class LivenessSearch : public AbstractNaiveVerification<PWListBase, NonStrictMarking> {
532 public:
533 LivenessSearch(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options);
534 LivenessSearch(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking>* waiting_list);
535
536=== modified file 'src/DiscreteVerification/VerificationTypes/ReachabilitySearch.cpp'
537--- src/DiscreteVerification/VerificationTypes/ReachabilitySearch.cpp 2013-10-29 09:16:12 +0000
538+++ src/DiscreteVerification/VerificationTypes/ReachabilitySearch.cpp 2014-06-11 15:19:00 +0000
539@@ -11,12 +11,12 @@
540 namespace DiscreteVerification {
541
542 ReachabilitySearch::ReachabilitySearch(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options)
543- : AbstractNaiveVerification<PWListBase>(tapn, initialMarking, query, options, NULL){
544+ : AbstractNaiveVerification<PWListBase,NonStrictMarking>(tapn, initialMarking, query, options, NULL){
545
546 }
547
548 ReachabilitySearch::ReachabilitySearch(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking>* waiting_list)
549- : AbstractNaiveVerification<PWListBase>(tapn, initialMarking, query, options, new PWList(waiting_list, false)) {
550+ : AbstractNaiveVerification<PWListBase,NonStrictMarking>(tapn, initialMarking, query, options, new PWList(waiting_list, false)) {
551
552 }
553
554@@ -34,9 +34,9 @@
555
556 bool noDelay = false;
557 Result res = successorGenerator.generateAndInsertSuccessors(next_marking);
558- if(res == QUERY_SATISFIED){
559+ if(res == ADDTOPW_RETURNED_TRUE){
560 return true;
561- } else if (res == URGENT_ENABLED) {
562+ } else if (res == ADDTOPW_RETURNED_FALSE_URGENTENABLED) {
563 noDelay = true;
564 }
565
566
567=== modified file 'src/DiscreteVerification/VerificationTypes/ReachabilitySearch.hpp'
568--- src/DiscreteVerification/VerificationTypes/ReachabilitySearch.hpp 2013-10-29 09:16:12 +0000
569+++ src/DiscreteVerification/VerificationTypes/ReachabilitySearch.hpp 2014-06-11 15:19:00 +0000
570@@ -29,7 +29,7 @@
571 namespace VerifyTAPN {
572 namespace DiscreteVerification {
573
574-class ReachabilitySearch : public AbstractNaiveVerification<PWListBase> {
575+class ReachabilitySearch : public AbstractNaiveVerification<PWListBase,NonStrictMarking> {
576 public:
577 ReachabilitySearch(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options);
578 ReachabilitySearch(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking>* waiting_list);
579
580=== modified file 'src/DiscreteVerification/VerificationTypes/Verification.hpp'
581--- src/DiscreteVerification/VerificationTypes/Verification.hpp 2014-04-06 11:00:59 +0000
582+++ src/DiscreteVerification/VerificationTypes/Verification.hpp 2014-06-11 15:19:00 +0000
583@@ -240,15 +240,15 @@
584 if (m->getNumberOfChildren() > 0) {
585 root->append_node(doc.allocate_node(node_element, "deadlock"));
586 } else {
587- // By default delay forever
588- xml_node<>* node = doc.allocate_node(node_element, "delay", doc.allocate_string("forever"));
589- for (PlaceList::const_iterator iter = m->getPlaceList().begin(); iter != m->getPlaceList().end(); iter++) {
590- if (iter->place->getInvariant().getBound() != std::numeric_limits<int>::max()) {
591- //Invariant, deadlock instead of delay forever
592- node = doc.allocate_node(node_element, "deadlock");
593- break;
594- }
595- }
596+
597+ xml_node<>* node;
598+ if(m->canDeadlock(tapn, 0, false)){
599+ // check if deadlock
600+ node = doc.allocate_node(node_element, "deadlock");
601+ } else {
602+ // if not it is delay forever
603+ node = doc.allocate_node(node_element, "delay", doc.allocate_string("forever"));
604+ }
605 root->append_node(node);
606 }
607 }
608
609=== removed file 'src/DiscreteVerification/VerificationTypes/Workflow.cpp'
610--- src/DiscreteVerification/VerificationTypes/Workflow.cpp 2013-10-29 10:49:49 +0000
611+++ src/DiscreteVerification/VerificationTypes/Workflow.cpp 1970-01-01 00:00:00 +0000
612@@ -1,23 +0,0 @@
613-/*
614- * NonStrictSearch.cpp
615- *
616- * Created on: 26/04/2012
617- * Author: MathiasGS
618- */
619-
620-#include "Workflow.hpp"
621-
622-namespace VerifyTAPN {
623- namespace DiscreteVerification {
624-
625- Workflow::Workflow(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking>* waiting_list)
626- : AbstractNaiveVerification<WorkflowPWList>(tapn, initialMarking, query, options, new WorkflowPWList(waiting_list)), in(NULL), out(NULL){
627- for (TimedPlace::Vector::const_iterator iter = tapn.getPlaces().begin(); iter != tapn.getPlaces().end(); iter++) {
628- if ((*iter)->getType() == Dead) {
629- (*iter)->setType(Std);
630- }
631- }
632- }
633-
634- } /* namespace DiscreteVerification */
635-} /* namespace VerifyTAPN */
636
637=== modified file 'src/DiscreteVerification/VerificationTypes/Workflow.hpp'
638--- src/DiscreteVerification/VerificationTypes/Workflow.hpp 2013-10-29 10:49:49 +0000
639+++ src/DiscreteVerification/VerificationTypes/Workflow.hpp 2014-06-11 15:19:00 +0000
640@@ -29,9 +29,10 @@
641 namespace VerifyTAPN {
642 namespace DiscreteVerification {
643
644-class Workflow : public AbstractNaiveVerification<WorkflowPWList> {
645+template<typename T>
646+class Workflow : public AbstractNaiveVerification<WorkflowPWList,T> {
647 public:
648- Workflow(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking>* waiting_list);
649+ Workflow(TAPN::TimedArcPetriNet& tapn, T& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking>* waiting_list);
650 virtual void printExecutionTime(ostream& stream) = 0;
651
652 protected:
653@@ -39,6 +40,16 @@
654 TimedPlace* out;
655 };
656
657+template<typename T>
658+Workflow<T>::Workflow(TAPN::TimedArcPetriNet& tapn, T& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking>* waiting_list)
659+: AbstractNaiveVerification<WorkflowPWList,T>(tapn, initialMarking, query, options, new WorkflowPWList(waiting_list)), in(NULL), out(NULL){
660+ for (TimedPlace::Vector::const_iterator iter = tapn.getPlaces().begin(); iter != tapn.getPlaces().end(); iter++) {
661+ if ((*iter)->getType() == Dead) {
662+ (*iter)->setType(Std);
663+ }
664+ }
665+}
666+
667 } /* namespace DiscreteVerification */
668 } /* namespace VerifyTAPN */
669 #endif /* NONSTRICTSEARCH_HPP_ */
670\ No newline at end of file
671
672=== modified file 'src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp'
673--- src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp 2014-02-01 22:13:42 +0000
674+++ src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp 2014-06-11 15:19:00 +0000
675@@ -11,7 +11,8 @@
676 namespace DiscreteVerification {
677
678 WorkflowSoundness::WorkflowSoundness(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking>* waiting_list)
679-: Workflow(tapn, initialMarking, query, options, waiting_list), passed_stack(), min_exec(INT_MAX), linearSweepTreshold(3), coveredMarking(NULL), modelType(calculateModelType()){
680+: Workflow<NonStrictMarking>(tapn, initialMarking, query, options, waiting_list), passedStack(), minExec(INT_MAX), linearSweepTreshold(3), coveredMarking(NULL), modelType(calculateModelType()){
681+
682 }
683
684 bool WorkflowSoundness::verify(){
685@@ -25,9 +26,9 @@
686 tmpParent = &next_marking;
687 bool noDelay = false;
688 Result res = successorGenerator.generateAndInsertSuccessors(next_marking);
689- if(res == QUERY_SATISFIED){
690+ if(res == ADDTOPW_RETURNED_TRUE){
691 return false;
692- } else if (res == URGENT_ENABLED) {
693+ } else if (res == ADDTOPW_RETURNED_FALSE_URGENTENABLED) {
694 noDelay = true;
695 }
696
697@@ -45,15 +46,15 @@
698 // Phase 2
699 // mark all as passed which ends in a final marking
700 int passed = 0;
701- while(passed_stack.size()){
702- WorkflowSoundnessMetaData* next = passed_stack.top();
703- passed_stack.pop();
704+ while(passedStack.size()){
705+ WorkflowSoundnessMetaData* next = passedStack.top();
706+ passedStack.pop();
707 if(next->passed) continue;
708 next->passed = true;
709 ++passed;
710 for(vector<WorkflowSoundnessMetaData*>::iterator iter = next->parents.begin();
711 iter != next->parents.end(); iter++){
712- passed_stack.push(*iter);
713+ passedStack.push(*iter);
714 }
715 }
716
717@@ -113,10 +114,10 @@
718 marking_meta_data->parents.push_back(((WorkflowSoundnessMetaData*)parent->meta));
719 // Set min
720 marking_meta_data->min = min(marking_meta_data->min, ((WorkflowSoundnessMetaData*)parent->meta)->min); // Transition
721- passed_stack.push(marking_meta_data);
722+ passedStack.push(marking_meta_data);
723 // keep track of shortest trace
724- if (marking_meta_data->min < min_exec) {
725- min_exec = marking_meta_data->min;
726+ if (marking_meta_data->min < minExec) {
727+ minExec = marking_meta_data->min;
728 lastMarking = marking;
729 }
730 }else{
731
732=== modified file 'src/DiscreteVerification/VerificationTypes/WorkflowSoundness.hpp'
733--- src/DiscreteVerification/VerificationTypes/WorkflowSoundness.hpp 2014-02-01 22:13:42 +0000
734+++ src/DiscreteVerification/VerificationTypes/WorkflowSoundness.hpp 2014-06-11 15:19:00 +0000
735@@ -29,7 +29,7 @@
736 namespace VerifyTAPN {
737 namespace DiscreteVerification {
738
739-class WorkflowSoundness : public Workflow {
740+class WorkflowSoundness : public Workflow<NonStrictMarking> {
741 public:
742 enum ModelType{
743 MTAWFN, ETAWFN, NOTTAWFN
744@@ -42,7 +42,7 @@
745 return getTrace(lastMarking);
746 }
747 void printExecutionTime(ostream& stream){
748- stream << "Minimum execution time: " << min_exec << endl;
749+ stream << "Minimum execution time: " << minExec << endl;
750 }
751 void printMessages(ostream& stream){
752 if(coveredMarking != NULL){
753@@ -58,8 +58,8 @@
754 ModelType calculateModelType();
755
756 protected:
757- stack<WorkflowSoundnessMetaData*> passed_stack;
758- int min_exec;
759+ stack<WorkflowSoundnessMetaData*> passedStack;
760+ int minExec;
761 unsigned int linearSweepTreshold;
762 NonStrictMarking* coveredMarking;
763 ModelType modelType;
764
765=== modified file 'src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.cpp'
766--- src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.cpp 2014-02-08 10:18:04 +0000
767+++ src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.cpp 2014-06-11 15:19:00 +0000
768@@ -10,26 +10,13 @@
769 namespace VerifyTAPN {
770 namespace DiscreteVerification {
771
772- WorkflowStrongSoundnessReachability::WorkflowStrongSoundnessReachability(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking>* waiting_list)
773- : Workflow(tapn, initialMarking, query, options, waiting_list), max_value(-1), timer(NULL), term1(NULL), term2(NULL) {
774+ WorkflowStrongSoundnessReachability::WorkflowStrongSoundnessReachability(TAPN::TimedArcPetriNet& tapn, NonStrictMarkingWithTotalDelay& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking>* waiting_list)
775+ : Workflow<NonStrictMarkingWithTotalDelay>(tapn, initialMarking, query, options, waiting_list), maxValue(-1), outPlace(NULL){
776 // Find timer place and store as out
777 for (TimedPlace::Vector::const_iterator iter = tapn.getPlaces().begin(); iter != tapn.getPlaces().end(); ++iter) {
778- if ((*iter)->getInvariant() != (*iter)->getInvariant().LS_INF) {
779- if (timer == NULL || timer->getInvariant().getBound() < (*iter)->getInvariant().getBound()) {
780- timer = *iter;
781- }
782- }
783-
784- if (!(*iter)->getTransportArcs().empty() || !(*iter)->getInputArcs().empty()) {
785- continue;
786- }
787-
788- if (term1 == NULL) {
789- term1 = *iter;
790- } else if (term2 == NULL) {
791- term2 = *iter;
792- } else {
793- assert(false);
794+ if ((*iter)->getTransportArcs().empty() && (*iter)->getInputArcs().empty()) {
795+ outPlace = *iter;
796+ break;
797 }
798 }
799 };
800@@ -41,35 +28,64 @@
801
802 //Main loop
803 while (pwList->hasWaitingStates()) {
804- NonStrictMarking& next_marking = *pwList->getNextUnexplored();
805+ NonStrictMarkingWithTotalDelay& next_marking =
806+ static_cast<NonStrictMarkingWithTotalDelay&>(*pwList->getNextUnexplored());
807 tmpParent = &next_marking;
808+
809+ // push onto trace
810+ trace.push(&next_marking);
811+ next_marking.meta->inTrace = true;
812+ validChildren = 0;
813
814 bool noDelay = false;
815 Result res = successorGenerator.generateAndInsertSuccessors(next_marking);
816- if (res == QUERY_SATISFIED) {
817+ if (res == ADDTOPW_RETURNED_TRUE) {
818 return true;
819- } else if (res == URGENT_ENABLED) {
820+ } else if (res == ADDTOPW_RETURNED_FALSE_URGENTENABLED) {
821 noDelay = true;
822 }
823
824- // Generate next markings
825+ // Generate delays markings
826 if (!noDelay && isDelayPossible(next_marking)) {
827- NonStrictMarking* marking = new NonStrictMarking(next_marking);
828+ NonStrictMarkingWithTotalDelay* marking = new NonStrictMarkingWithTotalDelay(next_marking);
829 marking->incrementAge();
830 marking->setGeneratedBy(NULL);
831+ if(marking->getTotalDelay() > options.getWorkflowBound()){
832+ // if the bound is exceeded, terminate
833+ marking->setParent(&next_marking);
834+ lastMarking = marking;
835+ return true;
836+ }
837 if (addToPW(marking, &next_marking)) {
838+ lastMarking = marking;
839 return true;
840 }
841 }
842+ if(validChildren != 0){
843+ next_marking.setNumberOfChildren(validChildren);
844+ } else {
845+ // remove childless markings from stack
846+ while(!trace.empty() && trace.top()->getNumberOfChildren() <= 1){
847+ trace.top()->meta->inTrace = false;
848+ trace.pop();
849+ }
850+ if(trace.empty()){
851+ // this should only happen when the waitinglist is empty
852+ return false;
853+ }
854+ trace.top()->decrementNumberOfChildren();
855+ }
856 }
857+ // should never reach here
858+ assert(false);
859 return false;
860 }
861
862 void WorkflowStrongSoundnessReachability::getTrace() {
863- std::stack < NonStrictMarking*> printStack;
864- NonStrictMarking* next = lastMarking;
865+ std::stack < NonStrictMarkingWithTotalDelay*> printStack;
866+ NonStrictMarkingWithTotalDelay* next = lastMarking;
867 do {
868- NonStrictMarking* parent = (NonStrictMarking*)next->getParent();
869+ NonStrictMarkingWithTotalDelay* parent = (NonStrictMarkingWithTotalDelay*)next->getParent();
870 printStack.push(next);
871 next = parent;
872
873@@ -82,11 +98,11 @@
874 if (options.getXmlTrace()) {
875 printXMLTrace(lastMarking, printStack, query, tapn);
876 } else {
877- printHumanTrace(lastMarking, printStack, query->getQuantifier());
878+ printHumanTrace(lastMarking, printStack, query->getQuantifier());
879 }
880 }
881
882- bool WorkflowStrongSoundnessReachability::addToPW(NonStrictMarking* marking, NonStrictMarking* parent) {
883+ bool WorkflowStrongSoundnessReachability::addToPW(NonStrictMarkingWithTotalDelay* marking, NonStrictMarkingWithTotalDelay* parent) {
884 marking->cut();
885 marking->setParent(parent);
886
887@@ -101,41 +117,47 @@
888
889 /* Handle max */
890 // Map to existing marking if any
891- NonStrictMarking* old = pwList->addToPassed(marking);
892- bool isNew = false;
893- if(old == NULL){
894- isNew = true;
895- } else {
896- delete marking;
897- marking = old;
898+ NonStrictMarkingWithTotalDelay* old = (NonStrictMarkingWithTotalDelay*)pwList->addToPassed(marking);
899+ if(old != NULL) {
900+ if(old->getTotalDelay() < marking->getTotalDelay()) {
901+ if(old->meta->inTrace){
902+ // delay loop
903+ lastMarking = marking;
904+ // make sure we can print trace
905+ marking->setNumberOfChildren(1);
906+ trace.push(marking);
907+ maxValue = marking->getTotalDelay();
908+ return true;
909+ } else {
910+ // search again to find maxdelay
911+ // copy data from new
912+ old->setParent(marking->getParent());
913+ old->setGeneratedBy(marking->getGeneratedBy());
914+ old->setTotalDelay(marking->getTotalDelay());
915+ delete marking;
916+ marking = old;
917+ // fall through on purpose
918+ }
919+ } else {
920+ delete marking;
921+ // already seen this maxage/marking combination
922+ return false;
923+ }
924+ } else {
925+ marking->meta = new MetaData();
926 }
927-
928
929- if (marking->getParent() == NULL) marking->setParent(parent);
930-
931- if (!marking->getTokenList(timer->getIndex()).empty() &&
932- (marking->getTokenList(timer->getIndex()).at(0).getAge() > max_value ||
933- (marking->getTokenList(timer->getIndex()).at(0).getAge() == max_value &&
934- (!marking->getTokenList(term1->getIndex()).empty() || !marking->getTokenList(term2->getIndex()).empty())))) {
935- max_value = marking->getTokenList(timer->getIndex()).at(0).getAge();
936- lastMarking = marking;
937- }
938-
939- // Add to passed
940- if (isNew) {
941+ if(marking->numberOfTokensInPlace(outPlace->getIndex()) == 0){
942+ // if nonterminal, add to waiting
943 pwList->addToWaiting(marking);
944- QueryVisitor<NonStrictMarking> checker(*marking, tapn);
945- BoolResult context;
946-
947- query->accept(checker, context);
948- if (context.value) {
949+ ++validChildren;
950+ } else {
951+ // if terminal, update max_value and last marking of trace
952+ if(maxValue < marking->getTotalDelay()) {
953+ maxValue = marking->getTotalDelay();
954 lastMarking = marking;
955- return true;
956- } else {
957- return false;
958 }
959 }
960-
961 return false;
962 }
963
964
965=== modified file 'src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.hpp'
966--- src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.hpp 2013-10-29 10:24:54 +0000
967+++ src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.hpp 2014-06-11 15:19:00 +0000
968@@ -12,30 +12,30 @@
969 #include "../DataStructures/WorkflowPWList.hpp"
970 #include "Workflow.hpp"
971 #include <stack>
972+#include <algorithm>
973
974 namespace VerifyTAPN {
975 namespace DiscreteVerification {
976
977-class WorkflowStrongSoundnessReachability : public Workflow{
978+class WorkflowStrongSoundnessReachability : public Workflow<NonStrictMarkingWithTotalDelay>{
979 public:
980
981- WorkflowStrongSoundnessReachability(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking>* waiting_list);
982+ WorkflowStrongSoundnessReachability(TAPN::TimedArcPetriNet& tapn, NonStrictMarkingWithTotalDelay& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking>* waiting_list);
983
984 bool verify();
985 void getTrace();
986
987 void printExecutionTime(ostream& stream){
988- stream << "Maximum execution time: " << max_value << endl;
989+ stream << "Maximum execution time: " << (maxValue * tapn.getGCD()) << endl;
990 }
991
992
993 protected:
994- bool addToPW(NonStrictMarking* marking, NonStrictMarking* parent);
995+ bool addToPW(NonStrictMarkingWithTotalDelay* marking, NonStrictMarkingWithTotalDelay* parent);
996 protected:
997- int max_value;
998- TimedPlace* timer;
999- TimedPlace* term1;
1000- TimedPlace* term2;
1001+ int maxValue;
1002+ TimedPlace* outPlace;
1003+ int validChildren;
1004 };
1005
1006 } /* namespace DiscreteVerification */
1007
1008=== modified file 'src/main.cpp'
1009--- src/main.cpp 2014-02-19 08:42:21 +0000
1010+++ src/main.cpp 2014-06-11 15:19:00 +0000
1011@@ -32,14 +32,44 @@
1012
1013 std::vector<int> initialPlacement(modelParser.parseMarking(options.getInputFile(), *tapn));
1014
1015- AST::Query* query;
1016- try{
1017- TAPNQueryParser queryParser(*tapn);
1018- queryParser.parse(options.getQueryFile());
1019- query = queryParser.getAST();
1020- }catch(...){
1021- std::cout << "There was an error parsing the query file." << std::endl;
1022- return 1;
1023+ AST::Query* query = NULL;
1024+ if (options.getWorkflowMode() == VerificationOptions::WORKFLOW_SOUNDNESS ||
1025+ options.getWorkflowMode() == VerificationOptions::WORKFLOW_STRONG_SOUNDNESS) {
1026+ if(options.getGCDLowerGuardsEnabled()){
1027+ cout << "Workflow-analysis does not support GCD-lowering" << endl;
1028+ exit(1);
1029+ }
1030+
1031+ if (options.getSearchType() != VerificationOptions::DEFAULT) {
1032+ cout << "Workflow-analysis only supports the default search-strategy" << endl;
1033+ exit(1);
1034+ }
1035+
1036+ if(options.getQueryFile() != ""){
1037+ cout << "Workflow-analysis does not accept a query file" << endl;
1038+ exit(1);
1039+ }
1040+
1041+ if(options.getWorkflowMode() == VerificationOptions::WORKFLOW_SOUNDNESS) {
1042+ options.setSearchType(VerificationOptions::MINDELAYFIRST);
1043+ query = new AST::Query(AST::EF, new AST::BoolExpression(true));
1044+ } else if(options.getWorkflowMode() == VerificationOptions::WORKFLOW_STRONG_SOUNDNESS) {
1045+ options.setSearchType(VerificationOptions::DEPTHFIRST);
1046+ query = new AST::Query(AST::AF, new AST::BoolExpression(false));
1047+ }
1048+
1049+ } else {
1050+ if (options.getSearchType() == VerificationOptions::DEFAULT) {
1051+ options.setSearchType(VerificationOptions::COVERMOST);
1052+ }
1053+ try{
1054+ TAPNQueryParser queryParser(*tapn);
1055+ queryParser.parse(options.getQueryFile());
1056+ query = queryParser.getAST();
1057+ }catch(...){
1058+ std::cout << "There was an error parsing the query file." << std::endl;
1059+ return 1;
1060+ }
1061 }
1062
1063 if (tapn->containsOrphanTransitions()) {

Subscribers

People subscribed via source and target branches