Merge lp:~tapaal-ltl/verifypn/weak-tarjan2 into lp:~tapaal-ltl/verifypn/ltl-model-checker

[Simon Virenfeldt]

Implements weak tarjan and is_reachability for LTL formulas

[Nikolaj Jensen Ulrik (waefwerf)]

review: Approve

=== modified file 'include/LTL/LTL_algorithm/ModelChecker.h'
--- include/LTL/LTL_algorithm/ModelChecker.h	2020-11-11 12:50:38 +0000
+++ include/LTL/LTL_algorithm/ModelChecker.h	2020-12-10 12:09:22 +0000
@@ -12,7 +12,7 @@
 namespace LTL {
     class ModelChecker {
     public:
-        ModelChecker(const PetriEngine::PetriNet& net, PetriEngine::PQL::Condition_ptr);
+        ModelChecker(const PetriEngine::PetriNet& net, PetriEngine::PQL::Condition_ptr, const bool shortcircuitweak);
         virtual bool isSatisfied() = 0;
         
         virtual ~ModelChecker() = default;
@@ -23,6 +23,8 @@
         PetriEngine::PQL::Condition_ptr formula;
 
         size_t _discovered = 0;
+        const bool shortcircuitweak;
+        bool is_weak = false;
     };
 }
 

=== modified file 'include/LTL/LTL_algorithm/NestedDepthFirstSearch.h'
--- include/LTL/LTL_algorithm/NestedDepthFirstSearch.h	2020-11-18 12:49:59 +0000
+++ include/LTL/LTL_algorithm/NestedDepthFirstSearch.h	2020-12-10 12:09:22 +0000
@@ -20,8 +20,8 @@
     class NestedDepthFirstSearch : public ModelChecker {
     public:
         NestedDepthFirstSearch(const PetriNet &net, PetriEngine::PQL::Condition_ptr ptr, const bool shortcircuitweak)
-                : ModelChecker(net, ptr), factory{net, successorGenerator->initial_buchi_state()},
-                states(net, 0, (int)net.numberOfPlaces() + 1), shortcircuitweak(shortcircuitweak) {}
+                : ModelChecker(net, ptr, shortcircuitweak), factory{net, successorGenerator->initial_buchi_state()},
+                states(net, 0, (int)net.numberOfPlaces() + 1) {}
 
         bool isSatisfied() override;
 
@@ -40,8 +40,6 @@
 
         State *seed;
         bool violation = false;
-        bool is_weak = false;
-        const bool shortcircuitweak;
 
         void dfs();
 

=== modified file 'include/LTL/LTL_algorithm/TarjanModelChecker.h'
--- include/LTL/LTL_algorithm/TarjanModelChecker.h	2020-12-10 10:06:53 +0000
+++ include/LTL/LTL_algorithm/TarjanModelChecker.h	2020-12-10 12:09:22 +0000
@@ -21,8 +21,8 @@
     template <bool SaveTrace>
     class TarjanModelChecker : public ModelChecker {
     public:
-        TarjanModelChecker(const PetriEngine::PetriNet &net, const Condition_ptr &cond)
-                : ModelChecker(net, cond), factory(net, successorGenerator->initial_buchi_state()),
+        TarjanModelChecker(const PetriEngine::PetriNet &net, const Condition_ptr &cond, const bool shortcircuitweak)
+                : ModelChecker(net, cond, shortcircuitweak), factory(net, successorGenerator->initial_buchi_state()),
                   seen(net, 0, (int) net.numberOfPlaces() + 1) {
             chash.fill(std::numeric_limits<idx_t>::max());
         }
@@ -84,6 +84,8 @@
         void update(idx_t to);
 
         bool nexttrans(State &state, State& parent, DEntry &delem);
+
+        void popCStack();
     };
 extern template class TarjanModelChecker<true>;
 extern template class TarjanModelChecker<false>;

=== modified file 'include/PetriEngine/PQL/Expressions.h'
--- include/PetriEngine/PQL/Expressions.h	2020-12-04 11:14:38 +0000
+++ include/PetriEngine/PQL/Expressions.h	2020-12-10 12:09:22 +0000
@@ -439,10 +439,7 @@
 
             Retval simplify(SimplificationContext& context) const override;
 
-            bool isReachability(uint32_t depth) const override {
-                // TODO implement
-                assert(false); std::cerr << "TODO implement" << std::endl; exit(0);
-            }
+            bool isReachability(uint32_t depth) const override;
             Condition_ptr prepareForReachability(bool negated) const override {
                 // TODO implement
                 assert(false); std::cerr << "TODO implement" << std::endl; exit(0);
@@ -475,10 +472,7 @@
             Result evaluate(const EvaluationContext& context) override;
 
             Retval simplify(SimplificationContext& context) const override;
-            bool isReachability(uint32_t depth) const override {
-                // TODO implement
-                assert(false); std::cerr << "TODO implement" << std::endl; exit(0);
-            }
+            bool isReachability(uint32_t depth) const override;
             Condition_ptr prepareForReachability(bool negated) const override {
                 // TODO implement
                 assert(false); std::cerr << "TODO implement" << std::endl; exit(0);
@@ -506,10 +500,9 @@
           Result evaluate(const EvaluationContext &context) override;
 
           bool isReachability(uint32_t depth) const override {
-              // TODO implement
-              assert(false);
-              std::cerr << "TODO implement" << std::endl;
-              exit(0);
+              // This could potentially be a reachability formula if the parent is an A.
+              // This case is however already handled by ACondition.
+              return false;
           }
 
           Condition_ptr prepareForReachability(bool negated) const override {
@@ -557,10 +550,11 @@
             Result evaluate(const EvaluationContext& context) override;
 
             Retval simplify(SimplificationContext& context) const override;
-            bool isReachability(uint32_t depth) const override {
-                // TODO implement
-                assert(false); std::cerr << "TODO implement" << std::endl; exit(0);
-            }
+          bool isReachability(uint32_t depth) const override {
+              // This could potentially be a reachability formula if the parent is an E.
+              // This case is however already handled by ECondition.
+              return false;
+          }
             Condition_ptr prepareForReachability(bool negated) const override {
                 // TODO implement
                 assert(false); std::cerr << "TODO implement" << std::endl; exit(0);
@@ -587,8 +581,7 @@
             using SimpleQuantifierCondition::SimpleQuantifierCondition;
 
             bool isReachability(uint32_t depth) const override {
-                // TODO implement
-                assert(false); std::cerr << "TODO implement" << std::endl; exit(0);
+                return false;
             }
             Condition_ptr prepareForReachability(bool negated) const override {
                 // TODO implement

=== modified file 'src/LTL/LTL_algorithm/ModelChecker.cpp'
--- src/LTL/LTL_algorithm/ModelChecker.cpp	2020-10-16 12:11:46 +0000
+++ src/LTL/LTL_algorithm/ModelChecker.cpp	2020-12-10 12:09:22 +0000
@@ -7,8 +7,8 @@
 #include <utility>
 
 namespace LTL {
-    ModelChecker::ModelChecker(const PetriEngine::PetriNet& net, PetriEngine::PQL::Condition_ptr condition)
-        : net(net), formula(condition)
+    ModelChecker::ModelChecker(const PetriEngine::PetriNet& net, PetriEngine::PQL::Condition_ptr condition, const bool shortcircuitweak)
+        : net(net), formula(condition), shortcircuitweak(shortcircuitweak)
     {
 
         successorGenerator = std::make_unique<ProductSuccessorGenerator>(net, condition);

=== modified file 'src/LTL/LTL_algorithm/TarjanModelChecker.cpp'
--- src/LTL/LTL_algorithm/TarjanModelChecker.cpp	2020-12-10 10:06:53 +0000
+++ src/LTL/LTL_algorithm/TarjanModelChecker.cpp	2020-12-10 12:09:22 +0000
@@ -21,6 +21,8 @@
 
     template<bool SaveTrace>
     bool TarjanModelChecker<SaveTrace>::isSatisfied() {
+        is_weak = successorGenerator->is_weak();
+        std::cerr << "Is weak: " << is_weak << std::endl;
         std::vector<State> initial_states;
         successorGenerator->makeInitialState(initial_states);
         State working = factory.newState();
@@ -128,10 +130,14 @@
         dstack.pop();
         if (cstack[p].lowlink == p) {
             while (cstack.size() > p) {
-                auto h = hash(cstack.back().stateid);
-                store.insert(cstack.back().stateid);
-                chash[h] = cstack.back().next;
-                cstack.pop_back();
+                popCStack();
+            }
+        } else if (is_weak) {
+            State state = factory.newState();
+            seen.decode(state, cstack[p].stateid);
+            if(!successorGenerator->isAccepting(state)){
+                popCStack();
+                weakskip = true;
             }
         }
         if (!astack.empty() && p == astack.top()) {
@@ -143,6 +149,14 @@
     }
 
     template<bool SaveTrace>
+    void TarjanModelChecker<SaveTrace>::popCStack(){
+        auto h = hash(cstack.back().stateid);
+        store.insert(cstack.back().stateid);
+        chash[h] = cstack.back().next;
+        cstack.pop_back();
+    }
+
+    template<bool SaveTrace>
     void TarjanModelChecker<SaveTrace>::update(idx_t to) {
         const auto from = dstack.top().pos;
         if (cstack[to].lowlink <= cstack[from].lowlink) {

=== modified file 'src/LTLMain.cpp'
--- src/LTLMain.cpp	2020-12-04 11:14:38 +0000
+++ src/LTLMain.cpp	2020-12-10 12:09:22 +0000
@@ -739,9 +739,9 @@
                     break;
                 case LTL::Algorithm::Tarjan:
                     if (options.trace)
-                        modelChecker = std::make_unique<LTL::TarjanModelChecker<true>>(*net, negated_formula);
+                        modelChecker = std::make_unique<LTL::TarjanModelChecker<true>>(*net, negated_formula, true);
                     else
-                        modelChecker = std::make_unique<LTL::TarjanModelChecker<false>>(*net, negated_formula);
+                        modelChecker = std::make_unique<LTL::TarjanModelChecker<false>>(*net, negated_formula, true);
                     break;
             }
             satisfied = negate_answer ^ modelChecker->isSatisfied();

=== modified file 'src/PetriEngine/PQL/Expressions.cpp'
--- src/PetriEngine/PQL/Expressions.cpp	2020-11-19 11:20:22 +0000
+++ src/PetriEngine/PQL/Expressions.cpp	2020-12-10 12:09:22 +0000
@@ -2994,6 +2994,28 @@
         bool AFCondition::isReachability(uint32_t depth) const {
             return false;
         }
+
+        bool ECondition::isReachability(uint32_t depth) const {
+            if (depth != 0) {
+                return false;
+            }
+
+            if (auto cond = dynamic_cast<FCondition*>(_cond.get())) {
+                // EF is a reachability formula so skip checking the F.
+                return cond[0].isReachability(depth + 1);
+            }
+            return _cond->isReachability(depth + 1);
+        }
+
+        bool ACondition::isReachability(uint32_t depth) const {
+            if (depth != 0) {
+                return false;
+            }
+            if (auto cond = dynamic_cast<GCondition*>(_cond.get())) {
+                return cond[0].isReachability(depth + 1);
+            }
+            return _cond->isReachability(depth + 1);
+        }
         
         bool UntilCondition::isReachability(uint32_t depth) const {
             return false;