Merge lp:~tapaal-ltl/verifypn/resumable-suc-generator into lp:~tapaal-ltl/verifypn/ltl_model_checker
- resumable-suc-generator
- Merge into ltl_model_checker
Proposed by
Simon Virenfeldt
Status: | Merged |
---|---|
Merged at revision: | 232 |
Proposed branch: | lp:~tapaal-ltl/verifypn/resumable-suc-generator |
Merge into: | lp:~tapaal-ltl/verifypn/ltl_model_checker |
Diff against target: |
1016 lines (+357/-197) 15 files modified
CMakeLists.txt (+2/-2) include/LTL/BuchiSuccessorGenerator.h (+2/-2) include/LTL/LTL_algorithm/ModelChecker.h (+2/-0) include/LTL/LTL_algorithm/NestedDepthFirstSearch.h (+9/-3) include/LTL/LTL_algorithm/TarjanModelChecker.h (+26/-22) include/LTL/ProductSuccessorGenerator.h (+68/-5) include/LTL/Structures/ProductState.h (+2/-0) include/PetriEngine/PQL/Expressions.h (+2/-2) include/PetriEngine/SuccessorGenerator.h (+5/-1) src/LTL/LTL_algorithm/LTLToBuchi.cpp (+17/-31) src/LTL/LTL_algorithm/NestedDepthFirstSearch.cpp (+57/-51) src/LTL/LTL_algorithm/ProductSuccessorGenerator.cpp (+42/-9) src/LTL/LTL_algorithm/TarjanModelChecker.cpp (+118/-64) src/LTLMain.cpp (+4/-4) src/PetriEngine/SuccessorGenerator.cpp (+1/-1) |
To merge this branch: | bzr merge lp:~tapaal-ltl/verifypn/resumable-suc-generator |
Related bugs: |
Reviewer | Review Type | Date Requested | Status |
---|---|---|---|
Simon Virenfeldt | Approve | ||
Review via email: mp+393497@code.launchpad.net |
Commit message
Merge branch resumable_
Description of the change
To post a comment you must log in.
- 262. By Simon Virenfeldt
-
Removed some commented code lines
- 263. By Simon Virenfeldt
-
Merge remote
Revision history for this message
Simon Virenfeldt (simwir) : | # |
review:
Approve
Preview Diff
[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1 | === modified file 'CMakeLists.txt' |
2 | --- CMakeLists.txt 2020-10-19 11:13:27 +0000 |
3 | +++ CMakeLists.txt 2020-11-09 13:59:57 +0000 |
4 | @@ -29,7 +29,7 @@ |
5 | endif() |
6 | |
7 | if (CMAKE_BUILD_TYPE MATCHES Debug) |
8 | - #add_compile_definitions(PRINTF_DEBUG) |
9 | + add_compile_definitions(PRINTF_DEBUG) |
10 | endif() |
11 | |
12 | if (VERIFYPN_Static) |
13 | @@ -59,7 +59,7 @@ |
14 | endif () |
15 | |
16 | set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -Wall -pedantic-errors -O3 -DNDEBUG") |
17 | -set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -O0 -fno-omit-frame-pointer -fsanitize=address ") |
18 | +set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -O0 -fno-omit-frame-pointer") |
19 | set(CMAKE_EXE_LINKER_FLAGS_RELEASE "${CMAKE_EXE_LINKER_FLAGS_RELEASE} -O3 -DNDEBUG") |
20 | if (VERIFYPN_Static AND NOT APPLE) |
21 | set(CMAKE_EXE_LINKER_FLAGS_RELEASE "${CMAKE_EXE_LINKER_FLAGS_RELEASE} -static") |
22 | |
23 | === modified file 'include/LTL/BuchiSuccessorGenerator.h' |
24 | --- include/LTL/BuchiSuccessorGenerator.h 2020-10-05 10:15:17 +0000 |
25 | +++ include/LTL/BuchiSuccessorGenerator.h 2020-11-09 13:59:57 +0000 |
26 | @@ -18,7 +18,7 @@ |
27 | namespace LTL { |
28 | class BuchiSuccessorGenerator { |
29 | public: |
30 | - BuchiSuccessorGenerator(Structures::BuchiAutomaton automaton) |
31 | + explicit BuchiSuccessorGenerator(Structures::BuchiAutomaton automaton) |
32 | : aut(std::move(automaton)) { |
33 | } |
34 | |
35 | @@ -31,7 +31,7 @@ |
36 | bool next(size_t &state, bdd &cond) { |
37 | if (!succ->done()) { |
38 | state = aut.buchi->state_number(succ->dst()); |
39 | -#ifdef PRINTF_DEBUG |
40 | +#ifdef _PRINTF_DEBUG |
41 | std::cerr << "buchi state " << state << std::endl; |
42 | #endif |
43 | cond = succ->cond(); |
44 | |
45 | === modified file 'include/LTL/LTL_algorithm/ModelChecker.h' |
46 | --- include/LTL/LTL_algorithm/ModelChecker.h 2020-10-16 11:34:00 +0000 |
47 | +++ include/LTL/LTL_algorithm/ModelChecker.h 2020-11-09 13:59:57 +0000 |
48 | @@ -20,6 +20,8 @@ |
49 | std::unique_ptr<ProductSuccessorGenerator> successorGenerator; |
50 | const PetriEngine::PetriNet &net; |
51 | PetriEngine::PQL::Condition_ptr formula; |
52 | + |
53 | + size_t _discovered = 0; |
54 | }; |
55 | } |
56 | |
57 | |
58 | === modified file 'include/LTL/LTL_algorithm/NestedDepthFirstSearch.h' |
59 | --- include/LTL/LTL_algorithm/NestedDepthFirstSearch.h 2020-10-05 10:15:17 +0000 |
60 | +++ include/LTL/LTL_algorithm/NestedDepthFirstSearch.h 2020-11-09 13:59:57 +0000 |
61 | @@ -12,6 +12,7 @@ |
62 | #include "LTL/Structures/ProductStateFactory.h" |
63 | |
64 | #include <ptrie/ptrie_stable.h> |
65 | +#include <unordered_set> |
66 | |
67 | using namespace PetriEngine; |
68 | |
69 | @@ -20,7 +21,7 @@ |
70 | public: |
71 | NestedDepthFirstSearch(const PetriNet &net, PetriEngine::PQL::Condition_ptr ptr) |
72 | : ModelChecker(net, ptr), factory{net, successorGenerator->initial_buchi_state()}, |
73 | - mark1(net, 0, (int)net.numberOfPlaces() + 1), mark2(net, 0, (int)net.numberOfPlaces() + 1) {} |
74 | + states(net, 0, (int)net.numberOfPlaces() + 1) {} |
75 | |
76 | bool isSatisfied() override; |
77 | |
78 | @@ -28,9 +29,14 @@ |
79 | using State = LTL::Structures::ProductState; |
80 | |
81 | Structures::ProductStateFactory factory; |
82 | - PetriEngine::Structures::StateSet mark1; |
83 | - PetriEngine::Structures::StateSet mark2; |
84 | + PetriEngine::Structures::StateSet states; |
85 | + std::set<size_t> mark1; |
86 | + std::set<size_t> mark2; |
87 | |
88 | + struct StackEntry { |
89 | + size_t id; |
90 | + successor_info sucinfo; |
91 | + }; |
92 | |
93 | State *seed; |
94 | bool violation = false; |
95 | |
96 | === modified file 'include/LTL/LTL_algorithm/TarjanModelChecker.h' |
97 | --- include/LTL/LTL_algorithm/TarjanModelChecker.h 2020-10-19 12:35:11 +0000 |
98 | +++ include/LTL/LTL_algorithm/TarjanModelChecker.h 2020-11-09 13:59:57 +0000 |
99 | @@ -18,10 +18,11 @@ |
100 | |
101 | namespace LTL { |
102 | |
103 | + template <bool SaveTrace> |
104 | class TarjanModelChecker : public ModelChecker { |
105 | public: |
106 | TarjanModelChecker(const PetriEngine::PetriNet &net, const Condition_ptr &cond) |
107 | - : ModelChecker(net, cond), successorGenerator(net, cond), factory(net, successorGenerator.initial_buchi_state()), |
108 | + : ModelChecker(net, cond), factory(net, successorGenerator->initial_buchi_state()), |
109 | seen(net, 0, (int) net.numberOfPlaces() + 1) { |
110 | chash.fill(std::numeric_limits<idx_t>::max()); |
111 | } |
112 | @@ -31,45 +32,46 @@ |
113 | private: |
114 | using State = LTL::Structures::ProductState; |
115 | using idx_t = size_t; |
116 | + static constexpr idx_t HashSz = 4096; |
117 | |
118 | - LTL::ProductSuccessorGenerator successorGenerator; |
119 | LTL::Structures::ProductStateFactory factory; |
120 | |
121 | PetriEngine::Structures::StateSet seen; |
122 | std::unordered_set<idx_t> store; |
123 | - //PetriEngine::Structures::StateSet store; |
124 | |
125 | - static constexpr idx_t HashSz = 4096; |
126 | std::array<idx_t, HashSz> chash; |
127 | - inline idx_t hash_search(idx_t stateid) { |
128 | - idx_t idx = chash[hash(stateid)]; |
129 | - while (idx != stateid && idx != std::numeric_limits<idx_t>::max()) { |
130 | - idx = cstack[idx].next; |
131 | - } |
132 | - return idx; |
133 | - } |
134 | |
135 | - inline idx_t hash(idx_t id) { |
136 | + static inline idx_t hash(idx_t id) { |
137 | return id % HashSz; |
138 | } |
139 | |
140 | - struct CStack { |
141 | + struct PlainCEntry { |
142 | size_t lowlink; |
143 | size_t stateid; |
144 | size_t next = std::numeric_limits<idx_t>::max(); |
145 | |
146 | - CStack(size_t lowlink, size_t stateid, size_t next) : lowlink(lowlink), stateid(stateid), next(next) {} |
147 | - }; |
148 | - |
149 | - struct DStack { |
150 | + PlainCEntry(size_t lowlink, size_t stateid, size_t next) : lowlink(lowlink), stateid(stateid), next(next) {} |
151 | + }; |
152 | + |
153 | + struct TracableCEntry : PlainCEntry { |
154 | + idx_t lowsource = std::numeric_limits<size_t>::max(); |
155 | + uint32_t sourcetrans; |
156 | + |
157 | + TracableCEntry(size_t lowlink, size_t stateid, size_t next) : PlainCEntry(lowlink, stateid, next) {} |
158 | + }; |
159 | + |
160 | + using CEntry = std::conditional_t<SaveTrace, |
161 | + TracableCEntry, |
162 | + PlainCEntry>; |
163 | + |
164 | + struct DEntry { |
165 | size_t pos; |
166 | - uint32_t nexttrans = -1; |
167 | - std::optional<std::vector<size_t>> neighbors; |
168 | + successor_info sucinfo; |
169 | }; |
170 | |
171 | |
172 | - std::vector<CStack> cstack; |
173 | - std::stack<DStack> dstack; |
174 | + std::vector<CEntry> cstack; |
175 | + std::stack<DEntry> dstack; |
176 | std::stack<idx_t> astack; |
177 | bool violation = false; |
178 | |
179 | @@ -79,8 +81,10 @@ |
180 | |
181 | void update(idx_t to); |
182 | |
183 | - bool nexttrans(State &state, DStack &delem); |
184 | + bool nexttrans(State &state, State& parent, DEntry &delem); |
185 | }; |
186 | +extern template class TarjanModelChecker<true>; |
187 | +extern template class TarjanModelChecker<false>; |
188 | } |
189 | |
190 | #endif //VERIFYPN_TARJANMODELCHECKER_H |
191 | |
192 | === modified file 'include/LTL/ProductSuccessorGenerator.h' |
193 | --- include/LTL/ProductSuccessorGenerator.h 2020-10-16 11:20:30 +0000 |
194 | +++ include/LTL/ProductSuccessorGenerator.h 2020-11-09 13:59:57 +0000 |
195 | @@ -11,13 +11,63 @@ |
196 | #include "LTL/BuchiSuccessorGenerator.h" |
197 | #include "LTL/LTLToBuchi.h" |
198 | |
199 | + |
200 | namespace LTL { |
201 | + /** |
202 | + * type holding sufficient information to resume successor generation for a state from a given point. |
203 | + */ |
204 | + struct successor_info { |
205 | + uint32_t pcounter; |
206 | + uint32_t tcounter; |
207 | + size_t buchi_state; |
208 | + size_t last_state; |
209 | + |
210 | + friend bool operator==(const successor_info &lhs, const successor_info &rhs) { |
211 | + return lhs.pcounter == rhs.pcounter && |
212 | + lhs.tcounter == rhs.tcounter && |
213 | + lhs.buchi_state == rhs.buchi_state && |
214 | + lhs.last_state == rhs.last_state; |
215 | + } |
216 | + |
217 | + friend bool operator!=(const successor_info &lhs, const successor_info &rhs) { |
218 | + return !(rhs == lhs); |
219 | + } |
220 | + |
221 | + inline bool has_pcounter() const { |
222 | + return pcounter != NoPCounter; |
223 | + } |
224 | + |
225 | + inline bool has_tcounter() const { |
226 | + return tcounter != NoTCounter; |
227 | + } |
228 | + |
229 | + inline bool has_buchistate() const { |
230 | + return buchi_state != NoBuchiState; |
231 | + } |
232 | + |
233 | + inline bool has_prev_state() const { |
234 | + return last_state != NoLastState; |
235 | + } |
236 | + |
237 | + static constexpr auto NoPCounter = 0; |
238 | + static constexpr auto NoTCounter = std::numeric_limits<uint32_t>::max(); |
239 | + static constexpr auto NoBuchiState = std::numeric_limits<size_t>::max(); |
240 | + static constexpr auto NoLastState = std::numeric_limits<size_t>::max(); |
241 | + }; |
242 | + |
243 | + constexpr successor_info initial_suc_info{ |
244 | + successor_info::NoPCounter, |
245 | + successor_info::NoTCounter, |
246 | + successor_info::NoBuchiState, |
247 | + successor_info::NoLastState |
248 | + }; |
249 | + |
250 | class ProductSuccessorGenerator : public PetriEngine::SuccessorGenerator { |
251 | public: |
252 | + |
253 | ProductSuccessorGenerator(const PetriEngine::PetriNet &net, |
254 | - const PetriEngine::PQL::Condition_ptr& cond) |
255 | - : PetriEngine::SuccessorGenerator(net), buchi(makeBuchiAutomaton(cond)) |
256 | - {} |
257 | + const PetriEngine::PQL::Condition_ptr &cond) |
258 | + : PetriEngine::SuccessorGenerator(net), buchi(makeBuchiAutomaton(cond)) {} |
259 | |
260 | [[nodiscard]] size_t initial_buchi_state() const { return buchi.initial_state_number(); }; |
261 | |
262 | @@ -43,8 +93,21 @@ |
263 | } |
264 | } |
265 | |
266 | - protected: |
267 | - bool next(LTL::Structures::ProductState &write, uint32_t &tindex); |
268 | + /** |
269 | + * prepare a state for successor generation, starting from specific point in iteration |
270 | + * @param state the source state to generate successors from |
271 | + * @param sucinfo the point in the iteration to start from, as returned by `next`. |
272 | + */ |
273 | + void prepare(const LTL::Structures::ProductState *state, const successor_info &sucinfo); |
274 | + |
275 | + /** |
276 | + * compute the next successor from the last state that was sent to `prepare`. |
277 | + * @param[out] state the state to write |
278 | + * @param[out] sucinfo checkpoint information from which iteration can later be resumed. |
279 | + * @return `true` if a successor was successfully generated, `false` otherwise. |
280 | + * @warning do not use the same State for both prepare and next, this will cause wildly incorrect behaviour! |
281 | + */ |
282 | + bool next(Structures::ProductState &state, successor_info &sucinfo); |
283 | |
284 | private: |
285 | BuchiSuccessorGenerator buchi; |
286 | |
287 | === modified file 'include/LTL/Structures/ProductState.h' |
288 | --- include/LTL/Structures/ProductState.h 2020-10-16 11:20:30 +0000 |
289 | +++ include/LTL/Structures/ProductState.h 2020-11-09 13:59:57 +0000 |
290 | @@ -48,6 +48,8 @@ |
291 | getBuchiState() == rhs.getBuchiState();*/ |
292 | } |
293 | |
294 | + size_t size() const { return buchi_state_idx + 1; } |
295 | + |
296 | bool operator!=(const ProductState &rhs) const { |
297 | return !(rhs == *this); |
298 | } |
299 | |
300 | === modified file 'include/PetriEngine/PQL/Expressions.h' |
301 | --- include/PetriEngine/PQL/Expressions.h 2020-09-23 12:26:04 +0000 |
302 | +++ include/PetriEngine/PQL/Expressions.h 2020-11-09 13:59:57 +0000 |
303 | @@ -533,7 +533,7 @@ |
304 | // TODO implement |
305 | assert(false); std::cerr << "TODO implement" << std::endl; exit(0); |
306 | } |
307 | - bool containsNext() const override { return true; } |
308 | + bool containsNext() const override { return _cond->containsNext(); } |
309 | virtual bool isLoopSensitive() const override { return true; } |
310 | void visit(Visitor&) const override; |
311 | private: |
312 | @@ -569,7 +569,7 @@ |
313 | // TODO implement |
314 | assert(false); std::cerr << "TODO implement" << std::endl; exit(0); |
315 | } |
316 | - bool containsNext() const override { return true; } |
317 | + bool containsNext() const override { return _cond->containsNext(); } |
318 | virtual bool isLoopSensitive() const override { return true; } |
319 | void visit(Visitor&) const override; |
320 | private: |
321 | |
322 | === modified file 'include/PetriEngine/SuccessorGenerator.h' |
323 | --- include/PetriEngine/SuccessorGenerator.h 2020-10-16 11:20:30 +0000 |
324 | +++ include/PetriEngine/SuccessorGenerator.h 2020-11-09 13:59:57 +0000 |
325 | @@ -60,16 +60,20 @@ |
326 | */ |
327 | void producePostset(Structures::State& write, uint32_t t); |
328 | |
329 | + size_t last_transition() const { return _suc_tcounter == std::numeric_limits<uint32_t>::max() ? std::numeric_limits<uint32_t>::max() : _suc_tcounter - 1; } |
330 | + |
331 | protected: |
332 | const PetriNet& _net; |
333 | |
334 | bool next(Structures::State &write, uint32_t &tindex); |
335 | |
336 | const Structures::State* _parent; |
337 | -private: |
338 | + |
339 | uint32_t _suc_pcounter; |
340 | uint32_t _suc_tcounter; |
341 | |
342 | +private: |
343 | + |
344 | friend class ReducingSuccessorGenerator; |
345 | |
346 | }; |
347 | |
348 | === modified file 'src/LTL/LTL_algorithm/LTLToBuchi.cpp' |
349 | --- src/LTL/LTL_algorithm/LTLToBuchi.cpp 2020-10-16 11:20:30 +0000 |
350 | +++ src/LTL/LTL_algorithm/LTLToBuchi.cpp 2020-11-09 13:59:57 +0000 |
351 | @@ -29,8 +29,6 @@ |
352 | |
353 | void _accept(const PetriEngine::PQL::OrCondition *element) override; |
354 | |
355 | - //void _accept(const PetriEngine::PQL::CompareConjunction *element) override; |
356 | - |
357 | void _accept(const PetriEngine::PQL::LessThanCondition *element) override; |
358 | |
359 | void _accept(const PetriEngine::PQL::LessThanOrEqualCondition *element) override; |
360 | @@ -63,7 +61,7 @@ |
361 | |
362 | public: |
363 | |
364 | - FormulaToSpotSyntax(std::ostream &os = std::cout) |
365 | + explicit FormulaToSpotSyntax(std::ostream &os = std::cout) |
366 | : PetriEngine::PQL::QueryPrinter(os) {} |
367 | |
368 | auto begin() const { |
369 | @@ -147,88 +145,76 @@ |
370 | |
371 | void FormulaToSpotSyntax::_accept(const PetriEngine::PQL::LiteralExpr *element) { |
372 | assert(false); |
373 | - std::cerr << "LiteralExpr should not be visited by Spot serialiezr" << std::endl; |
374 | + std::cerr << "LiteralExpr should not be visited by Spot serializer" << std::endl; |
375 | exit(1); |
376 | //make_atomic_prop(element->shared_from_this()); |
377 | } |
378 | |
379 | void FormulaToSpotSyntax::_accept(const PetriEngine::PQL::PlusExpr *element) { |
380 | assert(false); |
381 | - std::cerr << "PlusExpr should not be visited by Spot serialiezr" << std::endl; |
382 | + std::cerr << "PlusExpr should not be visited by Spot serializer" << std::endl; |
383 | exit(1); |
384 | //make_atomic_prop(element->shared_from_this()); |
385 | } |
386 | |
387 | void FormulaToSpotSyntax::_accept(const PetriEngine::PQL::MultiplyExpr *element) { |
388 | assert(false); |
389 | - std::cerr << "MultiplyExpr should not be visited by Spot serialiezr" << std::endl; |
390 | + std::cerr << "MultiplyExpr should not be visited by Spot serializer" << std::endl; |
391 | exit(1); |
392 | //make_atomic_prop(element->shared_from_this()); |
393 | } |
394 | |
395 | void FormulaToSpotSyntax::_accept(const PetriEngine::PQL::MinusExpr *element) { |
396 | assert(false); |
397 | - std::cerr << "MinusExpr should not be visited by Spot serialiezr" << std::endl; |
398 | + std::cerr << "MinusExpr should not be visited by Spot serializer" << std::endl; |
399 | exit(1); |
400 | //make_atomic_prop(element->shared_from_this()); |
401 | } |
402 | |
403 | void FormulaToSpotSyntax::_accept(const PetriEngine::PQL::SubtractExpr *element) { |
404 | assert(false); |
405 | - std::cerr << "LiteralExpr should not be visited by Spot serialiezr" << std::endl; |
406 | + std::cerr << "LiteralExpr should not be visited by Spot serializer" << std::endl; |
407 | exit(1); |
408 | //make_atomic_prop(element->shared_from_this()); |
409 | } |
410 | |
411 | void FormulaToSpotSyntax::_accept(const PetriEngine::PQL::IdentifierExpr *element) { |
412 | assert(false); |
413 | - std::cerr << "IdentifierExpr should not be visited by Spot serialiezr" << std::endl; |
414 | + std::cerr << "IdentifierExpr should not be visited by Spot serializer" << std::endl; |
415 | exit(1); |
416 | //make_atomic_prop(element->shared_from_this()); |
417 | } |
418 | |
419 | - |
420 | - std::string toSpotFormat(const QueryItem &query) { |
421 | - std::stringstream ss; |
422 | - toSpotFormat(query, ss); |
423 | - return ss.str(); |
424 | - } |
425 | - |
426 | - void toSpotFormat(const QueryItem &query, std::ostream &os) { |
427 | - FormulaToSpotSyntax spotConverter{os}; |
428 | - // FIXME nasty hack for top-level query, should be fixed elsewhere (e.g. asLTL) |
429 | - auto top_quant = dynamic_cast<SimpleQuantifierCondition *>(query.query.get()); |
430 | - (*top_quant)[0]->visit(spotConverter); |
431 | - } |
432 | - |
433 | BuchiSuccessorGenerator makeBuchiAutomaton(const Condition_ptr &query) { |
434 | std::stringstream ss; |
435 | FormulaToSpotSyntax spotConverter{ss}; |
436 | query->visit(spotConverter); |
437 | - |
438 | const std::string spotFormula = "!(" + ss.str() + ")"; |
439 | #ifdef PRINTF_DEBUG |
440 | std::cerr << "ORIG FORMULA: \n " << ss.str() << std::endl; |
441 | std::cerr << "SPOT FORMULA: \n " << spotFormula << std::endl; |
442 | #endif |
443 | spot::formula formula = spot::parse_formula(spotFormula); |
444 | - spot::bdd_dict_ptr bdd = spot::make_bdd_dict(); |
445 | - auto translator = spot::translator(bdd); |
446 | - translator.set_pref(spot::postprocessor::Complete |
447 | - | spot::postprocessor::SBAcc); |
448 | + spot::translator translator; |
449 | + translator.set_type(spot::postprocessor::BA); |
450 | + translator.set_pref(spot::postprocessor::Complete); |
451 | spot::twa_graph_ptr automaton = translator.run(formula); |
452 | #ifdef PRINTF_DEBUG |
453 | automaton->get_graph().dump_storage(std::cerr); |
454 | spot::print_dot(std::cerr, automaton); |
455 | - bdd->dump(std::cerr); |
456 | #endif |
457 | std::unordered_map<int, AtomicProposition> ap_map; |
458 | + // bind PQL expressions to the atomic proposition IDs used by spot. |
459 | + // the resulting map can be indexed using variables mentioned on edges of the created Büchi automaton. |
460 | for (const auto &apinfo : spotConverter) { |
461 | int varnum = automaton->register_ap(apinfo.text); |
462 | ap_map[varnum] = apinfo; |
463 | } |
464 | +#ifdef PRINTF_DEBUG |
465 | + automaton->get_dict()->dump(std::cerr); |
466 | +#endif |
467 | |
468 | - return BuchiSuccessorGenerator{Structures::BuchiAutomaton{automaton, ap_map}}; |
469 | + return BuchiSuccessorGenerator{Structures::BuchiAutomaton{std::move(automaton), std::move(ap_map)}}; |
470 | } |
471 | |
472 | -} |
473 | \ No newline at end of file |
474 | +} |
475 | |
476 | === modified file 'src/LTL/LTL_algorithm/NestedDepthFirstSearch.cpp' |
477 | --- src/LTL/LTL_algorithm/NestedDepthFirstSearch.cpp 2020-10-19 12:35:11 +0000 |
478 | +++ src/LTL/LTL_algorithm/NestedDepthFirstSearch.cpp 2020-11-09 13:59:57 +0000 |
479 | @@ -20,100 +20,106 @@ |
480 | |
481 | bool NestedDepthFirstSearch::isSatisfied() { |
482 | dfs(); |
483 | +#ifdef _PRINTF_DEBUG |
484 | + std::cout << "discovered " << _discovered << " states." << std::endl; |
485 | + std::cout << "mark1 size: " << mark1.size() << "\tmark2 size: " << mark2.size() << std::endl; |
486 | +#endif |
487 | return !violation; |
488 | } |
489 | |
490 | void NestedDepthFirstSearch::dfs() { |
491 | std::stack<size_t> call_stack; |
492 | - |
493 | - PetriEngine::Structures::StateSet states{net,0, (int)net.numberOfPlaces() + 1}; |
494 | - PetriEngine::Structures::DFSQueue todo{&states}; |
495 | + std::stack<StackEntry> todo; |
496 | |
497 | State working = factory.newState(); |
498 | - PQL::DistanceContext ctx{&net, working.marking()}; |
499 | State curState = factory.newState(); |
500 | + |
501 | { |
502 | std::vector<State> initial_states; |
503 | successorGenerator->makeInitialState(initial_states); |
504 | for (auto &state : initial_states) { |
505 | auto res = states.add(state); |
506 | assert(res.first); |
507 | - todo.push(res.second, ctx, formula); |
508 | + todo.push(StackEntry{res.second, initial_suc_info}); |
509 | + _discovered++; |
510 | } |
511 | } |
512 | |
513 | - while (todo.top(curState)) { |
514 | - |
515 | - if (!call_stack.empty() && states.lookup(curState).second == call_stack.top()) { |
516 | + while (!todo.empty()) { |
517 | + auto &top = todo.top(); |
518 | + states.decode(curState, top.id); |
519 | + successorGenerator->prepare(&curState, top.sucinfo); |
520 | + if (top.sucinfo.has_prev_state()) { |
521 | + states.decode(working, top.sucinfo.last_state); |
522 | + } |
523 | + if (!successorGenerator->next(working, top.sucinfo)) { |
524 | + // no successor |
525 | + todo.pop(); |
526 | if (successorGenerator->isAccepting(curState)) { |
527 | seed = &curState; |
528 | ndfs(curState); |
529 | - if (violation) |
530 | - return; |
531 | + if (violation) return; |
532 | } |
533 | - todo.pop(curState); |
534 | - call_stack.pop(); |
535 | } else { |
536 | - call_stack.push(states.add(curState).second); |
537 | - if (!mark1.add(curState).first) { |
538 | - continue; |
539 | - } |
540 | - successorGenerator->prepare(&curState); |
541 | -#ifdef PRINTF_DEBUG |
542 | - std::cerr << "curState:\n"; |
543 | - dump_state(curState); |
544 | -#endif |
545 | - while (successorGenerator->next(working)) { |
546 | -#ifdef PRINTF_DEBUG |
547 | - std::cerr << "working:\n"; |
548 | - dump_state(working); |
549 | -#endif |
550 | - auto r = states.add(working); |
551 | - todo.push(r.second, ctx, formula); |
552 | +#ifdef PRINTF_DEBUG |
553 | + dump_state(working); |
554 | +#endif |
555 | + auto[_, stateid] = states.add(working); |
556 | + auto[it, is_new] = mark1.insert(stateid); |
557 | + top.sucinfo.last_state = stateid; |
558 | + if (is_new) { |
559 | + _discovered++; |
560 | + todo.push(StackEntry{stateid, initial_suc_info}); |
561 | } |
562 | } |
563 | } |
564 | } |
565 | |
566 | |
567 | - void NestedDepthFirstSearch::ndfs(State& state) { |
568 | - PetriEngine::Structures::StateSet states{net, 0, (int)net.numberOfPlaces() + 1}; |
569 | - PetriEngine::Structures::DFSQueue todo{&states}; |
570 | + void NestedDepthFirstSearch::ndfs(State &state) { |
571 | +#ifdef PRINTF_DEBUG |
572 | + std::cerr << "ENTERING NDFS" << std::endl; |
573 | +#endif |
574 | + std::stack<StackEntry> todo; |
575 | |
576 | State working = factory.newState(); |
577 | State curState = factory.newState(); |
578 | |
579 | - PQL::DistanceContext ctx{&net, state.marking()}; |
580 | - |
581 | - todo.push(states.add(state).second, ctx, formula); |
582 | - |
583 | - while (todo.pop(curState)) { |
584 | - if (!mark2.add(curState).first) { |
585 | - continue; |
586 | + todo.push(StackEntry{states.add(state).second, initial_suc_info}); |
587 | + |
588 | + while (!todo.empty()) { |
589 | + auto &top = todo.top(); |
590 | + states.decode(curState, top.id); |
591 | + successorGenerator->prepare(&curState, top.sucinfo); |
592 | + if (top.sucinfo.has_prev_state()) { |
593 | + states.decode(working, top.sucinfo.last_state); |
594 | } |
595 | - |
596 | - successorGenerator->prepare(&curState); |
597 | -#ifdef PRINTF_DEBUG |
598 | - std::cerr << "curState:\n"; |
599 | - dump_state(curState); |
600 | -#endif |
601 | - while (successorGenerator->next(working)) { |
602 | -#ifdef PRINTF_DEBUG |
603 | - std::cerr << "working:\n"; |
604 | + if (!successorGenerator->next(working, top.sucinfo)) { |
605 | + todo.pop(); |
606 | + } else { |
607 | +#ifdef PRINTF_DEBUG |
608 | dump_state(working); |
609 | #endif |
610 | if (working == *seed) { |
611 | -#ifdef PRINTF_DEBUG |
612 | +#ifdef _PRINTF_DEBUG |
613 | std::cerr << "seed:\n "; dump_state(*seed); |
614 | std::cerr << "working:\n "; dump_state(working); |
615 | #endif |
616 | violation = true; |
617 | return; |
618 | } |
619 | - auto r = states.add(working); |
620 | - todo.push(r.second, ctx, formula); |
621 | + auto[_, stateid] = states.add(working); |
622 | + auto[it, is_new] = mark2.insert(stateid); |
623 | + top.sucinfo.last_state = stateid; |
624 | + if (is_new) { |
625 | + _discovered++; |
626 | + todo.push(StackEntry{stateid, initial_suc_info}); |
627 | + } |
628 | + |
629 | } |
630 | } |
631 | - |
632 | +#ifdef PRINTF_DEBUG |
633 | + std::cerr << "LEAVING NDFS" << std::endl; |
634 | +#endif |
635 | } |
636 | } |
637 | \ No newline at end of file |
638 | |
639 | === modified file 'src/LTL/LTL_algorithm/ProductSuccessorGenerator.cpp' |
640 | --- src/LTL/LTL_algorithm/ProductSuccessorGenerator.cpp 2020-10-16 11:20:30 +0000 |
641 | +++ src/LTL/LTL_algorithm/ProductSuccessorGenerator.cpp 2020-11-09 13:59:57 +0000 |
642 | @@ -29,6 +29,27 @@ |
643 | fresh_marking = true; |
644 | } |
645 | |
646 | + void ProductSuccessorGenerator::prepare(const LTL::Structures::ProductState *state, const successor_info &sucinfo) { |
647 | + SuccessorGenerator::prepare(state); |
648 | + buchi.prepare(state->getBuchiState()); |
649 | + buchi_parent = state->getBuchiState(); |
650 | + fresh_marking = sucinfo.pcounter == 0 && sucinfo.tcounter == std::numeric_limits<uint32_t>::max(); |
651 | + _suc_pcounter = sucinfo.pcounter; |
652 | + _suc_tcounter = sucinfo.tcounter; |
653 | + if (!fresh_marking) { |
654 | + assert(sucinfo.buchi_state != std::numeric_limits<size_t>::max()); |
655 | + // spool Büchi successors until last state found. |
656 | + // TODO is there perhaps a good way to avoid this, perhaps using raw edge vector? |
657 | + // Caveat: it seems like there usually are not that many successors, so this is probably cheap regardless |
658 | + size_t tmp; |
659 | + while (buchi.next(tmp, cond)) { |
660 | + if (tmp == sucinfo.buchi_state) { |
661 | + break; |
662 | + } |
663 | + } |
664 | + } |
665 | + } |
666 | + |
667 | bool ProductSuccessorGenerator::next(LTL::Structures::ProductState &state) { |
668 | if (fresh_marking) { |
669 | fresh_marking = false; |
670 | @@ -75,14 +96,16 @@ |
671 | |
672 | bool ProductSuccessorGenerator::guard_valid(const PetriEngine::Structures::State &state, bdd bdd) { |
673 | EvaluationContext ctx{state.marking(), &_net}; |
674 | - while (!(bdd == bddtrue || bdd == bddfalse)) { |
675 | + // IDs 0 and 1 are false and true atoms, respectively |
676 | + while (bdd.id() > 1/*!(bdd == bddtrue || bdd == bddfalse)*/) { |
677 | + // find variable to test, and test it |
678 | size_t var = bdd_var(bdd); |
679 | Condition::Result res = buchi.getExpression(var)->evaluate(ctx); |
680 | switch (res) { |
681 | case Condition::RUNKNOWN: |
682 | std::cerr << "Unexpected unknown answer from evaluating query!\n"; |
683 | assert(false); |
684 | - exit(0); |
685 | + exit(1); |
686 | break; |
687 | case Condition::RFALSE: |
688 | bdd = bdd_low(bdd); |
689 | @@ -95,23 +118,33 @@ |
690 | return bdd == bddtrue; |
691 | } |
692 | |
693 | - bool ProductSuccessorGenerator::next(Structures::ProductState &state, uint32_t &tindex) { |
694 | + bool ProductSuccessorGenerator::next(Structures::ProductState &state, successor_info &sucinfo) { |
695 | + auto update_sucinfo = [&]() { |
696 | + sucinfo.pcounter = _suc_pcounter; |
697 | + sucinfo.tcounter = _suc_tcounter; |
698 | + sucinfo.buchi_state = state.getBuchiState(); |
699 | + }; |
700 | + |
701 | if (fresh_marking) { |
702 | fresh_marking = false; |
703 | - if (!SuccessorGenerator::next(state, tindex)) { |
704 | - // This is a fresh marking, so if there is no more successors for the state the state is deadlocked. |
705 | + if (!SuccessorGenerator::next(state)) { |
706 | + // This is a fresh marking, so if there are no more successors for the state the state is deadlocked. |
707 | // The semantics for deadlock is to just loop the marking so return true without changing the value of state. |
708 | - // This assumes SuccessorGenerator::next only modifies &state if there is a successor. |
709 | + std::copy(_parent->marking(), _parent->marking() + state.buchi_state_idx + 1, state.marking()); |
710 | } |
711 | } |
712 | if (next_buchi_succ(state)) { |
713 | + update_sucinfo(); |
714 | return true; |
715 | } |
716 | - // No valid transition in Büchi automaton for current marking; |
717 | - // Try next marking(s) and see if we find a successor. |
718 | + // No valid transition in Büchi automaton for current marking; |
719 | + // Try next marking(s) and see if we find a successor. |
720 | else { |
721 | - while (SuccessorGenerator::next(state, tindex)) { |
722 | + while (SuccessorGenerator::next(state)) { |
723 | + // reset buchi successors |
724 | + buchi.prepare(buchi_parent); |
725 | if (next_buchi_succ(state)) { |
726 | + update_sucinfo(); |
727 | return true; |
728 | } |
729 | } |
730 | |
731 | === modified file 'src/LTL/LTL_algorithm/TarjanModelChecker.cpp' |
732 | --- src/LTL/LTL_algorithm/TarjanModelChecker.cpp 2020-10-19 12:35:11 +0000 |
733 | +++ src/LTL/LTL_algorithm/TarjanModelChecker.cpp 2020-11-09 13:59:57 +0000 |
734 | @@ -7,72 +7,123 @@ |
735 | |
736 | #include "LTL/LTL_algorithm/TarjanModelChecker.h" |
737 | |
738 | +#undef PRINTF_DEBUG |
739 | namespace LTL { |
740 | |
741 | - |
742 | -#ifdef PRINTF_DEBUG |
743 | - |
744 | - inline void _dump_state(const LTL::Structures::ProductState &state, int nplaces = -1) { |
745 | - if (nplaces == -1) nplaces = state.buchi_state_idx; |
746 | + inline void _dump_state(const LTL::Structures::ProductState &state) { |
747 | std::cerr << "marking: "; |
748 | std::cerr << state.marking()[0]; |
749 | - for (int i = 1; i <= nplaces; ++i) { |
750 | + for (int i = 1; i < state.size(); ++i) { |
751 | std::cerr << ", " << state.marking()[i]; |
752 | } |
753 | std::cerr << std::endl; |
754 | } |
755 | |
756 | -#endif |
757 | - |
758 | - bool LTL::TarjanModelChecker::isSatisfied() { |
759 | - { |
760 | - std::vector<State> initial_states; |
761 | - successorGenerator.makeInitialState(initial_states); |
762 | - for (auto &state : initial_states) { |
763 | - seen.add(state); |
764 | + template<bool SaveTrace> |
765 | + bool TarjanModelChecker<SaveTrace>::isSatisfied() { |
766 | + std::vector<State> initial_states; |
767 | + successorGenerator->makeInitialState(initial_states); |
768 | + State working = factory.newState(); |
769 | + State parent = factory.newState(); |
770 | + for (auto &state : initial_states) { |
771 | + auto res = seen.add(state); |
772 | + if (res.first) { |
773 | push(state); |
774 | } |
775 | - } |
776 | - State working = factory.newState(); |
777 | - while (!dstack.empty() && !violation) { |
778 | - DStack &dtop = dstack.top(); |
779 | - if (!nexttrans(working, dtop)) { |
780 | - pop(); |
781 | - continue; |
782 | - } |
783 | - // get ID of transition taken (nexttrans = lasttrans + 1) |
784 | - idx_t stateid = (*dtop.neighbors)[dtop.nexttrans - 1]; |
785 | - |
786 | - // lookup successor in 'hash' table |
787 | - auto p = chash[hash(stateid)]; |
788 | - while (p != std::numeric_limits<idx_t>::max() && cstack[p].stateid != stateid) { |
789 | - p = cstack[p].next; |
790 | - } |
791 | - if (p != std::numeric_limits<idx_t>::max()) { |
792 | - // we found the successor! update lowlinks etc |
793 | - update(p); |
794 | - continue; |
795 | - } |
796 | - if (store.find(stateid) == std::end(store)) { |
797 | - push(working); |
798 | + while (!dstack.empty() && !violation) { |
799 | + DEntry &dtop = dstack.top(); |
800 | + if (!nexttrans(working, parent, dtop)) { |
801 | + pop(); |
802 | + continue; |
803 | + } |
804 | + idx_t stateid = seen.add(working).second; |
805 | + dtop.sucinfo.last_state = stateid; |
806 | + |
807 | + // lookup successor in 'hash' table |
808 | + auto p = chash[hash(stateid)]; |
809 | + while (p != std::numeric_limits<idx_t>::max() && cstack[p].stateid != stateid) { |
810 | + p = cstack[p].next; |
811 | + } |
812 | + if (p != std::numeric_limits<idx_t>::max()) { |
813 | + // we found the successor, i.e. there's a loop! |
814 | + // now update lowlinks and check whether the loop contains an accepting state |
815 | + update(p); |
816 | + continue; |
817 | + } |
818 | + if (store.find(stateid) == std::end(store)) { |
819 | + push(working); |
820 | + } |
821 | + } |
822 | + if constexpr (SaveTrace) { |
823 | + if (violation) { |
824 | + State next = factory.newState(); |
825 | + std::cerr << "Printing trace: " << std::endl; |
826 | + std::vector<DEntry> rev; |
827 | + auto sz = dstack.size(); |
828 | + // dump stack to vector to allow iteration |
829 | + for (int i = 0; i < sz; ++i) { |
830 | + rev.push_back(dstack.top()); |
831 | + dstack.pop(); |
832 | + } |
833 | + idx_t pos = 0; |
834 | + // print dstack in-order. rev[0] is dstack.top(), so loop vector in reverse |
835 | + for (int i = rev.size() - 1; i >= 0; --i) { |
836 | + pos = rev[i].pos; |
837 | + seen.decode(parent, cstack[pos].stateid); |
838 | + _dump_state(parent); |
839 | + cstack[pos].lowlink = std::numeric_limits<idx_t>::max(); |
840 | + if (i > 0) { |
841 | + // print transition to next state |
842 | + seen.decode(next, cstack[rev[i - 1].pos].stateid); |
843 | + successorGenerator->prepare(&parent); |
844 | + while (successorGenerator->next(working)) { |
845 | + if (working == next) { |
846 | + std::cerr << net.transitionNames()[successorGenerator->last_transition()] |
847 | + << std::endl; |
848 | + break; |
849 | + } |
850 | + } |
851 | + } |
852 | + } |
853 | + |
854 | + // follow lowsource until back in dstack |
855 | + pos = cstack[pos].lowsource; |
856 | + if (cstack[pos].lowlink != std::numeric_limits<idx_t>::max()) { |
857 | + std::cerr << "Printing looping part\n"; |
858 | + } |
859 | + while (cstack[pos].lowlink != std::numeric_limits<idx_t>::max()) { |
860 | + seen.decode(parent, cstack[pos].stateid); |
861 | + _dump_state(parent); |
862 | + pos = cstack[pos].lowsource; |
863 | + } |
864 | + } |
865 | } |
866 | } |
867 | return !violation; |
868 | } |
869 | |
870 | - void TarjanModelChecker::push(State &state) { |
871 | + /** |
872 | + * Push a state to the various stacks. |
873 | + * @param state |
874 | + */ |
875 | + template<bool SaveTrace> |
876 | + void TarjanModelChecker<SaveTrace>::push(State &state) { |
877 | const auto res = seen.add(state); |
878 | const auto ctop = static_cast<idx_t>(cstack.size()); |
879 | const auto h = hash(res.second); |
880 | cstack.emplace_back(ctop, res.second, chash[h]); |
881 | + if constexpr (SaveTrace) { |
882 | + cstack.back().lowsource = ctop; |
883 | + } |
884 | chash[h] = ctop; |
885 | - dstack.push({ctop}); |
886 | - if (successorGenerator.isAccepting(state)) { |
887 | + dstack.push(DEntry{ctop, initial_suc_info}); |
888 | + if (successorGenerator->isAccepting(state)) { |
889 | astack.push(ctop); |
890 | } |
891 | } |
892 | |
893 | - void TarjanModelChecker::pop() { |
894 | + template<bool SaveTrace> |
895 | + void TarjanModelChecker<SaveTrace>::pop() { |
896 | const size_t p = dstack.top().pos; |
897 | dstack.pop(); |
898 | if (cstack[p].lowlink == p) { |
899 | @@ -91,42 +142,45 @@ |
900 | } |
901 | } |
902 | |
903 | - void TarjanModelChecker::update(idx_t to) { |
904 | + template<bool SaveTrace> |
905 | + void TarjanModelChecker<SaveTrace>::update(idx_t to) { |
906 | const auto from = dstack.top().pos; |
907 | if (cstack[to].lowlink <= cstack[from].lowlink) { |
908 | + // we have found a loop into earlier seen component cstack[to].lowlink. |
909 | + // if this earlier component was found before an accepting state, |
910 | + // we have found an accepting loop and thus a violation. |
911 | violation = (!astack.empty() && to <= astack.top()); |
912 | cstack[from].lowlink = cstack[to].lowlink; |
913 | + if constexpr (SaveTrace) { |
914 | + cstack[from].lowsource = to; |
915 | + } |
916 | } |
917 | } |
918 | |
919 | - bool TarjanModelChecker::nexttrans(State &state, TarjanModelChecker::DStack &delem) { |
920 | - if (!delem.neighbors) { |
921 | - delem.neighbors = std::vector<idx_t>(); |
922 | - delem.nexttrans = 0; |
923 | - State src = factory.newState(); |
924 | - State dst = factory.newState(); |
925 | - seen.decode(src, cstack[delem.pos].stateid); |
926 | - successorGenerator.prepare(&src); |
927 | - while (successorGenerator.next(dst)) { |
928 | - auto res = seen.add(dst); |
929 | + template<bool SaveTrace> |
930 | + bool TarjanModelChecker<SaveTrace>::nexttrans(State &state, State &parent, TarjanModelChecker::DEntry &delem) { |
931 | + seen.decode(parent, cstack[delem.pos].stateid); |
932 | #ifdef PRINTF_DEBUG |
933 | - std::cerr << "adding state\n"; |
934 | - _dump_state(dst); |
935 | + std::cerr << "loaded parent\n "; |
936 | + _dump_state(parent); |
937 | #endif |
938 | - delem.neighbors->push_back(res.second); |
939 | - } |
940 | + successorGenerator->prepare(&parent, delem.sucinfo); |
941 | + if (delem.sucinfo.has_prev_state()) { |
942 | + seen.decode(state, delem.sucinfo.last_state); |
943 | } |
944 | - if (delem.nexttrans == delem.neighbors->size()) { |
945 | - return false; |
946 | - } else { |
947 | - seen.decode(state, (*delem.neighbors)[delem.nexttrans]); |
948 | + auto res = successorGenerator->next(state, delem.sucinfo); |
949 | #ifdef PRINTF_DEBUG |
950 | - std::cerr << "loaded state\n"; |
951 | + if (res) { |
952 | + std::cerr << "going to state\n"; |
953 | _dump_state(state); |
954 | + } |
955 | #endif |
956 | - delem.nexttrans++; |
957 | - return true; |
958 | - } |
959 | + return res; |
960 | } |
961 | |
962 | + template |
963 | + class TarjanModelChecker<true>; |
964 | + |
965 | + template |
966 | + class TarjanModelChecker<false>; |
967 | } |
968 | \ No newline at end of file |
969 | |
970 | === modified file 'src/LTLMain.cpp' |
971 | --- src/LTLMain.cpp 2020-10-16 11:40:41 +0000 |
972 | +++ src/LTLMain.cpp 2020-11-09 13:59:57 +0000 |
973 | @@ -32,10 +32,8 @@ |
974 | |
975 | #include "CTL/CTLEngine.h" |
976 | #include "PetriEngine/PQL/Expressions.h" |
977 | -#include "LTL/LTLToBuchi.h" |
978 | #include "LTL/LTLValidator.h" |
979 | #include "LTL/LTL_algorithm/NestedDepthFirstSearch.h" |
980 | -#include "LTL/LTL_algorithm/ProductPrinter.h" |
981 | #include "LTL/LTL_algorithm/TarjanModelChecker.h" |
982 | #include "LTL/LTL.h" |
983 | |
984 | @@ -43,7 +41,6 @@ |
985 | using namespace PetriEngine::PQL; |
986 | using namespace PetriEngine::Reachability; |
987 | |
988 | - |
989 | std::vector<std::string> explode(std::string const & s) |
990 | { |
991 | std::vector<std::string> result; |
992 | @@ -502,7 +499,10 @@ |
993 | modelChecker = std::make_unique<LTL::NestedDepthFirstSearch>(*net, negated_formula); |
994 | break; |
995 | case LTL::Algorithm::Tarjan: |
996 | - modelChecker = std::make_unique<LTL::TarjanModelChecker>(*net, negated_formula); |
997 | + if (options.trace) |
998 | + modelChecker = std::make_unique<LTL::TarjanModelChecker<true>>(*net, negated_formula); |
999 | + else |
1000 | + modelChecker = std::make_unique<LTL::TarjanModelChecker<false>>(*net, negated_formula); |
1001 | break; |
1002 | } |
1003 | |
1004 | |
1005 | === modified file 'src/PetriEngine/SuccessorGenerator.cpp' |
1006 | --- src/PetriEngine/SuccessorGenerator.cpp 2020-10-16 13:38:03 +0000 |
1007 | +++ src/PetriEngine/SuccessorGenerator.cpp 2020-11-09 13:59:57 +0000 |
1008 | @@ -97,7 +97,7 @@ |
1009 | for (; _suc_tcounter != last; ++_suc_tcounter) { |
1010 | |
1011 | if (!checkPreset(_suc_tcounter)) continue; |
1012 | -#ifdef PRINTF_DEBUG |
1013 | +#ifdef _PRINTF_DEBUG |
1014 | std::cerr << "trace: " << _net.transitionNames()[_suc_tcounter] << std::endl; |
1015 | #endif |
1016 | memcpy(write.marking(), (*_parent).marking(), _net._nplaces * sizeof (MarkVal)); |