Disallow R on CTL when using -r 3 (TAPAAL#41)

* Disallow rule R on LTL in -r 3 * Disallow rule R on CTL in -r 3
TAPAAL-Developers · Feb 22, 2022 · b4cf73c · b4cf73c
1 parent cc77f57
commit b4cf73c
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 3 deletions.
diff --git a/include/PetriEngine/Reducer.h b/include/PetriEngine/Reducer.h
@@ -88,7 +88,7 @@ namespace PetriEngine {
         Reducer(PetriNetBuilder*);
         ~Reducer();
         void Print(QueryPlaceAnalysisContext& context); // prints the net, just for debugging
-        void Reduce(QueryPlaceAnalysisContext& context, int enablereduction, bool reconstructTrace, int timeout, bool remove_loops, bool remove_consumers, bool all_ltl, bool next_safe, std::vector<uint32_t>& reductions, std::vector<uint32_t>& secondaryreductions);
+        void Reduce(QueryPlaceAnalysisContext& context, int enablereduction, bool reconstructTrace, int timeout, bool remove_loops, bool all_reach, bool all_ltl, bool next_safe, std::vector<uint32_t>& reductions, std::vector<uint32_t>& secondaryreductions);
 
         size_t numberOfSkippedTransitions() const {
             return _skippedTransitions.size();

diff --git a/src/PetriEngine/PetriNetBuilder.cpp b/src/PetriEngine/PetriNetBuilder.cpp
@@ -479,7 +479,7 @@ namespace PetriEngine {
             {
                 PetriEngine::PQL::analyze(queries[i], placecontext);
                 all_reach &= (results[i] != Reachability::ResultPrinter::CTL && results[i] != Reachability::ResultPrinter::LTL);
-                all_ltl &= results[i] == Reachability::ResultPrinter::LTL;
+                all_ltl &= results[i] != Reachability::ResultPrinter::CTL;
                 remove_loops &= !PetriEngine::PQL::isLoopSensitive(queries[i]);
                 // There is a deadlock somewhere, if it is not alone, we cannot reduce.
                 // this has similar problems as nested next.

diff --git a/src/PetriEngine/Reducer.cpp b/src/PetriEngine/Reducer.cpp
@@ -2229,14 +2229,15 @@ else if (inhibArcs == 0)
             "T-server_process_7"
     };
 
-    void Reducer::Reduce(QueryPlaceAnalysisContext& context, int enablereduction, bool reconstructTrace, int timeout, bool remove_loops, bool remove_consumers, bool all_ltl, bool next_safe, std::vector<uint32_t>& reduction, std::vector<uint32_t>& secondaryreductions) {
+    void Reducer::Reduce(QueryPlaceAnalysisContext& context, int enablereduction, bool reconstructTrace, int timeout, bool remove_loops, bool all_reach, bool all_ltl, bool next_safe, std::vector<uint32_t>& reduction, std::vector<uint32_t>& secondaryreductions) {
 
         this->_timeout = timeout;
         _timer = std::chrono::high_resolution_clock::now();
         assert(consistent());
         this->reconstructTrace = reconstructTrace;
         if(reconstructTrace && enablereduction >= 1 && enablereduction <= 2)
             std::cout << "Rule H disabled when a trace is requested." << std::endl;
+        bool remove_consumers = all_reach;
         if (enablereduction == 2) { // for k-boundedness checking only rules A, D and H are applicable
             bool changed = true;
             while (changed && !hasTimedout()) {
@@ -2309,6 +2310,10 @@ else if (inhibArcs == 0)
                     std::cerr << "Skipping Rule" << rnames[reduction[i]] << " as proposition is loop sensitive" << std::endl;
                     reduction.erase(reduction.begin() + i);
                 }
+                if (!(all_ltl || all_reach) && reduction[i] == 17) {
+                    std::cerr << "Skipping Rule" << rnames[reduction[i]] << " as proposition is not LTL" << std::endl;
+                    reduction.erase(reduction.begin() + i);
+                }
             }
             bool changed = true;
             uint8_t lastChangeRound = 0;