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

[Jakob Dyhr]

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

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.

[Jiri Srba (srba)]

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

review: Needs Information

[Jiri Srba (srba)]

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)]

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)]

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]

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)]

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

[Jiri Srba (srba)]

review: Approve

=== 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 @@
         
         optionsOut += ",LPSolve_Timeout=" + std::to_string(lpsolveTimeout);
         
-        if (isctl) {
-            if (ctlalgorithm == CTL::CZero) {
-                optionsOut += ",CTLAlgorithm=CZERO";
-            } else {
-                optionsOut += ",CTLAlgorithm=LOCAL";
-            }
+
+        if (ctlalgorithm == CTL::CZero) {
+            optionsOut += ",CTLAlgorithm=CZERO";
+        } else {
+            optionsOut += ",CTLAlgorithm=LOCAL";
         }
+        
         optionsOut += "\n";
         
         std::cout << optionsOut;

=== 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 @@
                 return ErrorCode;
             }
         } else if (strcmp(argv[i], "-ctl") == 0){
-            options.isctl = true;
             if(argc > i + 1){
                 if(strcmp(argv[i + 1], "local") == 0){
                     i++;
@@ -322,18 +321,6 @@
         fprintf(stderr, "Argument Error: No query-file provided\n");
         return ErrorCode;
     }
-
-    // Check strategy when is CTL (CTLEngine does not support all of them)
-    if(options.isctl){
-        //Default to DFS (No heuristic strategy)
-        if(options.strategy == PetriEngine::Reachability::HEUR){
-            options.strategy = PetriEngine::Reachability::DFS;
-        }
-        else if(options.strategy != PetriEngine::Reachability::DFS){
-            std::cerr << "Argument Error: Invalid CTL search strategy. Only DFS is supported by CTL engine." << std::endl;
-            return ErrorCode;
-        }
-    }
     
     // Check if the choosen options are incompatible with upper bound queries
     if(options.stubbornreduction || options.queryReductionTimeout > 0) {
@@ -525,21 +512,6 @@
     
     if(parseModel(transitionEnabledness, builder, options) != ContinueCode) return ErrorCode;
     
-    //---------------- CTL Engine - forced CTL via FLAG -ctl -----------------//
-    if(options.isctl){
-        PetriNet* net = builder.makePetriNet();
-        ReturnValue rv = CTLMain(net,
-                    options.queryfile,
-                    options.ctlalgorithm,
-                    options.strategy,
-                    options.querynumbers,
-                    options.gamemode,
-                    options.printstatistics,
-                    true);
-        delete net;
-        return rv;
-    }
-    
     //----------------------- Parse Query -----------------------//
     std::vector<std::string> querynames;
     auto queries = readQueries(transitionEnabledness, options, querynames);
@@ -636,6 +608,7 @@
     std::string CTLQueries = getXMLQueries(queries, querynames, results);
     
     if (CTLQueries.size() > 0) {
+        options.isctl=true;
         PetriEngine::Reachability::Strategy reachabilityStrategy=options.strategy;
         PetriNet* ctlnet = builder.makePetriNet();
         // Update query indexes
@@ -646,12 +619,16 @@
             options.querynumbers.insert(x);
         }
         
-        // Default to DFS if strategy is not BFS or DFS (No heuristic strategy)        
-        if(options.strategy != PetriEngine::Reachability::DFS){
+        //Default to DFS (No heuristic strategy)
+        if(options.strategy == PetriEngine::Reachability::HEUR){
+            fprintf(stdout, "Default search strategy was changed to DFS as the CTL engine is called.\n");
             options.strategy = PetriEngine::Reachability::DFS;
-            fprintf(stdout, "Search strategy was changed to DFS as the CTL engine is called.\n");
-        }
-        
+        }
+        else if(options.strategy != PetriEngine::Reachability::DFS){
+            std::cerr << "Argument Error: Invalid CTL search strategy. Only DFS is supported by CTL engine." << std::endl;
+            return ErrorCode;
+        }
+   
         v = CTLMain(ctlnet,
             options.queryfile,
             options.ctlalgorithm,
@@ -670,7 +647,7 @@
         // go back to previous strategy if the program continues
         options.strategy=reachabilityStrategy;
     }
-    
+    options.isctl=false;
     //--------------------- Apply Net Reduction ---------------//
         
     if (options.enablereduction == 1 || options.enablereduction == 2) {