Merge lp:~tapaal-ltl/verifypn/ltl-neg-fix into lp:verifypn

[Peter Gjøl Jensen]

fixes issue with pushNegation that adds extra negation to outermost quantifier in each call.

fixes issue with pushNegation that adds extra negation to outermost quantifier in each call.

[Jiri Srba (srba)]

Correctness recovered for P/T and CPN nets in LTL category - tested againt oracle.

review: Approve

=== modified file 'src/PetriEngine/PQL/Expressions.cpp'
--- src/PetriEngine/PQL/Expressions.cpp	2021-04-14 11:51:52 +0000
+++ src/PetriEngine/PQL/Expressions.cpp	2021-05-19 14:15:34 +0000
@@ -3547,6 +3547,7 @@
             }, stats, context, nested, negated, initrw);
         }
 
+        /*LTL negation push*/
         Condition_ptr
         UntilCondition::pushNegation(negstat_t &stats, const EvaluationContext &context, bool nested, bool negated,
                                      bool initrw) {
@@ -3623,14 +3624,17 @@
 
         Condition_ptr ACondition::pushNegation(negstat_t &stats, const EvaluationContext &context, bool nested, bool negated,
                                                bool initrw) {
-            return ECondition(std::make_shared<NotCondition>(_cond)).pushNegation(stats, context, nested, !negated, initrw);
+            return ECondition(std::make_shared<NotCondition>(_cond))
+                .pushNegation(stats, context, nested, !negated, initrw);
         }
 
 
         Condition_ptr ECondition::pushNegation(negstat_t &stats, const EvaluationContext &context, bool nested, bool negated,
                                                bool initrw) {
-            auto _sub = _cond->pushNegation(stats, context, nested, !negated, initrw);
-            return negated ? (Condition_ptr)std::make_shared<ACondition>(_sub) : (Condition_ptr)std::make_shared<ECondition>(_sub);
+            // we forward the negated flag, we flip the outer quantifier later!
+            auto _sub = _cond->pushNegation(stats, context, nested, negated, initrw);
+            if(negated) return std::make_shared<ACondition>(_sub);
+            else        return std::make_shared<ECondition>(_sub);
         }
 
         Condition_ptr GCondition::pushNegation(negstat_t &stats, const EvaluationContext &context, bool nested, bool negated,
@@ -3638,6 +3642,7 @@
             return FCondition(std::make_shared<NotCondition>(_cond)).pushNegation(stats, context, nested, !negated, initrw);
         }
 
+        /*Boolean connectives */
         Condition_ptr pushAnd(const std::vector<Condition_ptr>& _conds, negstat_t& stats, const EvaluationContext& context, bool nested, bool negate_children, bool initrw)
         {
             std::vector<Condition_ptr> nef, other;