Merge lp:~tapaal-ltl/verifypn/rule-D-fix into lp:verifypn

[Simon Virenfeldt]

Fix logic error in structural reduction Rule D for LTL and CTL.

Adds a check to the structural reduction rule D if we are in LTL or CTL such that if the weights are not equal and the pre or post places are mentioned in the query we will not remove the transition.

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

Looks good to me.

review: Approve

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

Passes regression on MCC2020 models (changes answer on GlobalResAllocation-COL-09-CTLCardinality-00 on colored nets as intended)

review: Approve

[Jiri Srba (srba)]

review: Approve

=== modified file 'include/PetriEngine/Reducer.h'
--- include/PetriEngine/Reducer.h	2021-02-12 12:09:19 +0000
+++ include/PetriEngine/Reducer.h	2021-06-22 09:27:59 +0000
@@ -14,6 +14,7 @@
 #include "NetStructures.h"
 
 #include <vector>
+#include <optional>
 
 namespace PetriEngine {
 
@@ -131,7 +132,7 @@
         bool ReducebyRuleA(uint32_t* placeInQuery);
         bool ReducebyRuleB(uint32_t* placeInQuery, bool remove_deadlocks, bool remove_consumers);
         bool ReducebyRuleC(uint32_t* placeInQuery);
-        bool ReducebyRuleD(uint32_t* placeInQuery);
+        bool ReducebyRuleD(uint32_t *placeInQuery, bool remove_consumers);
         bool ReducebyRuleE(uint32_t* placeInQuery);
         bool ReducebyRuleI(uint32_t* placeInQuery, bool remove_loops, bool remove_consumers);
         bool ReducebyRuleF(uint32_t* placeInQuery);

=== modified file 'src/PetriEngine/Reducer.cpp'
--- src/PetriEngine/Reducer.cpp	2021-03-06 10:56:46 +0000
+++ src/PetriEngine/Reducer.cpp	2021-06-22 09:27:59 +0000
@@ -711,7 +711,7 @@
         return continueReductions;
     }
 
-    bool Reducer::ReducebyRuleD(uint32_t* placeInQuery) {
+    bool Reducer::ReducebyRuleD(uint32_t *placeInQuery, bool remove_consumers) {
         // Rule D - two transitions with the same pre and post and same inhibitor arcs 
         // This does not alter the trace.
         bool continueReductions = false;
@@ -742,6 +742,8 @@
             Transition& tout = getTransition(touter);
             if (tout.skip) continue;
 
+
+
             // D2. No inhibitors
             if (tout.inhib) continue;
 
@@ -799,6 +801,27 @@
                     if (ok == 2) break;
                     else if (ok == 1) continue;
 
+
+                    // If we are in CTL or LTL and the weights are not the same an additional requirement is needed.
+                    // In this case we cannot reduce if the pre or postset of the transition is in the query.
+                    if (!remove_consumers && mult != 1){
+                        bool has_place_in_query = false;
+                        for (const auto &arc : tout.pre) {
+                            if (placeInQuery[arc.place]) {
+                                has_place_in_query = true;
+                                break;
+                            }
+                        }
+                        if (has_place_in_query) break;
+                        for (const auto &arc : tout.post) {
+                            if (placeInQuery[arc.place]) {
+                                has_place_in_query = true;
+                                break;
+                            }
+                        }
+                        if (has_place_in_query) break;
+                    }
+
                     // D3. Presets must match
                     for (int i = trans1.pre.size() - 1; i >= 0; --i) {
                         Arc& arc = trans1.pre[i];
@@ -1620,7 +1643,7 @@
                 if(!next_safe)
                 {
                     while(ReducebyRuleA(context.getQueryPlaceCount())) changed = true;
-                    while(ReducebyRuleD(context.getQueryPlaceCount())) changed = true;
+                    while(ReducebyRuleD(context.getQueryPlaceCount(), remove_consumers)) changed = true;
                     while(ReducebyRuleH(context.getQueryPlaceCount())) changed = true;
                 }
             }
@@ -1642,7 +1665,7 @@
                             while(ReducebyRuleG(context.getQueryPlaceCount(), remove_loops, remove_consumers)) changed = true;
                             if(!remove_loops) 
                                 while(ReducebyRuleI(context.getQueryPlaceCount(), remove_loops, remove_consumers)) changed = true;
-                            while(ReducebyRuleD(context.getQueryPlaceCount())) changed = true;
+                            while(ReducebyRuleD(context.getQueryPlaceCount(), remove_consumers)) changed = true;
                             //changed |= ReducebyRuleK(context.getQueryPlaceCount(), remove_consumers); //Rule disabled as correctness has not been proved. Experiments indicate that it is not correct for CTL.
                         }
                     } while(changed && !hasTimedout());
@@ -1704,7 +1727,7 @@
                             while(ReducebyRuleC(context.getQueryPlaceCount())) changed = true;
                             break;
                         case 3:
-                            while(ReducebyRuleD(context.getQueryPlaceCount())) changed = true;
+                            while(ReducebyRuleD(context.getQueryPlaceCount(), remove_consumers)) changed = true;
                             break;              
                         case 4:
                             while(ReducebyRuleE(context.getQueryPlaceCount())) changed = true;