Merge lp:~tapaal-ltl/verifypn/simple-ltl-heuristics into lp:verifypn

[Nikolaj Jensen Ulrik]

Kill off the complex, non-impactful LTL heuristics. These remain available on the `experimental-ltl-heuristics` branch.
Required bison version was reverted back to before the `fix-required-bison-version` branch - this might need to be revised. I tested that it compiles using bison version 3.5.1 (obtained from `apt` in Ubuntu 20.04)

[Peter Gjøl Jensen (peter-gjoel)]

I assume the bison/flex files should also be purged?

review: Needs Information

[lp:~tapaal-ltl/verifypn/simple-ltl-heuristics]

254. By Nikolaj Jensen Ulrik on 2021-10-26

Removing dangling HeuristicParser.h

[Nikolaj Jensen Ulrik (waefwerf)]

> I assume the bison/flex files should also be purged?

The LTL heuristics parser files should be gone. I didn't remove the other ones (PQLQueryParser.{y,l}) since Jiri thought they might still be useful (if I understood correctly). I did find a dangling file which I just removed

[Peter Gjøl Jensen (peter-gjoel)]

LGTM

review: Approve

[lp:~tapaal-ltl/verifypn/simple-ltl-heuristics]

255. By Nikolaj Jensen Ulrik on 2021-10-27

making the --ltl-heur help string more clear

[Jiri Srba (srba)]

review: Approve

=== modified file 'CMakeLists.txt'
--- CMakeLists.txt	2021-10-17 18:18:35 +0000
+++ CMakeLists.txt	2021-10-27 20:06:36 +0000
@@ -62,7 +62,7 @@
 set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
 
 find_package(FLEX 2.6.4 REQUIRED)
-find_package(BISON 3.7.0 REQUIRED)
+find_package(BISON 3.0.5 REQUIRED)
 
 if (VERIFYPN_GetDependencies)
     # setup for external imports

=== removed file 'include/LTL/SuccessorGeneration/ComposedHeuristic.h'
=== removed file 'include/LTL/SuccessorGeneration/HeuristicParser.h'
=== modified file 'include/LTL/SuccessorGeneration/Heuristics.h'
--- include/LTL/SuccessorGeneration/Heuristics.h	2021-06-22 11:41:45 +0000
+++ include/LTL/SuccessorGeneration/Heuristics.h	2021-10-27 20:06:36 +0000
@@ -21,8 +21,6 @@
 #include "DistanceHeuristic.h"
 #include "RandomHeuristic.h"
 #include "AutomatonHeuristic.h"
-#include "ComposedHeuristic.h"
-#include "WeightedComposedHeuristic.h"
 #include "FireCountHeuristic.h"
 #include "LogFireCountHeuristic.h"
 

=== removed file 'include/LTL/SuccessorGeneration/WeightedComposedHeuristic.h'
=== modified file 'include/PetriEngine/options.h'
--- include/PetriEngine/options.h	2021-08-06 09:43:25 +0000
+++ include/PetriEngine/options.h	2021-10-27 20:06:36 +0000
@@ -43,6 +43,11 @@
     High = 3
 };
 
+enum class LTLHeuristic {
+    Distance,
+    Automaton,
+    FireCount,
+};
 struct options_t {
 //    bool outputtrace = false;
     int kbound = 0;
@@ -83,7 +88,7 @@
     APCompression ltl_compress_aps = APCompression::None;
     LTLPartialOrder ltl_por = LTLPartialOrder::VisibleReach;
     BuchiOptimization buchiOptimization = BuchiOptimization::Low;
-    const char* ltlHeuristic = "aut";
+    LTLHeuristic ltlHeuristic = LTLHeuristic::Automaton;
 
     bool replay_trace = false;
     std::string replay_file;

=== modified file 'src/LTL/LTLMain.cpp'
--- src/LTL/LTLMain.cpp	2021-10-03 09:38:47 +0000
+++ src/LTL/LTLMain.cpp	2021-10-27 20:06:36 +0000
@@ -22,7 +22,7 @@
 
 #include "LTL/SuccessorGeneration/Spoolers.h"
 #include "LTL/SuccessorGeneration/Heuristics.h"
-#include "LTL/SuccessorGeneration/HeuristicParser.h"
+//#include "LTL/SuccessorGeneration/HeuristicParser.h"
 
 #include <utility>
 
@@ -97,12 +97,14 @@
         if (options.strategy != Reachability::Strategy::HEUR && options.strategy != Reachability::Strategy::DEFAULT) {
             return nullptr;
         }
-        auto heur = ParseHeuristic(net, automaton, negated_formula, options.ltlHeuristic);
-        if (heur == nullptr) {
-            std::cerr << "Invalid heuristic specification, terminating.\n";
-            exit(1);
+        switch(options.ltlHeuristic) {
+            case LTLHeuristic::Distance:
+                return std::make_unique<AutomatonHeuristic>(net, automaton);
+            case LTLHeuristic::Automaton:
+                return std::make_unique<DistanceHeuristic>(net, negated_formula);
+            case LTLHeuristic::FireCount:
+                return std::make_unique<LogFireCountHeuristic>(net, 5000);
         }
-        else return heur;
     }
 
     bool LTLMain(const PetriNet *net,

=== modified file 'src/LTL/SuccessorGeneration/CMakeLists.txt'
--- src/LTL/SuccessorGeneration/CMakeLists.txt	2021-08-11 09:06:51 +0000
+++ src/LTL/SuccessorGeneration/CMakeLists.txt	2021-10-27 20:06:36 +0000
@@ -1,12 +1,6 @@
 set(CMAKE_INCLUDE_CURRENT_DIR ON)
 
-flex_target(heur_lexer "${CMAKE_CURRENT_SOURCE_DIR}/HeuristicLexer.l"
-        "${CMAKE_CURRENT_SOURCE_DIR}/HeuristicLexer.lexer.cpp")
-
-bison_target(heur_parser "${CMAKE_CURRENT_SOURCE_DIR}/HeuristicParser.y"
-        "${CMAKE_CURRENT_SOURCE_DIR}/HeuristicParser.parser.cpp")
-
-add_library(LTLSuccessorGeneration ${BISON_heur_parser_OUTPUTS} ${FLEX_heur_lexer_OUTPUTS} ${HEADER_FILES} ResumingSuccessorGenerator.cpp AutomatonHeuristic.cpp)
+add_library(LTLSuccessorGeneration ${HEADER_FILES} ResumingSuccessorGenerator.cpp AutomatonHeuristic.cpp)
 
 target_link_libraries(LTLSuccessorGeneration bddx spot)
 

=== removed file 'src/LTL/SuccessorGeneration/HeuristicLexer.l'
=== removed file 'src/LTL/SuccessorGeneration/HeuristicParser.y'
=== modified file 'src/VerifyPN.cpp'
--- src/VerifyPN.cpp	2021-10-25 14:55:51 +0000
+++ src/VerifyPN.cpp	2021-10-27 20:06:36 +0000
@@ -479,10 +479,17 @@
                 std::cerr << "Missing argument to --ltl-heur\n";
                 return ErrorCode;
             }
-            else {
-                options.ltlHeuristic = argv[i + 1];
+            if (strcmp(argv[i + 1], "aut") == 0) {
+                options.ltlHeuristic = LTLHeuristic::Automaton;
+            } else if (strcmp(argv[i + 1], "dist") == 0) {
+                options.ltlHeuristic = LTLHeuristic::Distance;
+            } else if (strcmp(argv[i + 1], "fire-count") == 0) {
+                options.ltlHeuristic = LTLHeuristic::FireCount;
+            } else {
+                continue;
             }
-            ++i;
+
+           ++i;
         }
         else if (strcmp(argv[i], "-noweak") == 0) {
             options.ltluseweak = false;
@@ -538,9 +545,13 @@
                     "                                                    classic otherwise.\n"
                     "                                       - automaton  apply fully Büchi-guided stubborn set method.\n"
                     "                                       - none       disable stubborn reductions (equivalent to -p).\n"
-                    "  --ltl-heur <spec>                    Select distance metric for LTL heuristic search\n"
-                    "                                       Use --ltl-heur-help to see specification grammar.\n"
-                    "                                       Defaults to 'aut'.\n"
+                    "  --ltl-heur <type>                    Select search heuristic for best-first search in LTL engine\n"
+                    "                                       Defaults to aut"
+                    "                                       - dist           Formula-driven heuristic, guiding toward states that satisfy\n"
+                    "                                                        the atomic propositions mentioned in the LTL formula.\n"
+                    "                                       - aut            Automaton-driven heuristic. Guides search toward states\n"
+                    "                                                        that satisfy progressing formulae in the automaton.\n"
+                    "                                       - fire-count     Prioritises transitions that were fired less often.\n"
                     "  -a, --siphon-trap <timeout>          Siphon-Trap analysis timeout in seconds (default 0)\n"
                     "      --siphon-depth <place count>     Search depth of siphon (default 0, which counts all places)\n"
                     "  -n, --no-statistics                  Do not display any statistics (default is to display it)\n"
@@ -629,22 +640,6 @@
             printf("GNU GPLv3 or later <http://gnu.org/licenses/gpl.html>\n");
             return SuccessCode;
         }
-        else if (strcmp(argv[i], "--ltl-heur-help") == 0) {
-            printf("Heuristics for LTL model checking are specified using the following grammar:\n"
-                   "  heurexp : {'aut' | 'automaton'}\n"
-                   "          | {'dist' | 'distance'}\n"
-                   "          | {'fc' | 'firecount' | 'fire-count'} <threshold>?\n"
-                   "          | '(' heurexp ')'\n"
-                   "          | 'sum' <weight>? heurexp <weight?> heurexp\n"
-                   "          | 'sum' '(' <weight>? heurexp ',' <weight>? heurexp ')'\n"
-                   "Example strings:\n"
-                   "  - aut - use the automaton heuristic for verification.\n"
-                   "  - sum dist fc 1000 - use the sum of distance heuristic and fire count heuristic with threshold 1000.\n"
-                   "Weight for sum and threshold for fire count are optional and integral.\n"
-                   "Sum weights default to 1 (thus plain sum), and default fire count threshold is 5000.\n"
-                   );
-            return SuccessCode;
-        }
         else if (options.modelfile == NULL) {
             options.modelfile = argv[i];
         } else if (options.queryfile == NULL) {