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

Proposed by Jakob Dyhr on 2017-05-15
Status: Merged
Approved by: Jiri Srba on 2017-05-17
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 2017-05-15 Approve on 2017-05-17
Jakob Dyhr (community) Resubmit on 2017-05-16
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.
Jiri Srba (srba) wrote :

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

review: Needs Information
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).

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?

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 on 2017-05-16
181. By Jakob Dyhr on 2017-05-16

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

182. By Jakob Dyhr on 2017-05-16

always print ctl options

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: Resubmit
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 'PetriEngine/options.h'
2--- PetriEngine/options.h 2017-05-02 13:57:24 +0000
3+++ PetriEngine/options.h 2017-05-16 08:21:50 +0000
4@@ -95,13 +95,13 @@
5
6 optionsOut += ",LPSolve_Timeout=" + std::to_string(lpsolveTimeout);
7
8- if (isctl) {
9- if (ctlalgorithm == CTL::CZero) {
10- optionsOut += ",CTLAlgorithm=CZERO";
11- } else {
12- optionsOut += ",CTLAlgorithm=LOCAL";
13- }
14+
15+ if (ctlalgorithm == CTL::CZero) {
16+ optionsOut += ",CTLAlgorithm=CZERO";
17+ } else {
18+ optionsOut += ",CTLAlgorithm=LOCAL";
19 }
20+
21 optionsOut += "\n";
22
23 std::cout << optionsOut;
24
25=== modified file 'VerifyPN.cpp'
26--- VerifyPN.cpp 2017-05-15 19:44:00 +0000
27+++ VerifyPN.cpp 2017-05-16 08:21:50 +0000
28@@ -203,7 +203,6 @@
29 return ErrorCode;
30 }
31 } else if (strcmp(argv[i], "-ctl") == 0){
32- options.isctl = true;
33 if(argc > i + 1){
34 if(strcmp(argv[i + 1], "local") == 0){
35 i++;
36@@ -322,18 +321,6 @@
37 fprintf(stderr, "Argument Error: No query-file provided\n");
38 return ErrorCode;
39 }
40-
41- // Check strategy when is CTL (CTLEngine does not support all of them)
42- if(options.isctl){
43- //Default to DFS (No heuristic strategy)
44- if(options.strategy == PetriEngine::Reachability::HEUR){
45- options.strategy = PetriEngine::Reachability::DFS;
46- }
47- else if(options.strategy != PetriEngine::Reachability::DFS){
48- std::cerr << "Argument Error: Invalid CTL search strategy. Only DFS is supported by CTL engine." << std::endl;
49- return ErrorCode;
50- }
51- }
52
53 // Check if the choosen options are incompatible with upper bound queries
54 if(options.stubbornreduction || options.queryReductionTimeout > 0) {
55@@ -525,21 +512,6 @@
56
57 if(parseModel(transitionEnabledness, builder, options) != ContinueCode) return ErrorCode;
58
59- //---------------- CTL Engine - forced CTL via FLAG -ctl -----------------//
60- if(options.isctl){
61- PetriNet* net = builder.makePetriNet();
62- ReturnValue rv = CTLMain(net,
63- options.queryfile,
64- options.ctlalgorithm,
65- options.strategy,
66- options.querynumbers,
67- options.gamemode,
68- options.printstatistics,
69- true);
70- delete net;
71- return rv;
72- }
73-
74 //----------------------- Parse Query -----------------------//
75 std::vector<std::string> querynames;
76 auto queries = readQueries(transitionEnabledness, options, querynames);
77@@ -636,6 +608,7 @@
78 std::string CTLQueries = getXMLQueries(queries, querynames, results);
79
80 if (CTLQueries.size() > 0) {
81+ options.isctl=true;
82 PetriEngine::Reachability::Strategy reachabilityStrategy=options.strategy;
83 PetriNet* ctlnet = builder.makePetriNet();
84 // Update query indexes
85@@ -646,12 +619,16 @@
86 options.querynumbers.insert(x);
87 }
88
89- // Default to DFS if strategy is not BFS or DFS (No heuristic strategy)
90- if(options.strategy != PetriEngine::Reachability::DFS){
91+ //Default to DFS (No heuristic strategy)
92+ if(options.strategy == PetriEngine::Reachability::HEUR){
93+ fprintf(stdout, "Default search strategy was changed to DFS as the CTL engine is called.\n");
94 options.strategy = PetriEngine::Reachability::DFS;
95- fprintf(stdout, "Search strategy was changed to DFS as the CTL engine is called.\n");
96- }
97-
98+ }
99+ else if(options.strategy != PetriEngine::Reachability::DFS){
100+ std::cerr << "Argument Error: Invalid CTL search strategy. Only DFS is supported by CTL engine." << std::endl;
101+ return ErrorCode;
102+ }
103+
104 v = CTLMain(ctlnet,
105 options.queryfile,
106 options.ctlalgorithm,
107@@ -670,7 +647,7 @@
108 // go back to previous strategy if the program continues
109 options.strategy=reachabilityStrategy;
110 }
111-
112+ options.isctl=false;
113 //--------------------- Apply Net Reduction ---------------//
114
115 if (options.enablereduction == 1 || options.enablereduction == 2) {

Subscribers

People subscribed via source and target branches