verifypn

Merge lp:~tapaal-ltl/verifypn/kbound-fix-ltl into lp:verifypn

  1. kbound-fix-ltl
  2. Merge into new-trunk
Proposed by Nikolaj Jensen Ulrik
Status: Merged
Approved by: Jiri Srba
Approved revision: 249
Merged at revision: 250
Proposed branch: lp:~tapaal-ltl/verifypn/kbound-fix-ltl
Merge into: lp:verifypn
Diff against target: 319 lines (+81/-42)
8 files modified
include/LTL/Algorithm/NestedDepthFirstSearch.h (+12/-12)
include/LTL/Algorithm/TarjanModelChecker.h (+2/-1)
include/LTL/Structures/BitProductStateSet.h (+5/-2)
include/PetriEngine/PQL/Expressions.h (+1/-0)
src/LTL/Algorithm/NestedDepthFirstSearch.cpp (+23/-14)
src/LTL/Algorithm/TarjanModelChecker.cpp (+3/-0)
src/LTL/LTLMain.cpp (+24/-12)
src/PetriEngine/PQL/Expressions.cpp (+11/-1)
To merge this branch: bzr merge lp:~tapaal-ltl/verifypn/kbound-fix-ltl
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Peter Gjøl Jensen Approve
Review via email: mp+406929@code.launchpad.net

Description of the change

introduces k-bounds checking in Tarjan and in NDFS, fixing a bug with bad token counts in NDFS.

To post a comment you must log in.
lp:~tapaal-ltl/verifypn/kbound-fix-ltl updated
249. By Nikolaj Jensen Ulrik

Fix 'A true' crashing the verifier in LTL mode

Revision history for this message
Peter Gjøl Jensen (peter-gjoel) :
Revision history for this message
Nikolaj Jensen Ulrik (waefwerf) :
Revision history for this message
Peter Gjøl Jensen (peter-gjoel) wrote :

LGTM.

review: Approve
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 'include/LTL/Algorithm/NestedDepthFirstSearch.h'
2--- include/LTL/Algorithm/NestedDepthFirstSearch.h 2021-04-29 11:05:46 +0000
3+++ include/LTL/Algorithm/NestedDepthFirstSearch.h 2021-08-12 12:36:05 +0000
4@@ -49,10 +49,10 @@
5 class NestedDepthFirstSearch : public ModelChecker<ProductSuccessorGenerator, SucGen> {
6 public:
7 NestedDepthFirstSearch(const PetriEngine::PetriNet *net, const PetriEngine::PQL::Condition_ptr &query,
8- const Structures::BuchiAutomaton &buchi, SucGen *gen)
9+ const Structures::BuchiAutomaton &buchi, SucGen *gen, int kbound)
10 : ModelChecker<ProductSuccessorGenerator, SucGen>(net, query, buchi, gen),
11 factory{net, this->successorGenerator->initial_buchi_state()},
12- states(*net, 0, (int) net->numberOfPlaces() + 1) {}
13+ states(net, kbound) {}
14
15 bool isSatisfied() override;
16
17@@ -87,16 +87,16 @@
18 };
19
20 extern template
21- class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, PetriEngine::Structures::StateSet>;
22-
23- extern template
24- class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, PetriEngine::Structures::TracableStateSet>;
25-
26- extern template
27- class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, PetriEngine::Structures::StateSet>;
28-
29- extern template
30- class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, PetriEngine::Structures::TracableStateSet>;
31+ class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, LTL::Structures::BitProductStateSet<>>;
32+
33+ extern template
34+ class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, LTL::Structures::TraceableBitProductStateSet<>>;
35+
36+ extern template
37+ class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, LTL::Structures::BitProductStateSet<>>;
38+
39+ extern template
40+ class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, LTL::Structures::TraceableBitProductStateSet<>>;
41 }
42
43 #endif //VERIFYPN_NESTEDDEPTHFIRSTSEARCH_H
44
45=== modified file 'include/LTL/Algorithm/TarjanModelChecker.h'
46--- include/LTL/Algorithm/TarjanModelChecker.h 2021-08-03 14:19:42 +0000
47+++ include/LTL/Algorithm/TarjanModelChecker.h 2021-08-12 12:36:05 +0000
48@@ -49,10 +49,11 @@
49 TarjanModelChecker(const PetriEngine::PetriNet *net, const PetriEngine::PQL::Condition_ptr &cond,
50 const Structures::BuchiAutomaton &buchi,
51 SuccessorGen *successorGen,
52+ int kbound,
53 std::unique_ptr<Spooler> &&...spooler)
54 : ModelChecker<ProductSucGen, SuccessorGen, Spooler...>(net, cond, buchi, successorGen, std::move(spooler)...),
55 factory(net, this->successorGenerator->initial_buchi_state()),
56- seen(net, 0)
57+ seen(net, kbound)
58 {
59 if (buchi._buchi->num_states() > 65535) {
60 std::cerr << "Fatal error: cannot handle Büchi automata larger than 2^16 states\n";
61
62=== modified file 'include/LTL/Structures/BitProductStateSet.h'
63--- include/LTL/Structures/BitProductStateSet.h 2021-08-03 14:19:42 +0000
64+++ include/LTL/Structures/BitProductStateSet.h 2021-08-12 12:36:05 +0000
65@@ -94,8 +94,11 @@
66 result_t add(const LTL::Structures::ProductState &state) override
67 {
68 ++_discovered;
69- const auto[_, markingId] = markings.add(state);
70- const stateid_t product_id = getProductId(markingId, state.getBuchiState());
71+ const auto res = markings.add(state);
72+ if (res.second == std::numeric_limits<size_t>::max()) {
73+ return res;
74+ }
75+ const stateid_t product_id = getProductId(res.second, state.getBuchiState());
76
77 const auto[iter, is_new] = states.insert(product_id);
78 assert(iter != std::end(states));
79
80=== modified file 'include/PetriEngine/PQL/Expressions.h'
81--- include/PetriEngine/PQL/Expressions.h 2021-07-07 13:19:23 +0000
82+++ include/PetriEngine/PQL/Expressions.h 2021-08-12 12:36:05 +0000
83@@ -489,6 +489,7 @@
84 uint32_t retval = _cond->distance(context);
85 return retval;
86 }
87+
88 void visit(Visitor&) const override;
89 void visit(MutatingVisitor&) override;
90
91
92=== modified file 'src/LTL/Algorithm/NestedDepthFirstSearch.cpp'
93--- src/LTL/Algorithm/NestedDepthFirstSearch.cpp 2021-08-04 13:24:38 +0000
94+++ src/LTL/Algorithm/NestedDepthFirstSearch.cpp 2021-08-12 12:36:05 +0000
95@@ -40,9 +40,11 @@
96 std::vector<State> initial_states = this->successorGenerator->makeInitialState();
97 for (auto &state : initial_states) {
98 auto res = states.add(state);
99- assert(res.first);
100- todo.push(StackEntry{res.second, S::initial_suc_info()});
101- this->_discovered++;
102+ if (res.first) {
103+ assert(res.first);
104+ todo.push(StackEntry{res.second, S::initial_suc_info()});
105+ this->_discovered++;
106+ }
107 }
108 }
109
110@@ -77,6 +79,9 @@
111 }
112 } else {
113 auto[_, stateid] = states.add(working);
114+ if (stateid == std::numeric_limits<size_t>::max()) {
115+ continue;
116+ }
117 auto[it, is_new] = mark1.insert(stateid);
118 top.sucinfo.last_state = stateid;
119 if (is_new) {
120@@ -131,6 +136,9 @@
121 return;
122 }
123 auto[_, stateid] = states.add(working);
124+ if (stateid == std::numeric_limits<size_t>::max()) {
125+ continue;
126+ }
127 auto[it, is_new] = mark2.insert(stateid);
128 top.sucinfo.last_state = stateid;
129 if (is_new) {
130@@ -151,7 +159,7 @@
131 {
132 std::cout << "STATS:\n"
133 << "\tdiscovered states: " << states.discovered() << std::endl
134- << "\tmax tokens: " << states.maxTokens() << std::endl
135+ << "\tmax tokens: " << states.max_tokens() << std::endl
136 << "\texplored states: " << mark1.size() << std::endl
137 << "\texplored states (nested): " << mark2.size() << std::endl;
138 }
139@@ -181,14 +189,15 @@
140 }
141
142 template
143- class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, PetriEngine::Structures::StateSet>;
144-
145- template
146- class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, PetriEngine::Structures::TracableStateSet>;
147-
148- template
149- class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, PetriEngine::Structures::StateSet>;
150-
151- template
152- class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, PetriEngine::Structures::TracableStateSet>;
153+ class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, LTL::Structures::BitProductStateSet<>>;
154+
155+ template
156+ class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, LTL::Structures::TraceableBitProductStateSet<>>;
157+
158+ template
159+ class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, LTL::Structures::BitProductStateSet<>>;
160+
161+ template
162+ class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, LTL::Structures::TraceableBitProductStateSet<>>;
163+
164 }
165
166=== modified file 'src/LTL/Algorithm/TarjanModelChecker.cpp'
167--- src/LTL/Algorithm/TarjanModelChecker.cpp 2021-08-03 14:19:42 +0000
168+++ src/LTL/Algorithm/TarjanModelChecker.cpp 2021-08-12 12:36:05 +0000
169@@ -41,6 +41,9 @@
170 }
171 ++this->stats.explored;
172 const auto[isnew, stateid] = seen.add(working);
173+ if (stateid == std::numeric_limits<idx_t>::max()) {
174+ continue;
175+ }
176
177 if constexpr (SaveTrace) {
178 if (isnew) {
179
180=== modified file 'src/LTL/LTLMain.cpp'
181--- src/LTL/LTLMain.cpp 2021-08-04 12:57:39 +0000
182+++ src/LTL/LTLMain.cpp 2021-08-12 12:36:05 +0000
183@@ -153,14 +153,16 @@
184 if (options.trace != TraceLevel::None) {
185 result = _verify(
186 net, negated_formula,
187- std::make_unique<NestedDepthFirstSearch<SpoolingSuccessorGenerator, PetriEngine::Structures::TracableStateSet>>(
188- net, negated_formula, automaton, &gen),
189+ std::make_unique<NestedDepthFirstSearch<SpoolingSuccessorGenerator, LTL::Structures::TraceableBitProductStateSet<> >>(
190+ net, negated_formula, automaton, &gen,
191+ options.kbound),
192 options);
193 } else {
194 result = _verify(
195 net, negated_formula,
196- std::make_unique<NestedDepthFirstSearch<SpoolingSuccessorGenerator, PetriEngine::Structures::StateSet>>(
197- net, negated_formula, automaton, &gen),
198+ std::make_unique<NestedDepthFirstSearch<SpoolingSuccessorGenerator, LTL::Structures::BitProductStateSet<> >>(
199+ net, negated_formula, automaton, &gen,
200+ options.kbound),
201 options);
202 }
203 } else {
204@@ -168,14 +170,16 @@
205 if (options.trace != TraceLevel::None) {
206 result = _verify(
207 net, negated_formula,
208- std::make_unique<NestedDepthFirstSearch<ResumingSuccessorGenerator, PetriEngine::Structures::TracableStateSet>>(
209- net, negated_formula, automaton, &gen),
210+ std::make_unique<NestedDepthFirstSearch<ResumingSuccessorGenerator, LTL::Structures::TraceableBitProductStateSet<> >>(
211+ net, negated_formula, automaton, &gen,
212+ options.kbound),
213 options);
214 } else {
215 result = _verify(
216 net, negated_formula,
217- std::make_unique<NestedDepthFirstSearch<ResumingSuccessorGenerator, PetriEngine::Structures::StateSet>>(
218- net, negated_formula, automaton, &gen),
219+ std::make_unique<NestedDepthFirstSearch<ResumingSuccessorGenerator, LTL::Structures::BitProductStateSet<> >>(
220+ net, negated_formula, automaton, &gen,
221+ options.kbound),
222 options);
223 }
224 }
225@@ -213,6 +217,7 @@
226 negated_formula,
227 automaton,
228 &gen,
229+ options.kbound,
230 std::make_unique<VisibleLTLStubbornSet>(*net, negated_formula)),
231 options);
232 }
233@@ -223,6 +228,7 @@
234 negated_formula,
235 automaton,
236 &gen,
237+ options.kbound,
238 std::make_unique<EnabledSpooler>(net, gen)),
239 options);
240 }
241@@ -232,7 +238,8 @@
242 net,
243 negated_formula,
244 automaton,
245- &gen),
246+ &gen,
247+ options.kbound),
248 options);
249 }
250 } else {
251@@ -244,6 +251,7 @@
252 negated_formula,
253 automaton,
254 &gen,
255+ options.kbound,
256 std::make_unique<VisibleLTLStubbornSet>(*net, negated_formula)),
257 options);
258 } else if (is_autreach_stub && !is_visible_stub) {
259@@ -253,6 +261,7 @@
260 negated_formula,
261 automaton,
262 &gen,
263+ options.kbound,
264 std::make_unique<EnabledSpooler>(net, gen)),
265 options);
266 }
267@@ -262,7 +271,8 @@
268 net,
269 negated_formula,
270 automaton,
271- &gen),
272+ &gen,
273+ options.kbound),
274 options);
275 }
276 }
277@@ -276,7 +286,8 @@
278 net,
279 negated_formula,
280 automaton,
281- &gen),
282+ &gen,
283+ options.kbound),
284 options);
285 } else {
286 result = _verify(net, negated_formula,
287@@ -284,7 +295,8 @@
288 net,
289 negated_formula,
290 automaton,
291- &gen),
292+ &gen,
293+ options.kbound),
294 options);
295 }
296 }
297
298=== modified file 'src/PetriEngine/PQL/Expressions.cpp'
299--- src/PetriEngine/PQL/Expressions.cpp 2021-07-07 13:19:23 +0000
300+++ src/PetriEngine/PQL/Expressions.cpp 2021-08-12 12:36:05 +0000
301@@ -3554,7 +3554,17 @@
302
303 Condition_ptr ACondition::prepareForReachability(bool negated) const {
304 auto g = std::dynamic_pointer_cast<GCondition>(_cond);
305- return g ? AGCondition((*g)[0]).prepareForReachability(negated) : nullptr;
306+ if (g) {
307+ return AGCondition((*g)[0]).prepareForReachability(negated);
308+ }
309+ else {
310+ // ugly hacking for `A true`.
311+ auto bcond = std::dynamic_pointer_cast<BooleanCondition>(_cond);
312+ if (bcond) {
313+ return bcond;
314+ }
315+ else return nullptr;
316+ }
317 }
318
319 Condition_ptr ECondition::prepareForReachability(bool negated) const {

Subscribers

People subscribed via source and target branches