← Back to branch summary

~tapaal-red/verifypn/rule-l

« back to all changes in this revision

Viewing changes to src/PetriEngine/PQL/Expressions.cpp

  • Committer: Peter G. Jensen
  • Date: 2021-05-19 13:20:33 UTC
  • mto: This revision was merged to the branch mainline in revision 238.
  • Revision ID: root@petergjoel.dk-20210519132033-ijp113dqjfv2281v
fixing issue with LTL

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/PetriEngine/PQL/Expressions.cpp
3547
3547
            }, stats, context, nested, negated, initrw);
3548
3548
        }
3549
3549
 
 
3550
        /*LTL negation push*/
3550
3551
        Condition_ptr
3551
3552
        UntilCondition::pushNegation(negstat_t &stats, const EvaluationContext &context, bool nested, bool negated,
3552
3553
                                     bool initrw) {
3623
3624
 
3624
3625
        Condition_ptr ACondition::pushNegation(negstat_t &stats, const EvaluationContext &context, bool nested, bool negated,
3625
3626
                                               bool initrw) {
3626
 
            return ECondition(std::make_shared<NotCondition>(_cond)).pushNegation(stats, context, nested, !negated, initrw);
 
3627
            return ECondition(std::make_shared<NotCondition>(_cond))
 
3628
                .pushNegation(stats, context, nested, !negated, initrw);
3627
3629
        }
3628
3630
 
3629
3631
 
3630
3632
        Condition_ptr ECondition::pushNegation(negstat_t &stats, const EvaluationContext &context, bool nested, bool negated,
3631
3633
                                               bool initrw) {
3632
 
            auto _sub = _cond->pushNegation(stats, context, nested, !negated, initrw);
3633
 
            return negated ? (Condition_ptr)std::make_shared<ACondition>(_sub) : (Condition_ptr)std::make_shared<ECondition>(_sub);
 
3634
            // we forward the negated flag, we flip the outer quantifier later!
 
3635
            auto _sub = _cond->pushNegation(stats, context, nested, negated, initrw);
 
3636
            if(negated) return std::make_shared<ACondition>(_sub);
 
3637
            else        return std::make_shared<ECondition>(_sub);
3634
3638
        }
3635
3639
 
3636
3640
        Condition_ptr GCondition::pushNegation(negstat_t &stats, const EvaluationContext &context, bool nested, bool negated,
3638
3642
            return FCondition(std::make_shared<NotCondition>(_cond)).pushNegation(stats, context, nested, !negated, initrw);
3639
3643
        }
3640
3644
 
 
3645
        /*Boolean connectives */
3641
3646
        Condition_ptr pushAnd(const std::vector<Condition_ptr>& _conds, negstat_t& stats, const EvaluationContext& context, bool nested, bool negate_children, bool initrw)
3642
3647
        {
3643
3648
            std::vector<Condition_ptr> nef, other;