verifypn

Merge lp:~verifypn-stub/verifypn/dl-structural-bug into lp:verifypn

  1. dl-structural-bug
  2. Merge into new-trunk
Proposed by Jiri Srba
Status: Merged
Approved by: Jiri Srba
Approved revision: 205
Merged at revision: 204
Proposed branch: lp:~verifypn-stub/verifypn/dl-structural-bug
Merge into: lp:verifypn
Diff against target: 160 lines (+35/-2)
4 files modified
PetriEngine/PQL/Expressions.cpp (+16/-0)
PetriEngine/PQL/Expressions.h (+14/-1)
PetriEngine/PQL/PQL.h (+1/-0)
PetriEngine/PetriNetBuilder.cpp (+4/-1)
To merge this branch: bzr merge lp:~verifypn-stub/verifypn/dl-structural-bug
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Review via email: mp+344852@code.launchpad.net

Commit message

Makes sure that structural reductions are not used when deadlock proposition is in conjunction or disjunction with other predicates. Fixes bug #1750629.

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

Fixes the bug but needs a special fix for 2.2 version.

review: Approve

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 2018-04-17 12:13:30 +0000
3+++ PetriEngine/PQL/Expressions.cpp 2018-04-30 15:54:05 +0000
4@@ -4046,6 +4046,22 @@
5 init(std::move(exprs));
6 }
7
8+ bool LogicalCondition::nestedDeadlock() const {
9+ for(auto& c : _conds)
10+ {
11+ if(c->getQuantifier() == PQL::DEADLOCK ||
12+ c->nestedDeadlock() ||
13+ (c->getQuantifier() == PQL::NEG &&
14+ (*static_cast<NotCondition*>(c.get()))[0]->getQuantifier() == PQL::DEADLOCK
15+ ))
16+ {
17+ return true;
18+ }
19+ }
20+ return false;
21+ }
22+
23+
24 } // PQL
25 } // PetriEngine
26
27
28=== modified file 'PetriEngine/PQL/Expressions.h'
29--- PetriEngine/PQL/Expressions.h 2018-03-29 19:20:35 +0000
30+++ PetriEngine/PQL/Expressions.h 2018-04-30 15:54:05 +0000
31@@ -337,6 +337,7 @@
32 const Condition_ptr& operator[](size_t i) const { return _cond; };
33 virtual bool isTemporal() const override { return _temporal;}
34 bool containsNext() const override { return _cond->containsNext(); }
35+ bool nestedDeadlock() const override { return _cond->nestedDeadlock(); }
36 #ifdef ENABLE_TAR
37 virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
38 #endif
39@@ -375,6 +376,7 @@
40 void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
41 virtual const Condition_ptr& operator[] (size_t i) const override { return _cond;}
42 virtual bool containsNext() const override { return _cond->containsNext(); }
43+ bool nestedDeadlock() const override { return _cond->nestedDeadlock(); }
44 #ifdef ENABLE_TAR
45 virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const
46 {
47@@ -525,6 +527,7 @@
48 Path getPath() const override
49 { return Path::U; }
50 bool containsNext() const override { return _cond1->containsNext() || _cond2->containsNext(); }
51+ bool nestedDeadlock() const override { return _cond1->nestedDeadlock() || _cond2->nestedDeadlock(); }
52 private:
53 virtual std::string op() const = 0;
54
55@@ -605,6 +608,8 @@
56 { return _compiled->formulaSize(); }
57 bool containsNext() const override
58 { return false; }
59+ bool nestedDeadlock() const override
60+ { return false; }
61 #ifdef ENABLE_TAR
62 z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const override
63 {
64@@ -704,6 +709,8 @@
65 bool singular() const { return _conds.size() == 1; }
66 bool containsNext() const override
67 { return std::any_of(begin(), end(), [](auto& a){return a->containsNext();}); }
68+ bool nestedDeadlock() const override;
69+
70 protected:
71 LogicalCondition() {};
72 Retval simplifyOr(SimplificationContext& context) const;
73@@ -838,6 +845,7 @@
74 _constraints[0]._upper == std::numeric_limits<uint32_t>::max());
75 };
76 bool containsNext() const override { return false;}
77+ bool nestedDeadlock() const override { return false; }
78 #ifdef ENABLE_TAR
79 virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
80 #endif
81@@ -875,6 +883,7 @@
82 else return _expr2;
83 }
84 bool containsNext() const override { return false; }
85+ bool nestedDeadlock() const override { return false; }
86 protected:
87 uint32_t _distance(DistanceContext& c,
88 std::function<uint32_t(uint32_t, uint32_t, bool)> d) const
89@@ -1053,6 +1062,7 @@
90 Path getPath() const override { return Path::pError; }
91 CTLType getQueryType() const override { return CTLType::EVAL; }
92 bool containsNext() const override { return false; }
93+ bool nestedDeadlock() const override { return false; }
94 #ifdef ENABLE_TAR
95 virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const
96 {
97@@ -1087,10 +1097,11 @@
98 void toBinary(std::ostream&) const override;
99 void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
100 static Condition_ptr DEADLOCK;
101- Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
102+ Quantifier getQuantifier() const override { return Quantifier::DEADLOCK; }
103 Path getPath() const override { return Path::pError; }
104 CTLType getQueryType() const override { return CTLType::EVAL; }
105 bool containsNext() const override { return false; }
106+ bool nestedDeadlock() const override { return false; }
107 #ifdef ENABLE_TAR
108 virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
109 #endif
110@@ -1140,6 +1151,7 @@
111 Path getPath() const override { return Path::pError; }
112 CTLType getQueryType() const override { return CTLType::EVAL; }
113 bool containsNext() const override { return false; }
114+ bool nestedDeadlock() const override { return false; }
115 #ifdef ENABLE_TAR
116 virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const
117 { return _compiled->encodeSat(net, context, uses, incremented); }
118@@ -1192,6 +1204,7 @@
119 Path getPath() const override { return Path::pError; }
120 CTLType getQueryType() const override { return CTLType::EVAL; }
121 bool containsNext() const override { return false; }
122+ bool nestedDeadlock() const override { return false; }
123 size_t bounds() const { return _bound; }
124 #ifdef ENABLE_TAR
125 virtual z3::expr encodeSat(const PetriNet& net, z3::context& context, std::vector<int32_t>& uses, std::vector<bool>& incremented) const;
126
127=== modified file 'PetriEngine/PQL/PQL.h'
128--- PetriEngine/PQL/PQL.h 2018-04-17 12:13:30 +0000
129+++ PetriEngine/PQL/PQL.h 2018-04-30 15:54:05 +0000
130@@ -283,6 +283,7 @@
131 static std::shared_ptr<Condition>
132 initialMarkingRW(std::function<std::shared_ptr<Condition> ()> func, negstat_t& stats, const EvaluationContext& context, bool nested, bool negated, bool initrw);
133 virtual bool containsNext() const = 0;
134+ virtual bool nestedDeadlock() const = 0;
135 protected:
136 //Value for checking if condition is trivially true or false.
137 //0 is undecided (default), 1 is true, 2 is false.
138
139=== modified file 'PetriEngine/PetriNetBuilder.cpp'
140--- PetriEngine/PetriNetBuilder.cpp 2018-02-22 16:42:37 +0000
141+++ PetriEngine/PetriNetBuilder.cpp 2018-04-30 15:54:05 +0000
142@@ -27,6 +27,7 @@
143 #include "PQL/PQL.h"
144 #include "PQL/Contexts.h"
145 #include "Reducer.h"
146+#include "PQL/Expressions.h"
147
148 using namespace std;
149
150@@ -463,7 +464,9 @@
151 queries[i]->analyze(placecontext);
152 all_reach &= (results[i] != Reachability::ResultPrinter::CTL);
153 remove_loops &= !queries[i]->isLoopSensitive();
154- contains_next |= queries[i]->containsNext();
155+ // There is a deadlock somewhere, if it is not alone, we cannot reduce.
156+ // this has similar problems as nested next.
157+ contains_next |= queries[i]->containsNext() || queries[i]->nestedDeadlock();
158 }
159 }
160 reducer.Reduce(placecontext, reductiontype, reconstructTrace, timeout, remove_loops, all_reach, contains_next);

Subscribers

People subscribed via source and target branches