Merge lp:~verifypn-cpn/verifypn/query_rewrite_fix into lp:verifypn

[Peter Gjøl Jensen]

Fixes wrong answer in CTLFireability from MCC2018 using
-x 2 ./SmallOperatingSystem-PT-MT8192DC4096/model.pnml ./SmallOperatingSystem-PT-MT8192DC4096/CTLFireability.xml

Is consistent on 2017 models and queries.

[Jiri Srba (srba)]

review: Approve

=== modified file 'PetriEngine/PQL/Contexts.h'
--- PetriEngine/PQL/Contexts.h	2018-03-09 18:37:07 +0000
+++ PetriEngine/PQL/Contexts.h	2018-08-27 14:34:51 +0000
@@ -144,6 +144,8 @@
                 _marking = marking;
                 _net = net;
             }
+            
+            EvaluationContext() {};
 
             const MarkVal* marking() const {
                 return _marking;
@@ -157,8 +159,8 @@
                 return _net;
             }
         private:
-            const MarkVal* _marking;
-            const PetriNet* _net;
+            const MarkVal* _marking = nullptr;
+            const PetriNet* _net = nullptr;
         };
 
         /** Context for distance computation */
 
=== modified file 'PetriEngine/PQL/Expressions.cpp'
--- PetriEngine/PQL/Expressions.cpp	2018-05-12 15:14:12 +0000
+++ PetriEngine/PQL/Expressions.cpp	2018-08-27 14:34:51 +0000
@@ -69,8 +69,8 @@
                 }
                 else
                 {
-                    if(! ((dynamic_cast<UnfoldedIdentifierExpr*>((*comp)[0].get()) && dynamic_cast<LiteralExpr*>((*comp)[1].get())) ||
-                          (dynamic_cast<UnfoldedIdentifierExpr*>((*comp)[1].get()) && dynamic_cast<LiteralExpr*>((*comp)[0].get()))))
+                    if(! ((dynamic_cast<UnfoldedIdentifierExpr*>((*comp)[0].get()) && (*comp)[1]->placeFree()) ||
+                          (dynamic_cast<UnfoldedIdentifierExpr*>((*comp)[1].get()) && (*comp)[0]->placeFree())))
                     {
                         _conds.emplace_back(ptr);
                         return;
@@ -807,8 +807,7 @@
                              context.marking()[c._place] >= c._lower;
                 if(!res) break;
             }
-            
-            return _negated xor res ? RTRUE : RFALSE;
+            return (_negated xor res) ? RTRUE : RFALSE;
         }
         
         Condition::Result CompareCondition::evaluate(const EvaluationContext& context) {
@@ -2486,8 +2485,15 @@
                     auto id = std::make_shared<UnfoldedIdentifierExpr>(c._name, c._place);
                     auto ll = std::make_shared<LiteralExpr>(c._lower);
                     auto lu = std::make_shared<LiteralExpr>(c._upper);
-                    if     (c._lower == c._upper && !neg) return std::make_shared<EqualCondition>(id, lu);
-                    else if(c._lower == c._upper &&  neg) return std::make_shared<NotEqualCondition>(id, lu);
+                    if(c._lower == c._upper)
+                    {
+                        if(c._lower != 0)
+                            if(neg) return std::make_shared<NotEqualCondition>(id, lu);
+                            else    return std::make_shared<EqualCondition>(id, lu);
+                        else
+                            if(neg) return std::make_shared<GreaterThanCondition>(id, lu);
+                            else    return std::make_shared<LessThanOrEqualCondition>(id, lu);
+                    }
                     else
                     {
                         if(c._lower != 0 && c._upper != std::numeric_limits<uint32_t>::max())
@@ -3480,20 +3486,33 @@
             }, stats, context, nested, negated, initrw);
         }
                 
+        Condition_ptr pushEqual(CompareCondition* org, bool negated, bool noteq, const EvaluationContext& context)
+        {
+            if(org->isTrivial()) return BooleanCondition::getShared(org->evaluate(context) xor negated);
+            if((*org)[0]->placeFree() && (*org)[0]->evaluate(context) == 0)
+            {
+                if(negated == noteq) return std::make_shared<LessThanOrEqualCondition>((*org)[1], std::make_shared<LiteralExpr>(0));
+                else                 return std::make_shared<GreaterThanOrEqualCondition>((*org)[1], std::make_shared<LiteralExpr>(1));
+            }
+            if((*org)[1]->placeFree() && (*org)[1]->evaluate(context) == 0)
+            {
+                if(negated == noteq) return std::make_shared<LessThanOrEqualCondition>((*org)[1], std::make_shared<LiteralExpr>(0));
+                else                 return std::make_shared<GreaterThanOrEqualCondition>((*org)[1], std::make_shared<LiteralExpr>(1));                
+            }
+            if(negated == noteq) return std::make_shared<EqualCondition>((*org)[0], (*org)[1]);
+            else                 return std::make_shared<NotEqualCondition>((*org)[0], (*org)[1]);            
+        }
+        
         Condition_ptr NotEqualCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
             return initialMarkingRW([&]() -> Condition_ptr {
-            if(isTrivial()) return BooleanCondition::getShared(evaluate(context) xor negated);
-            if(negated) return std::make_shared<EqualCondition>(_expr1, _expr2);
-            else        return std::make_shared<NotEqualCondition>(_expr1, _expr2);
+                return pushEqual(this, negated, true, context);
             }, stats, context, nested, negated, initrw);
         }
 
         
         Condition_ptr EqualCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
             return initialMarkingRW([&]() -> Condition_ptr {
-            if(isTrivial()) return BooleanCondition::getShared(evaluate(context) xor negated);
-            if(negated) return std::make_shared<NotEqualCondition>(_expr1, _expr2);
-            else        return std::make_shared<EqualCondition>(_expr1, _expr2);
+                return pushEqual(this, negated, false, context);
             }, stats, context, nested, negated, initrw);
         }
                 
@@ -3909,135 +3928,83 @@
                 exit(ErrorCode);
             }
             auto il = _constraints.begin();
-            for(auto& c : other._constraints)
+            for(auto c : other._constraints)
             {
+                if(neg)
+                    c.invert();
+                                
+                if(c._upper == std::numeric_limits<uint32_t>::max() && c._lower == 0)
+                {
+                    continue;
+                }
+                else if (c._upper != std::numeric_limits<uint32_t>::max() && c._lower != 0 && neg)
+                {
+                    std::cerr << "MERGE OF CONJUNCT AND DISJUNCT NOT ALLOWED" << std::endl;
+                    assert(false);
+                    exit(ErrorCode);
+                }
+                
                 il = std::lower_bound(_constraints.begin(), _constraints.end(), c);
-                cons_t c2;
-                if(neg)
-                {
-                    if(c._upper == 0)
-                    {
-                        c2._lower = 1;
-                    }
-                    else if (c._upper == std::numeric_limits<uint32_t>::max())
-                    {
-                        c2._upper = c._lower + (other._negated ? -1 :  1);
-                    }
-                    else if(c._lower == 0)
-                    {
-                        c2._lower = c._upper + (other._negated ?  1 : -1);
-                    }
-                    else
-                    {
-                        std::cerr << "MERGE OF CONJUNCT AND DISJUNCT NOT ALLOWED" << std::endl;
-                        assert(false);
-                        exit(ErrorCode);
-                    }
-                    c2._place = c._place;
-                    assert(c2._lower <= c2._upper);
-                }
-                else
-                {
-                    c2 = c;
-                }
-                            
-                if(il == _constraints.end() || il->_place != c2._place)
-                {
-                    c2._name = c._name;
-                    il = _constraints.insert(il, c2);
-                }
-                else
-                {
-                    il->_lower = std::max(il->_lower, c2._lower);
-                    il->_upper = std::min(il->_upper, c2._upper);
+                if(il == _constraints.end() || il->_place != c._place)
+                {
+                    il = _constraints.insert(il, c);
+                }
+                else
+                {
+                    il->_lower = std::max(il->_lower, c._lower);
+                    il->_upper = std::min(il->_upper, c._upper);
                 }
             }
         }
         
         void CompareConjunction::merge(const std::vector<Condition_ptr>& conditions, bool negated)
         {
-
             for(auto& c : conditions)
             {
                 auto cmp = dynamic_cast<CompareCondition*>(c.get());
                 assert(cmp);
                 auto id = dynamic_cast<UnfoldedIdentifierExpr*>((*cmp)[0].get());
-                LiteralExpr* lit = nullptr;
+                uint32_t val;
                 bool inverted = false;
+                EvaluationContext context;
                 if(!id)
                 {
                     id = dynamic_cast<UnfoldedIdentifierExpr*>((*cmp)[1].get());
-                    lit = dynamic_cast<LiteralExpr*>((*cmp)[0].get());
+                    val = (*cmp)[0]->evaluate(context);
                     inverted = true;
                 }
                 else
                 {
-                    lit = dynamic_cast<LiteralExpr*>((*cmp)[1].get());                
+                    val = (*cmp)[1]->evaluate(context);
                 }
-                assert(lit);
                 assert(id);
-                uint32_t val = lit->value();
                 cons_t next;
                 next._place = id->offset();
-                auto lb = std::lower_bound(std::begin(_constraints), std::end(_constraints), next);
-                if(lb == std::end(_constraints))
-                {
-                    next._name = id->name();
-                    lb = _constraints.insert(lb, next);
-                }  
-                else
-                {
-                    assert(id->name().compare(lb->_name) == 0);
-                }
 
                 if(dynamic_cast<LessThanOrEqualCondition*>(c.get()))
-                {
-                    if(!negated)
-                        if(inverted) lb->_lower = std::max(lb->_lower, val);
-                        else         lb->_upper = std::min(lb->_upper, val);
-                    else
-                        if(!inverted) lb->_lower = std::max(lb->_lower, val+1);
-                        else          lb->_upper = std::min(lb->_upper, val-1);                        
-                }
+                    if(inverted) next._lower = val;
+                    else         next._upper = val;
+                else if(dynamic_cast<LessThanCondition*>(c.get()))
+                    if(inverted) next._lower = val+1;
+                    else         next._upper = val-1;
                 else if(dynamic_cast<GreaterThanOrEqualCondition*>(c.get()))
-                {
-                    if(!negated)
-                        if(!inverted) lb->_lower = std::max(lb->_lower, val);
-                        else          lb->_upper = std::min(lb->_upper, val);
-                    else
-                        if(inverted) lb->_lower = std::max(lb->_lower, val+1);
-                        else         lb->_upper = std::min(lb->_upper, val-1);                        
-                }
-                else if(dynamic_cast<LessThanCondition*>(c.get()))
-                {
-                    if(!negated)
-                        if(inverted) lb->_lower = std::max(lb->_lower, val+1);
-                        else         lb->_upper = std::min(lb->_upper, val-1);
-                    else
-                        if(!inverted) lb->_lower = std::max(lb->_lower, val);
-                        else          lb->_upper = std::min(lb->_upper, val);
-                        
-                }
+                    if(inverted) next._upper = val;
+                    else         next._lower = val;
                 else if(dynamic_cast<GreaterThanCondition*>(c.get()))
-                {
-                    if(!negated)
-                        if(!inverted) lb->_lower = std::max(lb->_lower, val+1);
-                        else          lb->_upper = std::min(lb->_upper, val-1);
-                    else
-                        if(inverted) lb->_lower = std::max(lb->_lower, val);
-                        else         lb->_upper = std::min(lb->_upper, val);                       
-                }
+                    if(inverted) next._upper = val-1;
+                    else         next._lower = val+1;
                 else if(dynamic_cast<EqualCondition*>(c.get()))
                 {
                     assert(!negated);
-                    lb->_lower = std::max(lb->_lower, val);
-                    lb->_upper = std::min(lb->_upper, val);
+                    next._lower = val;
+                    next._upper = val;
                 }
                 else if(dynamic_cast<NotEqualCondition*>(c.get()))
                 {
                     assert(negated);
-                    lb->_lower = std::max(lb->_lower, val);
-                    lb->_upper = std::min(lb->_upper, val);
+                    next._lower = val;
+                    next._upper = val;
+                    negated = false; // we already handled negation here!
                 }
                 else
                 {
@@ -4045,14 +4012,31 @@
                     assert(false);
                     exit(ErrorCode);
                 }
+                if(negated)
+                    next.invert();
+                
+                auto lb = std::lower_bound(std::begin(_constraints), std::end(_constraints), next);
+                if(lb == std::end(_constraints) || lb->_place != next._place)
+                {
+                    next._name = id->name();
+                    _constraints.insert(lb, next);
+                }  
+                else
+                {
+                    assert(id->name().compare(lb->_name) == 0);
+                    lb->intersect(next);
+                }
             }            
         }
        
         void CommutativeExpr::init(std::vector<Expr_ptr>&& exprs)
         {
             for (auto& e : exprs) {
-                if (auto lit = dynamic_pointer_cast<PQL::LiteralExpr>(e))
-                    _constant = apply(_constant, lit->value());
+                if (e->placeFree())
+                {
+                    EvaluationContext c;
+                    _constant = apply(_constant, e->evaluate(c));
+                }
                 else if (auto id = dynamic_pointer_cast<PQL::UnfoldedIdentifierExpr>(e)) {
                     _ids.emplace_back(id->offset(), id->name());
                 } 
 
=== modified file 'PetriEngine/PQL/Expressions.h'
--- PetriEngine/PQL/Expressions.h	2018-04-29 07:58:51 +0000
+++ PetriEngine/PQL/Expressions.h	2018-08-27 14:34:51 +0000
@@ -791,6 +791,33 @@
                 {
                     return _place < other._place;
                 }
+                
+                void invert()
+                {
+                    if(_lower == 0 && _upper == std::numeric_limits<uint32_t>::max())
+                        return;
+                    assert(_lower == 0 || _upper == std::numeric_limits<uint32_t>::max());
+                    if(_lower == 0)
+                    {
+                        _lower = _upper + 1;
+                        _upper = std::numeric_limits<uint32_t>::max();
+                    }
+                    else if(_upper == std::numeric_limits<uint32_t>::max())
+                    {
+                        _upper = _lower - 1;
+                        _lower = 0;
+                    }
+                    else
+                    {
+                        assert(false);
+                    }
+                }
+                
+                void intersect(const cons_t& other)
+                {
+                    _lower = std::max(_lower, other._lower);
+                    _upper = std::min(_upper, other._upper);
+                }
             };
 
             CompareConjunction(bool negated = false) 
@@ -884,13 +911,13 @@
             }
             bool containsNext() const override { return false; }
             bool nestedDeadlock() const override { return false; }
+            bool isTrivial() const;
         protected:
             uint32_t _distance(DistanceContext& c, 
                     std::function<uint32_t(uint32_t, uint32_t, bool)> d) const
             {
                 return d(_expr1->evaluate(c), _expr2->evaluate(c), c.negated());
             }
-            bool isTrivial() const;
         private:
             virtual bool apply(int v1, int v2) const = 0;
             virtual std::string op() const = 0;