verifypn

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

  1. query_rewrite_fix
  2. Merge into new-trunk
Proposed by Peter Gjøl Jensen
Status: Merged
Approved by: Jiri Srba
Approved revision: 216
Merged at revision: 213
Proposed branch: lp:~verifypn-cpn/verifypn/query_rewrite_fix
Merge into: lp:verifypn
Diff against target: 370 lines (+123/-110)
3 files modified
PetriEngine/PQL/Contexts.h (+4/-2)
PetriEngine/PQL/Expressions.cpp (+91/-107)
PetriEngine/PQL/Expressions.h (+28/-1)
To merge this branch: bzr merge lp:~verifypn-cpn/verifypn/query_rewrite_fix
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Review via email: mp+353797@code.launchpad.net

Commit message

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.

To post a comment you must log in.
Revision history for this message
Jiri Srba (srba) :
review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'PetriEngine/PQL/Contexts.h'
2--- PetriEngine/PQL/Contexts.h 2018-03-09 18:37:07 +0000
3+++ PetriEngine/PQL/Contexts.h 2018-08-27 14:34:51 +0000
4@@ -144,6 +144,8 @@
5 _marking = marking;
6 _net = net;
7 }
8+
9+ EvaluationContext() {};
10
11 const MarkVal* marking() const {
12 return _marking;
13@@ -157,8 +159,8 @@
14 return _net;
15 }
16 private:
17- const MarkVal* _marking;
18- const PetriNet* _net;
19+ const MarkVal* _marking = nullptr;
20+ const PetriNet* _net = nullptr;
21 };
22
23 /** Context for distance computation */
24
25=== modified file 'PetriEngine/PQL/Expressions.cpp'
26--- PetriEngine/PQL/Expressions.cpp 2018-05-12 15:14:12 +0000
27+++ PetriEngine/PQL/Expressions.cpp 2018-08-27 14:34:51 +0000
28@@ -69,8 +69,8 @@
29 }
30 else
31 {
32- if(! ((dynamic_cast<UnfoldedIdentifierExpr*>((*comp)[0].get()) && dynamic_cast<LiteralExpr*>((*comp)[1].get())) ||
33- (dynamic_cast<UnfoldedIdentifierExpr*>((*comp)[1].get()) && dynamic_cast<LiteralExpr*>((*comp)[0].get()))))
34+ if(! ((dynamic_cast<UnfoldedIdentifierExpr*>((*comp)[0].get()) && (*comp)[1]->placeFree()) ||
35+ (dynamic_cast<UnfoldedIdentifierExpr*>((*comp)[1].get()) && (*comp)[0]->placeFree())))
36 {
37 _conds.emplace_back(ptr);
38 return;
39@@ -807,8 +807,7 @@
40 context.marking()[c._place] >= c._lower;
41 if(!res) break;
42 }
43-
44- return _negated xor res ? RTRUE : RFALSE;
45+ return (_negated xor res) ? RTRUE : RFALSE;
46 }
47
48 Condition::Result CompareCondition::evaluate(const EvaluationContext& context) {
49@@ -2486,8 +2485,15 @@
50 auto id = std::make_shared<UnfoldedIdentifierExpr>(c._name, c._place);
51 auto ll = std::make_shared<LiteralExpr>(c._lower);
52 auto lu = std::make_shared<LiteralExpr>(c._upper);
53- if (c._lower == c._upper && !neg) return std::make_shared<EqualCondition>(id, lu);
54- else if(c._lower == c._upper && neg) return std::make_shared<NotEqualCondition>(id, lu);
55+ if(c._lower == c._upper)
56+ {
57+ if(c._lower != 0)
58+ if(neg) return std::make_shared<NotEqualCondition>(id, lu);
59+ else return std::make_shared<EqualCondition>(id, lu);
60+ else
61+ if(neg) return std::make_shared<GreaterThanCondition>(id, lu);
62+ else return std::make_shared<LessThanOrEqualCondition>(id, lu);
63+ }
64 else
65 {
66 if(c._lower != 0 && c._upper != std::numeric_limits<uint32_t>::max())
67@@ -3480,20 +3486,33 @@
68 }, stats, context, nested, negated, initrw);
69 }
70
71+ Condition_ptr pushEqual(CompareCondition* org, bool negated, bool noteq, const EvaluationContext& context)
72+ {
73+ if(org->isTrivial()) return BooleanCondition::getShared(org->evaluate(context) xor negated);
74+ if((*org)[0]->placeFree() && (*org)[0]->evaluate(context) == 0)
75+ {
76+ if(negated == noteq) return std::make_shared<LessThanOrEqualCondition>((*org)[1], std::make_shared<LiteralExpr>(0));
77+ else return std::make_shared<GreaterThanOrEqualCondition>((*org)[1], std::make_shared<LiteralExpr>(1));
78+ }
79+ if((*org)[1]->placeFree() && (*org)[1]->evaluate(context) == 0)
80+ {
81+ if(negated == noteq) return std::make_shared<LessThanOrEqualCondition>((*org)[1], std::make_shared<LiteralExpr>(0));
82+ else return std::make_shared<GreaterThanOrEqualCondition>((*org)[1], std::make_shared<LiteralExpr>(1));
83+ }
84+ if(negated == noteq) return std::make_shared<EqualCondition>((*org)[0], (*org)[1]);
85+ else return std::make_shared<NotEqualCondition>((*org)[0], (*org)[1]);
86+ }
87+
88 Condition_ptr NotEqualCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
89 return initialMarkingRW([&]() -> Condition_ptr {
90- if(isTrivial()) return BooleanCondition::getShared(evaluate(context) xor negated);
91- if(negated) return std::make_shared<EqualCondition>(_expr1, _expr2);
92- else return std::make_shared<NotEqualCondition>(_expr1, _expr2);
93+ return pushEqual(this, negated, true, context);
94 }, stats, context, nested, negated, initrw);
95 }
96
97
98 Condition_ptr EqualCondition::pushNegation(negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw) {
99 return initialMarkingRW([&]() -> Condition_ptr {
100- if(isTrivial()) return BooleanCondition::getShared(evaluate(context) xor negated);
101- if(negated) return std::make_shared<NotEqualCondition>(_expr1, _expr2);
102- else return std::make_shared<EqualCondition>(_expr1, _expr2);
103+ return pushEqual(this, negated, false, context);
104 }, stats, context, nested, negated, initrw);
105 }
106
107@@ -3909,135 +3928,83 @@
108 exit(ErrorCode);
109 }
110 auto il = _constraints.begin();
111- for(auto& c : other._constraints)
112+ for(auto c : other._constraints)
113 {
114+ if(neg)
115+ c.invert();
116+
117+ if(c._upper == std::numeric_limits<uint32_t>::max() && c._lower == 0)
118+ {
119+ continue;
120+ }
121+ else if (c._upper != std::numeric_limits<uint32_t>::max() && c._lower != 0 && neg)
122+ {
123+ std::cerr << "MERGE OF CONJUNCT AND DISJUNCT NOT ALLOWED" << std::endl;
124+ assert(false);
125+ exit(ErrorCode);
126+ }
127+
128 il = std::lower_bound(_constraints.begin(), _constraints.end(), c);
129- cons_t c2;
130- if(neg)
131- {
132- if(c._upper == 0)
133- {
134- c2._lower = 1;
135- }
136- else if (c._upper == std::numeric_limits<uint32_t>::max())
137- {
138- c2._upper = c._lower + (other._negated ? -1 : 1);
139- }
140- else if(c._lower == 0)
141- {
142- c2._lower = c._upper + (other._negated ? 1 : -1);
143- }
144- else
145- {
146- std::cerr << "MERGE OF CONJUNCT AND DISJUNCT NOT ALLOWED" << std::endl;
147- assert(false);
148- exit(ErrorCode);
149- }
150- c2._place = c._place;
151- assert(c2._lower <= c2._upper);
152- }
153- else
154- {
155- c2 = c;
156- }
157-
158- if(il == _constraints.end() || il->_place != c2._place)
159- {
160- c2._name = c._name;
161- il = _constraints.insert(il, c2);
162- }
163- else
164- {
165- il->_lower = std::max(il->_lower, c2._lower);
166- il->_upper = std::min(il->_upper, c2._upper);
167+ if(il == _constraints.end() || il->_place != c._place)
168+ {
169+ il = _constraints.insert(il, c);
170+ }
171+ else
172+ {
173+ il->_lower = std::max(il->_lower, c._lower);
174+ il->_upper = std::min(il->_upper, c._upper);
175 }
176 }
177 }
178
179 void CompareConjunction::merge(const std::vector<Condition_ptr>& conditions, bool negated)
180 {
181-
182 for(auto& c : conditions)
183 {
184 auto cmp = dynamic_cast<CompareCondition*>(c.get());
185 assert(cmp);
186 auto id = dynamic_cast<UnfoldedIdentifierExpr*>((*cmp)[0].get());
187- LiteralExpr* lit = nullptr;
188+ uint32_t val;
189 bool inverted = false;
190+ EvaluationContext context;
191 if(!id)
192 {
193 id = dynamic_cast<UnfoldedIdentifierExpr*>((*cmp)[1].get());
194- lit = dynamic_cast<LiteralExpr*>((*cmp)[0].get());
195+ val = (*cmp)[0]->evaluate(context);
196 inverted = true;
197 }
198 else
199 {
200- lit = dynamic_cast<LiteralExpr*>((*cmp)[1].get());
201+ val = (*cmp)[1]->evaluate(context);
202 }
203- assert(lit);
204 assert(id);
205- uint32_t val = lit->value();
206 cons_t next;
207 next._place = id->offset();
208- auto lb = std::lower_bound(std::begin(_constraints), std::end(_constraints), next);
209- if(lb == std::end(_constraints))
210- {
211- next._name = id->name();
212- lb = _constraints.insert(lb, next);
213- }
214- else
215- {
216- assert(id->name().compare(lb->_name) == 0);
217- }
218
219 if(dynamic_cast<LessThanOrEqualCondition*>(c.get()))
220- {
221- if(!negated)
222- if(inverted) lb->_lower = std::max(lb->_lower, val);
223- else lb->_upper = std::min(lb->_upper, val);
224- else
225- if(!inverted) lb->_lower = std::max(lb->_lower, val+1);
226- else lb->_upper = std::min(lb->_upper, val-1);
227- }
228+ if(inverted) next._lower = val;
229+ else next._upper = val;
230+ else if(dynamic_cast<LessThanCondition*>(c.get()))
231+ if(inverted) next._lower = val+1;
232+ else next._upper = val-1;
233 else if(dynamic_cast<GreaterThanOrEqualCondition*>(c.get()))
234- {
235- if(!negated)
236- if(!inverted) lb->_lower = std::max(lb->_lower, val);
237- else lb->_upper = std::min(lb->_upper, val);
238- else
239- if(inverted) lb->_lower = std::max(lb->_lower, val+1);
240- else lb->_upper = std::min(lb->_upper, val-1);
241- }
242- else if(dynamic_cast<LessThanCondition*>(c.get()))
243- {
244- if(!negated)
245- if(inverted) lb->_lower = std::max(lb->_lower, val+1);
246- else lb->_upper = std::min(lb->_upper, val-1);
247- else
248- if(!inverted) lb->_lower = std::max(lb->_lower, val);
249- else lb->_upper = std::min(lb->_upper, val);
250-
251- }
252+ if(inverted) next._upper = val;
253+ else next._lower = val;
254 else if(dynamic_cast<GreaterThanCondition*>(c.get()))
255- {
256- if(!negated)
257- if(!inverted) lb->_lower = std::max(lb->_lower, val+1);
258- else lb->_upper = std::min(lb->_upper, val-1);
259- else
260- if(inverted) lb->_lower = std::max(lb->_lower, val);
261- else lb->_upper = std::min(lb->_upper, val);
262- }
263+ if(inverted) next._upper = val-1;
264+ else next._lower = val+1;
265 else if(dynamic_cast<EqualCondition*>(c.get()))
266 {
267 assert(!negated);
268- lb->_lower = std::max(lb->_lower, val);
269- lb->_upper = std::min(lb->_upper, val);
270+ next._lower = val;
271+ next._upper = val;
272 }
273 else if(dynamic_cast<NotEqualCondition*>(c.get()))
274 {
275 assert(negated);
276- lb->_lower = std::max(lb->_lower, val);
277- lb->_upper = std::min(lb->_upper, val);
278+ next._lower = val;
279+ next._upper = val;
280+ negated = false; // we already handled negation here!
281 }
282 else
283 {
284@@ -4045,14 +4012,31 @@
285 assert(false);
286 exit(ErrorCode);
287 }
288+ if(negated)
289+ next.invert();
290+
291+ auto lb = std::lower_bound(std::begin(_constraints), std::end(_constraints), next);
292+ if(lb == std::end(_constraints) || lb->_place != next._place)
293+ {
294+ next._name = id->name();
295+ _constraints.insert(lb, next);
296+ }
297+ else
298+ {
299+ assert(id->name().compare(lb->_name) == 0);
300+ lb->intersect(next);
301+ }
302 }
303 }
304
305 void CommutativeExpr::init(std::vector<Expr_ptr>&& exprs)
306 {
307 for (auto& e : exprs) {
308- if (auto lit = dynamic_pointer_cast<PQL::LiteralExpr>(e))
309- _constant = apply(_constant, lit->value());
310+ if (e->placeFree())
311+ {
312+ EvaluationContext c;
313+ _constant = apply(_constant, e->evaluate(c));
314+ }
315 else if (auto id = dynamic_pointer_cast<PQL::UnfoldedIdentifierExpr>(e)) {
316 _ids.emplace_back(id->offset(), id->name());
317 }
318
319=== modified file 'PetriEngine/PQL/Expressions.h'
320--- PetriEngine/PQL/Expressions.h 2018-04-29 07:58:51 +0000
321+++ PetriEngine/PQL/Expressions.h 2018-08-27 14:34:51 +0000
322@@ -791,6 +791,33 @@
323 {
324 return _place < other._place;
325 }
326+
327+ void invert()
328+ {
329+ if(_lower == 0 && _upper == std::numeric_limits<uint32_t>::max())
330+ return;
331+ assert(_lower == 0 || _upper == std::numeric_limits<uint32_t>::max());
332+ if(_lower == 0)
333+ {
334+ _lower = _upper + 1;
335+ _upper = std::numeric_limits<uint32_t>::max();
336+ }
337+ else if(_upper == std::numeric_limits<uint32_t>::max())
338+ {
339+ _upper = _lower - 1;
340+ _lower = 0;
341+ }
342+ else
343+ {
344+ assert(false);
345+ }
346+ }
347+
348+ void intersect(const cons_t& other)
349+ {
350+ _lower = std::max(_lower, other._lower);
351+ _upper = std::min(_upper, other._upper);
352+ }
353 };
354
355 CompareConjunction(bool negated = false)
356@@ -884,13 +911,13 @@
357 }
358 bool containsNext() const override { return false; }
359 bool nestedDeadlock() const override { return false; }
360+ bool isTrivial() const;
361 protected:
362 uint32_t _distance(DistanceContext& c,
363 std::function<uint32_t(uint32_t, uint32_t, bool)> d) const
364 {
365 return d(_expr1->evaluate(c), _expr2->evaluate(c), c.negated());
366 }
367- bool isTrivial() const;
368 private:
369 virtual bool apply(int v1, int v2) const = 0;
370 virtual std::string op() const = 0;

Subscribers

People subscribed via source and target branches