Merge lp:~tapaal-ltl/verifypn/ruleI.5 into lp:~tapaal-ltl/verifypn/ltl-model-checker

[Simon Virenfeldt]

Implements the new structural reduction rule K which is a weaker version of rule I tailored to LTL reduction.

[Nikolaj Jensen Ulrik (waefwerf)]

review: Approve

[lp:~tapaal-ltl/verifypn/ruleI.5]

252. By Simon Virenfeldt on 2021-02-19

Merge lp:~tapaal-ltl/verifypn/ruleI.5@253

=== modified file 'include/PetriEngine/Reducer.h'
--- include/PetriEngine/Reducer.h	2020-11-26 10:36:20 +0000
+++ include/PetriEngine/Reducer.h	2021-02-18 12:06:25 +0000
@@ -110,7 +110,8 @@
                 << "Applications of rule G: " << _ruleG << "\n"
                 << "Applications of rule H: " << _ruleH << "\n"
                 << "Applications of rule I: " << _ruleI << "\n"
-                << "Applications of rule J: " << _ruleJ << std::endl;
+                << "Applications of rule J: " << _ruleJ << "\n"
+                << "Applications of rule K: " << _ruleK << std::endl;
         }
 
         void postFire(std::ostream&, const std::string& transition);
@@ -120,7 +121,7 @@
     private:
         size_t _removedTransitions = 0;
         size_t _removedPlaces= 0;
-        size_t _ruleA = 0, _ruleB = 0, _ruleC = 0, _ruleD = 0, _ruleE = 0, _ruleF = 0, _ruleG = 0, _ruleH = 0, _ruleI = 0, _ruleJ = 0;
+        size_t _ruleA = 0, _ruleB = 0, _ruleC = 0, _ruleD = 0, _ruleE = 0, _ruleF = 0, _ruleG = 0, _ruleH = 0, _ruleI = 0, _ruleJ = 0, _ruleK = 0;
         PetriNetBuilder* parent = nullptr;
         bool reconstructTrace = false;
         std::chrono::high_resolution_clock::time_point _timer;
@@ -137,7 +138,11 @@
         bool ReducebyRuleG(uint32_t* placeInQuery, bool remove_loops, bool remove_consumers);
         bool ReducebyRuleH(uint32_t* placeInQuery);
         bool ReducebyRuleJ(uint32_t* placeInQuery);
-        
+        bool ReducebyRuleK(uint32_t* placeInQuery, bool remove_consumers);
+
+        std::optional<std::pair<std::vector<bool>, std::vector<bool>>>relevant(const uint32_t* placeInQuery, bool remove_consumers);
+        bool remove_irrelevant(const uint32_t* placeInQuery, const std::vector<bool> &tseen, const std::vector<bool> &pseen);
+
         std::string getTransitionName(uint32_t transition);
         std::string getPlaceName(uint32_t place);
         

=== modified file 'src/PetriEngine/Reducer.cpp'
--- src/PetriEngine/Reducer.cpp	2020-12-04 11:14:38 +0000
+++ src/PetriEngine/Reducer.cpp	2021-02-18 12:06:25 +0000
@@ -903,131 +903,24 @@
 
             if(skipplace)
                 skipPlace(p);
-            
+
         }
         assert(consistent());
         return continueReductions;
     }
-   
+
     bool Reducer::ReducebyRuleI(uint32_t* placeInQuery, bool remove_loops, bool remove_consumers) {
         bool reduced = false;
         if(remove_loops)
         {
-            std::vector<uint32_t> wtrans;
-            std::vector<bool> tseen(parent->numberOfTransitions(), false);
-
-            for(uint32_t p = 0; p < parent->numberOfPlaces(); ++p)
-            {
-                if(hasTimedout()) return false;
-                if(placeInQuery[p] > 0)
-                {
-                    const Place& place = parent->_places[p];
-                    for(auto t : place.consumers)
-                    {
-                        if(!tseen[t])
-                        {
-                            wtrans.push_back(t);
-                            tseen[t] = true;
-                        }
-                    }
-                    for(auto t : place.producers)
-                    {
-                        if(!tseen[t])
-                        {
-                            wtrans.push_back(t);
-                            tseen[t] = true;
-                        }
-                    }
-                }
-            }
-
-            std::vector<bool> pseen(parent->numberOfPlaces(), false);        
-            while(!wtrans.empty())
-            {
-                if(hasTimedout()) return false;
-                auto t = wtrans.back();
-                wtrans.pop_back();
-                const Transition& trans = parent->_transitions[t];
-                for(const Arc& arc : trans.pre)
-                {
-                    const Place& place = parent->_places[arc.place];
-                    if(arc.inhib)
-                    {
-                        for(auto pt : place.consumers)
-                        {
-                            if(!tseen[pt])
-                            {
-                                Transition& trans = parent->_transitions[pt];
-                                auto it = trans.post.begin();
-                                for(; it != trans.post.end(); ++it)
-                                    if(it->place >= arc.place) break;
-                                if(it != trans.post.end() && it->place == arc.place)
-                                {
-                                    auto it2 = trans.pre.begin();
-                                    for(; it2 != trans.pre.end(); ++it2)
-                                        if(it2->place >= arc.place || it2->inhib) break;
-                                    if(it->weight <= it2->weight) continue;
-                                }
-                                tseen[pt] = true;
-                                wtrans.push_back(pt);                                    
-                            }
-                        }                        
-                    }
-                    else
-                    {
-                        for(auto pt : place.producers)
-                        {
-                            if(!tseen[pt])
-                            {                                    
-                                Transition& trans = parent->_transitions[pt];
-                                auto it = trans.pre.begin();
-                                for(; it != trans.pre.end(); ++it)
-                                    if(it->place >= arc.place) break;
-
-                                if(it != trans.pre.end() && it->place == arc.place && !it->inhib)
-                                {
-                                    auto it2 = trans.post.begin();
-                                    for(; it2 != trans.post.end(); ++it2)
-                                        if(it2->place >= arc.place) break;
-                                    if(it->weight >= it2->weight) continue;
-                                }
-
-                                tseen[pt] = true;
-                                wtrans.push_back(pt);
-                            }
-                        }
-
-                        for(auto pt : place.consumers)
-                        {
-                            if(!tseen[pt] && (!remove_consumers || placeInQuery[arc.place] > 0))
-                            {
-                                tseen[pt] = true;
-                                wtrans.push_back(pt);                                    
-                            }
-                        }
-                    }
-                    pseen[arc.place] = true;
-                }
-            }
-
-            for(size_t t = 0; t < parent->numberOfTransitions(); ++t)
-            {
-                if(!tseen[t] && !parent->_transitions[t].skip)
-                {
-                    skipTransition(t);
-                    reduced = true;
-                }
-            }
-
-            for(size_t p = 0; p < parent->numberOfPlaces(); ++p)
-            {
-                if(!pseen[p] && !parent->_places[p].skip && placeInQuery[p] == 0)
-                {
-                    assert(placeInQuery[p] == 0);
-                    skipPlace(p);
-                    reduced = true;
-                }
-            }
+
+            auto result = relevant(placeInQuery, remove_consumers);
+            if (!result) {
+                return false;
+            }
+            auto[tseen, pseen] = result.value();
+
+            reduced |= remove_irrelevant(placeInQuery, tseen, pseen);
             
             if(reduced)
                 ++_ruleI;
@@ -1565,6 +1458,153 @@
         }
         return continueReductions;
     }
+
+    bool Reducer::ReducebyRuleK(uint32_t *placeInQuery, bool remove_consumers) {
+        bool reduced = false;
+        auto opt = relevant(placeInQuery, remove_consumers);
+        if (!opt)
+            return false;
+        auto[tseen, pseen] = opt.value();
+        for (std::size_t p = 0; p < parent->numberOfPlaces(); ++p) {
+            if (placeInQuery[p] != 0)
+                pseen[p] = true;
+        }
+
+        for (std::size_t t = 0; t < parent->numberOfTransitions(); ++t) {
+            auto transition = parent->_transitions[t];
+            if (!tseen[t] && !transition.skip && !transition.inhib && transition.pre.size() == 1 &&
+                transition.post.size() == 1
+                && transition.pre[0].place == transition.post[0].place) {
+                auto p = transition.pre[0].place;
+                if (!pseen[p] && !parent->_places[p].inhib) {
+                    if (parent->initialMarking[p] >= transition.pre[0].weight){
+                        //Mark the initially marked self loop as relevant.
+                        tseen[t] = true;
+                        pseen[p] = true;
+                        reduced |= remove_irrelevant(placeInQuery, tseen, pseen);
+                        _ruleK++;
+                        return reduced;
+                    }
+                    if (transition.pre[0].weight == 1){
+                        for (auto t2 : parent->_places[p].consumers) {
+                            auto transition2 = parent->_transitions[t2];
+                            if (t != t2 && !tseen[t2] && !transition2.skip) {
+                                skipTransition(t2);
+                                reduced = true;
+                                _ruleK++;
+                            }
+                        }
+                    }
+                }
+            }
+        }
+        return reduced;
+    }
+
+    std::optional<std::pair<std::vector<bool>, std::vector<bool>>>
+    Reducer::relevant(const uint32_t *placeInQuery, bool remove_consumers) {
+        std::vector<uint32_t> wtrans;
+        std::vector<bool> tseen(parent->numberOfTransitions(), false);
+        for (uint32_t p = 0; p < parent->numberOfPlaces(); ++p) {
+            if (hasTimedout()) return std::nullopt;
+            if (placeInQuery[p] > 0) {
+                const Place &place = parent->_places[p];
+                for (auto t : place.consumers) {
+                    if (!tseen[t]) {
+                        wtrans.push_back(t);
+                        tseen[t] = true;
+                    }
+                }
+                for (auto t : place.producers) {
+                    if (!tseen[t]) {
+                        wtrans.push_back(t);
+                        tseen[t] = true;
+                    }
+                }
+            }
+        }
+        std::vector<bool> pseen(parent->numberOfPlaces(), false);
+
+        while (!wtrans.empty()) {
+            if (hasTimedout()) return std::nullopt;
+            auto t = wtrans.back();
+            wtrans.pop_back();
+            const Transition &trans = parent->_transitions[t];
+            for (const Arc &arc : trans.pre) {
+                const Place &place = parent->_places[arc.place];
+                if (arc.inhib) {
+                    for (auto pt : place.consumers) {
+                        if (!tseen[pt]) {
+                            Transition &trans = parent->_transitions[pt];
+                            auto it = trans.post.begin();
+                            for (; it != trans.post.end(); ++it)
+                                if (it->place >= arc.place) break;
+                            if (it != trans.post.end() && it->place == arc.place) {
+                                auto it2 = trans.pre.begin();
+                                for (; it2 != trans.pre.end(); ++it2)
+                                    if (it2->place >= arc.place || it2->inhib) break;
+                                if (it->weight <= it2->weight) continue;
+                            }
+                            tseen[pt] = true;
+                            wtrans.push_back(pt);
+                        }
+                    }
+                } else {
+                    for (auto pt : place.producers) {
+                        if (!tseen[pt]) {
+                            Transition &trans = parent->_transitions[pt];
+                            auto it = trans.pre.begin();
+                            for (; it != trans.pre.end(); ++it)
+                                if (it->place >= arc.place) break;
+
+                            if (it != trans.pre.end() && it->place == arc.place && !it->inhib) {
+                                auto it2 = trans.post.begin();
+                                for (; it2 != trans.post.end(); ++it2)
+                                    if (it2->place >= arc.place) break;
+                                if (it->weight >= it2->weight) continue;
+                            }
+
+                            tseen[pt] = true;
+                            wtrans.push_back(pt);
+                        }
+                    }
+
+                    for (auto pt : place.consumers) {
+                        if (!tseen[pt] && (!remove_consumers || placeInQuery[arc.place] > 0)) {
+                            tseen[pt] = true;
+                            wtrans.push_back(pt);
+                        }
+                    }
+                }
+                pseen[arc.place] = true;
+            }
+        }
+        return std::make_optional(std::pair(tseen, pseen));
+    }
+
+    bool Reducer::remove_irrelevant(const uint32_t* placeInQuery, const std::vector<bool> &tseen, const std::vector<bool> &pseen) {
+        bool reduced = false;
+        for(size_t t = 0; t < parent->numberOfTransitions(); ++t)
+        {
+            if(!tseen[t] && !parent->_transitions[t].skip)
+            {
+                skipTransition(t);
+                reduced = true;
+            }
+        }
+
+        for(size_t p = 0; p < parent->numberOfPlaces(); ++p)
+        {
+            if(!pseen[p] && !parent->_places[p].skip && placeInQuery[p] == 0)
+            {
+                assert(placeInQuery[p] == 0);
+                skipPlace(p);
+                reduced = true;
+            }
+        }
+        return reduced;
+    }
+
     void Reducer::Reduce(QueryPlaceAnalysisContext& context, int enablereduction, bool reconstructTrace, int timeout, bool remove_loops, bool remove_consumers, bool next_safe, std::vector<uint32_t>& reduction) {
 
         this->_timeout = timeout;
@@ -1603,6 +1643,7 @@
                             if(!remove_loops) 
                                 while(ReducebyRuleI(context.getQueryPlaceCount(), remove_loops, remove_consumers)) changed = true;
                             while(ReducebyRuleD(context.getQueryPlaceCount())) changed = true;
+                            changed |= ReducebyRuleK(context.getQueryPlaceCount(), remove_consumers);
                         }
                     } while(changed && !hasTimedout());
                     if(!next_safe) 
@@ -1622,7 +1663,7 @@
         }
         else
         {
-            const char* rnames = "ABCDEFGHIJ";
+            const char* rnames = "ABCDEFGHIJK";
             for(int i = reduction.size() - 1; i >= 0; --i)
             {
                 if(next_safe)
@@ -1683,6 +1724,9 @@
                         case 9:
                             while(ReducebyRuleJ(context.getQueryPlaceCount())) changed = true;
                             break;
+                        case 10:
+                            if (ReducebyRuleK(context.getQueryPlaceCount(), remove_consumers)) changed = true;
+                            break;
                     }
 #ifndef NDEBUG
                     auto end = std::chrono::high_resolution_clock::now();

=== modified file 'src/VerifyPN.cpp'
--- src/VerifyPN.cpp	2021-02-04 11:16:09 +0000
+++ src/VerifyPN.cpp	2021-02-18 12:06:25 +0000
@@ -204,7 +204,7 @@
                 for(auto& qn : q)
                 {
                     int32_t n;
-                    if(sscanf(qn.c_str(), "%d", &n) != 1 || n < 0 || n > 9)
+                    if(sscanf(qn.c_str(), "%d", &n) != 1 || n < 0 || n > 10)
                     {
                         std::cerr << "Error in reduction rule choice : " << qn << std::endl;
                         return ErrorCode;