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
=== modified file 'include/LTL/Algorithm/NestedDepthFirstSearch.h'
--- include/LTL/Algorithm/NestedDepthFirstSearch.h 2021-04-29 11:05:46 +0000
+++ include/LTL/Algorithm/NestedDepthFirstSearch.h 2021-08-12 12:36:05 +0000
@@ -49,10 +49,10 @@
49class NestedDepthFirstSearch : public ModelChecker<ProductSuccessorGenerator, SucGen> {49class NestedDepthFirstSearch : public ModelChecker<ProductSuccessorGenerator, SucGen> {
50 public:50 public:
51 NestedDepthFirstSearch(const PetriEngine::PetriNet *net, const PetriEngine::PQL::Condition_ptr &query,51 NestedDepthFirstSearch(const PetriEngine::PetriNet *net, const PetriEngine::PQL::Condition_ptr &query,
52 const Structures::BuchiAutomaton &buchi, SucGen *gen)52 const Structures::BuchiAutomaton &buchi, SucGen *gen, int kbound)
53 : ModelChecker<ProductSuccessorGenerator, SucGen>(net, query, buchi, gen),53 : ModelChecker<ProductSuccessorGenerator, SucGen>(net, query, buchi, gen),
54 factory{net, this->successorGenerator->initial_buchi_state()},54 factory{net, this->successorGenerator->initial_buchi_state()},
55 states(*net, 0, (int) net->numberOfPlaces() + 1) {}55 states(net, kbound) {}
5656
57 bool isSatisfied() override;57 bool isSatisfied() override;
5858
@@ -87,16 +87,16 @@
87 };87 };
8888
89 extern template89 extern template
90 class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, PetriEngine::Structures::StateSet>;90 class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, LTL::Structures::BitProductStateSet<>>;
9191
92 extern template92 extern template
93 class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, PetriEngine::Structures::TracableStateSet>;93 class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, LTL::Structures::TraceableBitProductStateSet<>>;
9494
95 extern template95 extern template
96 class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, PetriEngine::Structures::StateSet>;96 class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, LTL::Structures::BitProductStateSet<>>;
9797
98 extern template98 extern template
99 class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, PetriEngine::Structures::TracableStateSet>;99 class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, LTL::Structures::TraceableBitProductStateSet<>>;
100}100}
101101
102#endif //VERIFYPN_NESTEDDEPTHFIRSTSEARCH_H102#endif //VERIFYPN_NESTEDDEPTHFIRSTSEARCH_H
103103
=== modified file 'include/LTL/Algorithm/TarjanModelChecker.h'
--- include/LTL/Algorithm/TarjanModelChecker.h 2021-08-03 14:19:42 +0000
+++ include/LTL/Algorithm/TarjanModelChecker.h 2021-08-12 12:36:05 +0000
@@ -49,10 +49,11 @@
49 TarjanModelChecker(const PetriEngine::PetriNet *net, const PetriEngine::PQL::Condition_ptr &cond,49 TarjanModelChecker(const PetriEngine::PetriNet *net, const PetriEngine::PQL::Condition_ptr &cond,
50 const Structures::BuchiAutomaton &buchi,50 const Structures::BuchiAutomaton &buchi,
51 SuccessorGen *successorGen,51 SuccessorGen *successorGen,
52 int kbound,
52 std::unique_ptr<Spooler> &&...spooler)53 std::unique_ptr<Spooler> &&...spooler)
53 : ModelChecker<ProductSucGen, SuccessorGen, Spooler...>(net, cond, buchi, successorGen, std::move(spooler)...),54 : ModelChecker<ProductSucGen, SuccessorGen, Spooler...>(net, cond, buchi, successorGen, std::move(spooler)...),
54 factory(net, this->successorGenerator->initial_buchi_state()),55 factory(net, this->successorGenerator->initial_buchi_state()),
55 seen(net, 0)56 seen(net, kbound)
56 {57 {
57 if (buchi._buchi->num_states() > 65535) {58 if (buchi._buchi->num_states() > 65535) {
58 std::cerr << "Fatal error: cannot handle Büchi automata larger than 2^16 states\n";59 std::cerr << "Fatal error: cannot handle Büchi automata larger than 2^16 states\n";
5960
=== modified file 'include/LTL/Structures/BitProductStateSet.h'
--- include/LTL/Structures/BitProductStateSet.h 2021-08-03 14:19:42 +0000
+++ include/LTL/Structures/BitProductStateSet.h 2021-08-12 12:36:05 +0000
@@ -94,8 +94,11 @@
94 result_t add(const LTL::Structures::ProductState &state) override94 result_t add(const LTL::Structures::ProductState &state) override
95 {95 {
96 ++_discovered;96 ++_discovered;
97 const auto[_, markingId] = markings.add(state);97 const auto res = markings.add(state);
98 const stateid_t product_id = getProductId(markingId, state.getBuchiState());98 if (res.second == std::numeric_limits<size_t>::max()) {
99 return res;
100 }
101 const stateid_t product_id = getProductId(res.second, state.getBuchiState());
99102
100 const auto[iter, is_new] = states.insert(product_id);103 const auto[iter, is_new] = states.insert(product_id);
101 assert(iter != std::end(states));104 assert(iter != std::end(states));
102105
=== modified file 'include/PetriEngine/PQL/Expressions.h'
--- include/PetriEngine/PQL/Expressions.h 2021-07-07 13:19:23 +0000
+++ include/PetriEngine/PQL/Expressions.h 2021-08-12 12:36:05 +0000
@@ -489,6 +489,7 @@
489 uint32_t retval = _cond->distance(context);489 uint32_t retval = _cond->distance(context);
490 return retval;490 return retval;
491 }491 }
492
492 void visit(Visitor&) const override;493 void visit(Visitor&) const override;
493 void visit(MutatingVisitor&) override;494 void visit(MutatingVisitor&) override;
494495
495496
=== modified file 'src/LTL/Algorithm/NestedDepthFirstSearch.cpp'
--- src/LTL/Algorithm/NestedDepthFirstSearch.cpp 2021-08-04 13:24:38 +0000
+++ src/LTL/Algorithm/NestedDepthFirstSearch.cpp 2021-08-12 12:36:05 +0000
@@ -40,9 +40,11 @@
40 std::vector<State> initial_states = this->successorGenerator->makeInitialState();40 std::vector<State> initial_states = this->successorGenerator->makeInitialState();
41 for (auto &state : initial_states) {41 for (auto &state : initial_states) {
42 auto res = states.add(state);42 auto res = states.add(state);
43 assert(res.first);43 if (res.first) {
44 todo.push(StackEntry{res.second, S::initial_suc_info()});44 assert(res.first);
45 this->_discovered++;45 todo.push(StackEntry{res.second, S::initial_suc_info()});
46 this->_discovered++;
47 }
46 }48 }
47 }49 }
4850
@@ -77,6 +79,9 @@
77 }79 }
78 } else {80 } else {
79 auto[_, stateid] = states.add(working);81 auto[_, stateid] = states.add(working);
82 if (stateid == std::numeric_limits<size_t>::max()) {
83 continue;
84 }
80 auto[it, is_new] = mark1.insert(stateid);85 auto[it, is_new] = mark1.insert(stateid);
81 top.sucinfo.last_state = stateid;86 top.sucinfo.last_state = stateid;
82 if (is_new) {87 if (is_new) {
@@ -131,6 +136,9 @@
131 return;136 return;
132 }137 }
133 auto[_, stateid] = states.add(working);138 auto[_, stateid] = states.add(working);
139 if (stateid == std::numeric_limits<size_t>::max()) {
140 continue;
141 }
134 auto[it, is_new] = mark2.insert(stateid);142 auto[it, is_new] = mark2.insert(stateid);
135 top.sucinfo.last_state = stateid;143 top.sucinfo.last_state = stateid;
136 if (is_new) {144 if (is_new) {
@@ -151,7 +159,7 @@
151 {159 {
152 std::cout << "STATS:\n"160 std::cout << "STATS:\n"
153 << "\tdiscovered states: " << states.discovered() << std::endl161 << "\tdiscovered states: " << states.discovered() << std::endl
154 << "\tmax tokens: " << states.maxTokens() << std::endl162 << "\tmax tokens: " << states.max_tokens() << std::endl
155 << "\texplored states: " << mark1.size() << std::endl163 << "\texplored states: " << mark1.size() << std::endl
156 << "\texplored states (nested): " << mark2.size() << std::endl;164 << "\texplored states (nested): " << mark2.size() << std::endl;
157 }165 }
@@ -181,14 +189,15 @@
181 }189 }
182190
183 template191 template
184 class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, PetriEngine::Structures::StateSet>;192 class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, LTL::Structures::BitProductStateSet<>>;
185193
186 template194 template
187 class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, PetriEngine::Structures::TracableStateSet>;195 class NestedDepthFirstSearch<LTL::ResumingSuccessorGenerator, LTL::Structures::TraceableBitProductStateSet<>>;
188196
189 template197 template
190 class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, PetriEngine::Structures::StateSet>;198 class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, LTL::Structures::BitProductStateSet<>>;
191199
192 template200 template
193 class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, PetriEngine::Structures::TracableStateSet>;201 class NestedDepthFirstSearch<LTL::SpoolingSuccessorGenerator, LTL::Structures::TraceableBitProductStateSet<>>;
202
194}203}
195204
=== modified file 'src/LTL/Algorithm/TarjanModelChecker.cpp'
--- src/LTL/Algorithm/TarjanModelChecker.cpp 2021-08-03 14:19:42 +0000
+++ src/LTL/Algorithm/TarjanModelChecker.cpp 2021-08-12 12:36:05 +0000
@@ -41,6 +41,9 @@
41 }41 }
42 ++this->stats.explored;42 ++this->stats.explored;
43 const auto[isnew, stateid] = seen.add(working);43 const auto[isnew, stateid] = seen.add(working);
44 if (stateid == std::numeric_limits<idx_t>::max()) {
45 continue;
46 }
4447
45 if constexpr (SaveTrace) {48 if constexpr (SaveTrace) {
46 if (isnew) {49 if (isnew) {
4750
=== modified file 'src/LTL/LTLMain.cpp'
--- src/LTL/LTLMain.cpp 2021-08-04 12:57:39 +0000
+++ src/LTL/LTLMain.cpp 2021-08-12 12:36:05 +0000
@@ -153,14 +153,16 @@
153 if (options.trace != TraceLevel::None) {153 if (options.trace != TraceLevel::None) {
154 result = _verify(154 result = _verify(
155 net, negated_formula,155 net, negated_formula,
156 std::make_unique<NestedDepthFirstSearch<SpoolingSuccessorGenerator, PetriEngine::Structures::TracableStateSet>>(156 std::make_unique<NestedDepthFirstSearch<SpoolingSuccessorGenerator, LTL::Structures::TraceableBitProductStateSet<> >>(
157 net, negated_formula, automaton, &gen),157 net, negated_formula, automaton, &gen,
158 options.kbound),
158 options);159 options);
159 } else {160 } else {
160 result = _verify(161 result = _verify(
161 net, negated_formula,162 net, negated_formula,
162 std::make_unique<NestedDepthFirstSearch<SpoolingSuccessorGenerator, PetriEngine::Structures::StateSet>>(163 std::make_unique<NestedDepthFirstSearch<SpoolingSuccessorGenerator, LTL::Structures::BitProductStateSet<> >>(
163 net, negated_formula, automaton, &gen),164 net, negated_formula, automaton, &gen,
165 options.kbound),
164 options);166 options);
165 }167 }
166 } else {168 } else {
@@ -168,14 +170,16 @@
168 if (options.trace != TraceLevel::None) {170 if (options.trace != TraceLevel::None) {
169 result = _verify(171 result = _verify(
170 net, negated_formula,172 net, negated_formula,
171 std::make_unique<NestedDepthFirstSearch<ResumingSuccessorGenerator, PetriEngine::Structures::TracableStateSet>>(173 std::make_unique<NestedDepthFirstSearch<ResumingSuccessorGenerator, LTL::Structures::TraceableBitProductStateSet<> >>(
172 net, negated_formula, automaton, &gen),174 net, negated_formula, automaton, &gen,
175 options.kbound),
173 options);176 options);
174 } else {177 } else {
175 result = _verify(178 result = _verify(
176 net, negated_formula,179 net, negated_formula,
177 std::make_unique<NestedDepthFirstSearch<ResumingSuccessorGenerator, PetriEngine::Structures::StateSet>>(180 std::make_unique<NestedDepthFirstSearch<ResumingSuccessorGenerator, LTL::Structures::BitProductStateSet<> >>(
178 net, negated_formula, automaton, &gen),181 net, negated_formula, automaton, &gen,
182 options.kbound),
179 options);183 options);
180 }184 }
181 }185 }
@@ -213,6 +217,7 @@
213 negated_formula,217 negated_formula,
214 automaton,218 automaton,
215 &gen,219 &gen,
220 options.kbound,
216 std::make_unique<VisibleLTLStubbornSet>(*net, negated_formula)),221 std::make_unique<VisibleLTLStubbornSet>(*net, negated_formula)),
217 options);222 options);
218 }223 }
@@ -223,6 +228,7 @@
223 negated_formula,228 negated_formula,
224 automaton,229 automaton,
225 &gen,230 &gen,
231 options.kbound,
226 std::make_unique<EnabledSpooler>(net, gen)),232 std::make_unique<EnabledSpooler>(net, gen)),
227 options);233 options);
228 }234 }
@@ -232,7 +238,8 @@
232 net,238 net,
233 negated_formula,239 negated_formula,
234 automaton,240 automaton,
235 &gen),241 &gen,
242 options.kbound),
236 options);243 options);
237 }244 }
238 } else {245 } else {
@@ -244,6 +251,7 @@
244 negated_formula,251 negated_formula,
245 automaton,252 automaton,
246 &gen,253 &gen,
254 options.kbound,
247 std::make_unique<VisibleLTLStubbornSet>(*net, negated_formula)),255 std::make_unique<VisibleLTLStubbornSet>(*net, negated_formula)),
248 options);256 options);
249 } else if (is_autreach_stub && !is_visible_stub) {257 } else if (is_autreach_stub && !is_visible_stub) {
@@ -253,6 +261,7 @@
253 negated_formula,261 negated_formula,
254 automaton,262 automaton,
255 &gen,263 &gen,
264 options.kbound,
256 std::make_unique<EnabledSpooler>(net, gen)),265 std::make_unique<EnabledSpooler>(net, gen)),
257 options);266 options);
258 }267 }
@@ -262,7 +271,8 @@
262 net,271 net,
263 negated_formula,272 negated_formula,
264 automaton,273 automaton,
265 &gen),274 &gen,
275 options.kbound),
266 options);276 options);
267 }277 }
268 }278 }
@@ -276,7 +286,8 @@
276 net,286 net,
277 negated_formula,287 negated_formula,
278 automaton,288 automaton,
279 &gen),289 &gen,
290 options.kbound),
280 options);291 options);
281 } else {292 } else {
282 result = _verify(net, negated_formula,293 result = _verify(net, negated_formula,
@@ -284,7 +295,8 @@
284 net,295 net,
285 negated_formula,296 negated_formula,
286 automaton,297 automaton,
287 &gen),298 &gen,
299 options.kbound),
288 options);300 options);
289 }301 }
290 }302 }
291303
=== modified file 'src/PetriEngine/PQL/Expressions.cpp'
--- src/PetriEngine/PQL/Expressions.cpp 2021-07-07 13:19:23 +0000
+++ src/PetriEngine/PQL/Expressions.cpp 2021-08-12 12:36:05 +0000
@@ -3554,7 +3554,17 @@
35543554
3555 Condition_ptr ACondition::prepareForReachability(bool negated) const {3555 Condition_ptr ACondition::prepareForReachability(bool negated) const {
3556 auto g = std::dynamic_pointer_cast<GCondition>(_cond);3556 auto g = std::dynamic_pointer_cast<GCondition>(_cond);
3557 return g ? AGCondition((*g)[0]).prepareForReachability(negated) : nullptr;3557 if (g) {
3558 return AGCondition((*g)[0]).prepareForReachability(negated);
3559 }
3560 else {
3561 // ugly hacking for `A true`.
3562 auto bcond = std::dynamic_pointer_cast<BooleanCondition>(_cond);
3563 if (bcond) {
3564 return bcond;
3565 }
3566 else return nullptr;
3567 }
3558 }3568 }
35593569
3560 Condition_ptr ECondition::prepareForReachability(bool negated) const {3570 Condition_ptr ECondition::prepareForReachability(bool negated) const {

Subscribers

People subscribed via source and target branches