Merge lp:~verifypn-stub/verifypn/ctl-flow into lp:verifypn

Proposed by Jakob Dyhr
Status: Merged
Approved by: Jiri Srba
Approved revision: 182
Merged at revision: 181
Proposed branch: lp:~verifypn-stub/verifypn/ctl-flow
Merge into: lp:verifypn
Diff against target: 115 lines (+17/-40)
2 files modified
PetriEngine/options.h (+6/-6)
VerifyPN.cpp (+11/-34)
To merge this branch: bzr merge lp:~verifypn-stub/verifypn/ctl-flow
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Jakob Dyhr (community) Needs Resubmitting
Review via email: mp+324048@code.launchpad.net

Commit message

Flag '-ctl' no longer force calls the ctl engine. Instead, the flag only sets the CTL algorithm.

Description of the change

We do this change to be able to call verifypn from the TAPAAL gui with either "-ctl zcero" or "-ctl local", without worrying about it changing the optimal flow in the verifypn main.

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

Why, then there is no way to call the CTL engine on EF and AG queries?

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

OK, I like the idea now, it will work better with the GUI. However, the first removed
code at lines 8 to 19 should stay (the defaul heuristic CTL search strategy should be changed to DFS).

Revision history for this message
Jakob Dyhr (jdyhr12) wrote :

The change to DFS is done on line 624 in http://bazaar.launchpad.net/~verifypn-stub/verifypn/ctl-flow/view/head:/VerifyPN.cpp

However, this code does not give an error if the search strategy is e.g BFS like the previous code did on lines 8-19. It simply changes strategy to DFS since it is the only valid strategy.

Is this the intended behavior?

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

No, CTL engine can be called with DFS or Heuristic search (which in this case becomes DFS).
Call with BFS or RDFS should exit with error message that the strategy is not possible for
CTL engine.

lp:~verifypn-stub/verifypn/ctl-flow updated
181. By Jakob Dyhr

Throw error if CTL engine is called with non-DFS strategy

182. By Jakob Dyhr

always print ctl options

Revision history for this message
Jakob Dyhr (jdyhr12) wrote :

I inserted the strategy check and error message into the part where we have identified the query to be CTL. We cannot do the check already on line 8 anymore, as we do not know if the query will require the CTL engine at that point.

review: Needs Resubmitting
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
=== modified file 'PetriEngine/options.h'
--- PetriEngine/options.h 2017-05-02 13:57:24 +0000
+++ PetriEngine/options.h 2017-05-16 08:21:50 +0000
@@ -95,13 +95,13 @@
95 95
96 optionsOut += ",LPSolve_Timeout=" + std::to_string(lpsolveTimeout);96 optionsOut += ",LPSolve_Timeout=" + std::to_string(lpsolveTimeout);
97 97
98 if (isctl) {98
99 if (ctlalgorithm == CTL::CZero) {99 if (ctlalgorithm == CTL::CZero) {
100 optionsOut += ",CTLAlgorithm=CZERO";100 optionsOut += ",CTLAlgorithm=CZERO";
101 } else {101 } else {
102 optionsOut += ",CTLAlgorithm=LOCAL";102 optionsOut += ",CTLAlgorithm=LOCAL";
103 }
104 }103 }
104
105 optionsOut += "\n";105 optionsOut += "\n";
106 106
107 std::cout << optionsOut;107 std::cout << optionsOut;
108108
=== modified file 'VerifyPN.cpp'
--- VerifyPN.cpp 2017-05-15 19:44:00 +0000
+++ VerifyPN.cpp 2017-05-16 08:21:50 +0000
@@ -203,7 +203,6 @@
203 return ErrorCode;203 return ErrorCode;
204 }204 }
205 } else if (strcmp(argv[i], "-ctl") == 0){205 } else if (strcmp(argv[i], "-ctl") == 0){
206 options.isctl = true;
207 if(argc > i + 1){206 if(argc > i + 1){
208 if(strcmp(argv[i + 1], "local") == 0){207 if(strcmp(argv[i + 1], "local") == 0){
209 i++;208 i++;
@@ -322,18 +321,6 @@
322 fprintf(stderr, "Argument Error: No query-file provided\n");321 fprintf(stderr, "Argument Error: No query-file provided\n");
323 return ErrorCode;322 return ErrorCode;
324 }323 }
325
326 // Check strategy when is CTL (CTLEngine does not support all of them)
327 if(options.isctl){
328 //Default to DFS (No heuristic strategy)
329 if(options.strategy == PetriEngine::Reachability::HEUR){
330 options.strategy = PetriEngine::Reachability::DFS;
331 }
332 else if(options.strategy != PetriEngine::Reachability::DFS){
333 std::cerr << "Argument Error: Invalid CTL search strategy. Only DFS is supported by CTL engine." << std::endl;
334 return ErrorCode;
335 }
336 }
337 324
338 // Check if the choosen options are incompatible with upper bound queries325 // Check if the choosen options are incompatible with upper bound queries
339 if(options.stubbornreduction || options.queryReductionTimeout > 0) {326 if(options.stubbornreduction || options.queryReductionTimeout > 0) {
@@ -525,21 +512,6 @@
525 512
526 if(parseModel(transitionEnabledness, builder, options) != ContinueCode) return ErrorCode;513 if(parseModel(transitionEnabledness, builder, options) != ContinueCode) return ErrorCode;
527 514
528 //---------------- CTL Engine - forced CTL via FLAG -ctl -----------------//
529 if(options.isctl){
530 PetriNet* net = builder.makePetriNet();
531 ReturnValue rv = CTLMain(net,
532 options.queryfile,
533 options.ctlalgorithm,
534 options.strategy,
535 options.querynumbers,
536 options.gamemode,
537 options.printstatistics,
538 true);
539 delete net;
540 return rv;
541 }
542
543 //----------------------- Parse Query -----------------------//515 //----------------------- Parse Query -----------------------//
544 std::vector<std::string> querynames;516 std::vector<std::string> querynames;
545 auto queries = readQueries(transitionEnabledness, options, querynames);517 auto queries = readQueries(transitionEnabledness, options, querynames);
@@ -636,6 +608,7 @@
636 std::string CTLQueries = getXMLQueries(queries, querynames, results);608 std::string CTLQueries = getXMLQueries(queries, querynames, results);
637 609
638 if (CTLQueries.size() > 0) {610 if (CTLQueries.size() > 0) {
611 options.isctl=true;
639 PetriEngine::Reachability::Strategy reachabilityStrategy=options.strategy;612 PetriEngine::Reachability::Strategy reachabilityStrategy=options.strategy;
640 PetriNet* ctlnet = builder.makePetriNet();613 PetriNet* ctlnet = builder.makePetriNet();
641 // Update query indexes614 // Update query indexes
@@ -646,12 +619,16 @@
646 options.querynumbers.insert(x);619 options.querynumbers.insert(x);
647 }620 }
648 621
649 // Default to DFS if strategy is not BFS or DFS (No heuristic strategy) 622 //Default to DFS (No heuristic strategy)
650 if(options.strategy != PetriEngine::Reachability::DFS){623 if(options.strategy == PetriEngine::Reachability::HEUR){
624 fprintf(stdout, "Default search strategy was changed to DFS as the CTL engine is called.\n");
651 options.strategy = PetriEngine::Reachability::DFS;625 options.strategy = PetriEngine::Reachability::DFS;
652 fprintf(stdout, "Search strategy was changed to DFS as the CTL engine is called.\n");626 }
653 }627 else if(options.strategy != PetriEngine::Reachability::DFS){
654 628 std::cerr << "Argument Error: Invalid CTL search strategy. Only DFS is supported by CTL engine." << std::endl;
629 return ErrorCode;
630 }
631
655 v = CTLMain(ctlnet,632 v = CTLMain(ctlnet,
656 options.queryfile,633 options.queryfile,
657 options.ctlalgorithm,634 options.ctlalgorithm,
@@ -670,7 +647,7 @@
670 // go back to previous strategy if the program continues647 // go back to previous strategy if the program continues
671 options.strategy=reachabilityStrategy;648 options.strategy=reachabilityStrategy;
672 }649 }
673 650 options.isctl=false;
674 //--------------------- Apply Net Reduction ---------------//651 //--------------------- Apply Net Reduction ---------------//
675 652
676 if (options.enablereduction == 1 || options.enablereduction == 2) {653 if (options.enablereduction == 1 || options.enablereduction == 2) {

Subscribers

People subscribed via source and target branches