Merge lp:~verifypn-cpn/verifypn/eq-push-fix into lp:~verifypn-cpn/verifypn/MCC19

Proposed by Peter Gjøl Jensen on 2019-04-17
Status: Needs review
Proposed branch: lp:~verifypn-cpn/verifypn/eq-push-fix
Merge into: lp:~verifypn-cpn/verifypn/MCC19
Diff against target: 26 lines (+7/-9)
1 file modified
PetriEngine/PQL/Expressions.cpp (+7/-9)
To merge this branch: bzr merge lp:~verifypn-cpn/verifypn/eq-push-fix
Reviewer Review Type Date Requested Status
Jiri Srba 2019-04-17 Pending
Review via email: mp+366157@code.launchpad.net

Commit message

Fixes rewrite of X=Y when either X or Y is either 0 or 1 into <= or >= constraints.
Bug was triggered as cases were not handled symmetrically (i.e. an indexing error)

To post a comment you must log in.

Unmerged revisions

239. By Peter Gjøl Jensen on 2019-04-17

fixed error in re-write of equality into simpler form

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'PetriEngine/PQL/Expressions.cpp'
2--- PetriEngine/PQL/Expressions.cpp 2019-02-11 21:18:10 +0000
3+++ PetriEngine/PQL/Expressions.cpp 2019-04-17 08:26:19 +0000
4@@ -3443,15 +3443,13 @@
5 Condition_ptr pushEqual(CompareCondition* org, bool negated, bool noteq, const EvaluationContext& context)
6 {
7 if(org->isTrivial()) return BooleanCondition::getShared(org->evaluate(context) xor negated);
8- if((*org)[0]->placeFree() && (*org)[0]->evaluate(context) == 0)
9- {
10- if(negated == noteq) return std::make_shared<LessThanOrEqualCondition>((*org)[1], std::make_shared<LiteralExpr>(0));
11- else return std::make_shared<GreaterThanOrEqualCondition>((*org)[1], std::make_shared<LiteralExpr>(1));
12- }
13- if((*org)[1]->placeFree() && (*org)[1]->evaluate(context) == 0)
14- {
15- if(negated == noteq) return std::make_shared<LessThanOrEqualCondition>((*org)[1], std::make_shared<LiteralExpr>(0));
16- else return std::make_shared<GreaterThanOrEqualCondition>((*org)[1], std::make_shared<LiteralExpr>(1));
17+ for(auto i : {0,1})
18+ {
19+ if((*org)[i]->placeFree() && (*org)[i]->evaluate(context) == 0)
20+ {
21+ if(negated == noteq) return std::make_shared<LessThanOrEqualCondition>((*org)[(i + 1) % 2], std::make_shared<LiteralExpr>(0));
22+ else return std::make_shared<GreaterThanOrEqualCondition>((*org)[(i + 1) % 2], std::make_shared<LiteralExpr>(1));
23+ }
24 }
25 if(negated == noteq) return std::make_shared<EqualCondition>((*org)[0], (*org)[1]);
26 else return std::make_shared<NotEqualCondition>((*org)[0], (*org)[1]);

Subscribers

People subscribed via source and target branches

to all changes: