verifypn

Merge lp:~tapaal-ltl/verifypn/stubborn-set-refactor into lp:verifypn

  1. stubborn-set-refactor
  2. Merge into new-trunk
Proposed by Nikolaj Jensen Ulrik
Status: Merged
Merged at revision: 231
Proposed branch: lp:~tapaal-ltl/verifypn/stubborn-set-refactor
Merge into: lp:verifypn
Diff against target: 2482 lines (+1242/-747)
23 files modified
include/PetriEngine/PQL/Contexts.h (+6/-6)
include/PetriEngine/PQL/Expressions.h (+51/-36)
include/PetriEngine/PQL/PQL.h (+2/-7)
include/PetriEngine/PQL/Visitor.h (+87/-3)
include/PetriEngine/PetriNet.h (+1/-0)
include/PetriEngine/Reachability/ReachabilityResult.h (+2/-2)
include/PetriEngine/Reachability/ReachabilitySearch.h (+12/-2)
include/PetriEngine/ReducingSuccessorGenerator.h (+25/-54)
include/PetriEngine/Stubborn/InterestingTransitionVisitor.h (+163/-0)
include/PetriEngine/Stubborn/ReachabilityStubbornSet.h (+40/-0)
include/PetriEngine/Stubborn/StubbornSet.h (+146/-0)
include/PetriEngine/TAR/Solver.h (+1/-0)
include/PetriParse/QueryParser.h (+2/-3)
include/PetriParse/QueryXMLParser.h (+1/-1)
src/CTL/PetriNets/OnTheFlyDG.cpp (+2/-1)
src/PetriEngine/CMakeLists.txt (+2/-1)
src/PetriEngine/PQL/Expressions.cpp (+10/-328)
src/PetriEngine/ReducingSuccessorGenerator.cpp (+31/-302)
src/PetriEngine/Stubborn/CMakeLists.txt (+3/-0)
src/PetriEngine/Stubborn/InterestingTransitionVisitor.cpp (+311/-0)
src/PetriEngine/Stubborn/ReachabilityStubbornSet.cpp (+41/-0)
src/PetriEngine/Stubborn/StubbornSet.cpp (+302/-0)
src/PetriParse/QueryXMLParser.cpp (+1/-1)
To merge this branch: bzr merge lp:~tapaal-ltl/verifypn/stubborn-set-refactor
Reviewer Review Type Date Requested Status
VerifyPN Maintainers Pending
Review via email: mp+399092@code.launchpad.net

Description of the change

Refactor stubborn set generation out of ReducingSuccessorGenerator and into a separate type StubbornSet with pure virtual method `prepare(State)` to facilitate use of different stubborn set approaches. Additionally, interesting transition generation (the findInteresting, incr and decr methods on Condition/Expression types) is refactored into a Visitor. An experiment running each MCC'20 query for 5 minutes yields about 40 more answers (somehow) and no inconsistencies with verifypn@230.

This merge should be independent from the LTL engine merge proposal, although there may be conflicts wrt. PQL.h and Expressions.{cpp,h}.

To post a comment you must log in.
lp:~tapaal-ltl/verifypn/stubborn-set-refactor updated
232. By Nikolaj Jensen Ulrik

Remove commented code, fix one indent

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'include/PetriEngine/PQL/Contexts.h'
2--- include/PetriEngine/PQL/Contexts.h 2020-04-27 14:47:10 +0000
3+++ include/PetriEngine/PQL/Contexts.h 2021-03-04 07:47:28 +0000
4@@ -38,8 +38,8 @@
5 /** Context provided for context analysis */
6 class AnalysisContext {
7 protected:
8- const unordered_map<std::string, uint32_t>& _placeNames;
9- const unordered_map<std::string, uint32_t>& _transitionNames;
10+ const std::unordered_map<std::string, uint32_t>& _placeNames;
11+ const std::unordered_map<std::string, uint32_t>& _transitionNames;
12 const PetriNet* _net;
13 std::vector<ExprError> _errors;
14 public:
15@@ -176,7 +176,7 @@
16
17 SimplificationContext(const MarkVal* marking,
18 const PetriNet* net, uint32_t queryTimeout, uint32_t lpTimeout,
19- LPCache* cache)
20+ Simplification::LPCache* cache)
21 : _queryTimeout(queryTimeout), _lpTimeout(lpTimeout) {
22 _negated = false;
23 _marking = marking;
24@@ -222,8 +222,8 @@
25 }
26
27 uint32_t getLpTimeout() const;
28-
29- LPCache* cache() const
30+
31+ Simplification::LPCache* cache() const
32 {
33 return _cache;
34 }
35@@ -237,7 +237,7 @@
36 const PetriNet* _net;
37 uint32_t _queryTimeout, _lpTimeout;
38 std::chrono::high_resolution_clock::time_point _start;
39- LPCache* _cache;
40+ Simplification::LPCache* _cache;
41 mutable glp_prob* _base_lp = nullptr;
42
43 glp_prob* buildBase() const;
44
45=== modified file 'include/PetriEngine/PQL/Expressions.h'
46--- include/PetriEngine/PQL/Expressions.h 2020-06-02 16:20:24 +0000
47+++ include/PetriEngine/PQL/Expressions.h 2021-03-04 07:47:28 +0000
48@@ -103,8 +103,7 @@
49 Member constraint(SimplificationContext& context) const override;
50 void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
51 bool tk = false;
52- void incr(ReducingSuccessorGenerator& generator) const override;
53- void decr(ReducingSuccessorGenerator& generator) const override;
54+
55 void visit(Visitor& visitor) const override;
56 protected:
57 int apply(int v1, int v2) const override;
58@@ -122,8 +121,7 @@
59 Expr::Types type() const override;
60 Member constraint(SimplificationContext& context) const override;
61 void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
62- void incr(ReducingSuccessorGenerator& generator) const override;
63- void decr(ReducingSuccessorGenerator& generator) const override;
64+
65 void toBinary(std::ostream&) const override;
66 void visit(Visitor& visitor) const override;
67 protected:
68@@ -140,8 +138,7 @@
69 Expr::Types type() const override;
70 Member constraint(SimplificationContext& context) const override;
71 void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
72- void incr(ReducingSuccessorGenerator& generator) const override;
73- void decr(ReducingSuccessorGenerator& generator) const override;
74+
75 void visit(Visitor& visitor) const override;
76 protected:
77 int apply(int v1, int v2) const override;
78@@ -163,8 +160,7 @@
79 Member constraint(SimplificationContext& context) const override;
80 void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
81 void toBinary(std::ostream&) const override;
82- void incr(ReducingSuccessorGenerator& generator) const override;
83- void decr(ReducingSuccessorGenerator& generator) const override;
84+
85 void visit(Visitor& visitor) const override;
86 int formulaSize() const override{
87 return _expr->formulaSize() + 1;
88@@ -187,8 +183,7 @@
89 Expr::Types type() const override;
90 void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
91 void toBinary(std::ostream&) const override;
92- void incr(ReducingSuccessorGenerator& generator) const override;
93- void decr(ReducingSuccessorGenerator& generator) const override;
94+
95 void visit(Visitor& visitor) const override;
96 int formulaSize() const override{
97 return 1;
98@@ -223,12 +218,6 @@
99 void toXML(std::ostream& os, uint32_t tabs, bool tokencount = false) const override {
100 _compiled->toXML(os, tabs, tokencount);
101 }
102- void incr(ReducingSuccessorGenerator& generator) const override {
103- _compiled->incr(generator);
104- }
105- void decr(ReducingSuccessorGenerator& generator) const override {
106- _compiled->decr(generator);
107- }
108 int formulaSize() const override {
109 if(_compiled) return _compiled->formulaSize();
110 return 1;
111@@ -245,7 +234,13 @@
112 void toBinary(std::ostream& s) const override {
113 _compiled->toBinary(s);
114 }
115- void visit(Visitor& visitor) const override;
116+ void visit(Visitor& visitor) const override;
117+
118+ [[nodiscard]] const Expr_ptr &compiled() const
119+ {
120+ return _compiled;
121+ }
122+
123 private:
124 std::string _name;
125 Expr_ptr _compiled;
126@@ -267,8 +262,6 @@
127 Expr::Types type() const override;
128 void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const override;
129 void toBinary(std::ostream&) const override;
130- void incr(ReducingSuccessorGenerator& generator) const override;
131- void decr(ReducingSuccessorGenerator& generator) const override;
132 int formulaSize() const override{
133 return 1;
134 }
135@@ -311,8 +304,8 @@
136
137 void toXML(std::ostream& out, uint32_t tabs) const override
138 { _compiled->toXML(out, tabs); }
139- void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override
140- { _compiled->findInteresting(generator, negated);}
141+
142+
143 Quantifier getQuantifier() const override
144 { return _compiled->getQuantifier(); }
145 Path getPath() const override { return _compiled->getPath(); }
146@@ -381,7 +374,7 @@
147 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
148 void toXML(std::ostream&, uint32_t tabs) const override;
149 void toBinary(std::ostream&) const override;
150- void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
151+
152 Quantifier getQuantifier() const override { return Quantifier::NEG; }
153 Path getPath() const override { return Path::pError; }
154 CTLType getQueryType() const override { return CTLType::LOPERATOR; }
155@@ -421,7 +414,7 @@
156 void toString(std::ostream&) const override;
157 void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
158 void toBinary(std::ostream& out) const override;
159- void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
160+
161 virtual const Condition_ptr& operator[] (size_t i) const override { return _cond;}
162 virtual bool containsNext() const override { return _cond->containsNext(); }
163 bool nestedDeadlock() const override { return _cond->nestedDeadlock(); }
164@@ -562,7 +555,7 @@
165 void toBinary(std::ostream& out) const override;
166 bool isReachability(uint32_t depth) const override;
167 Condition_ptr prepareForReachability(bool negated) const override;
168- void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
169+
170 Result evalAndSet(const EvaluationContext& context) override;
171
172 virtual const Condition_ptr& operator[] (size_t i) const override
173@@ -571,6 +564,17 @@
174 { return Path::U; }
175 bool containsNext() const override { return _cond1->containsNext() || _cond2->containsNext(); }
176 bool nestedDeadlock() const override { return _cond1->nestedDeadlock() || _cond2->nestedDeadlock(); }
177+
178+ const Condition_ptr &getCond1() const
179+ {
180+ return _cond1;
181+ }
182+
183+ const Condition_ptr &getCond2() const
184+ {
185+ return _cond2;
186+ }
187+
188 private:
189 virtual std::string op() const = 0;
190
191@@ -702,7 +706,7 @@
192 Result evalAndSet(const EvaluationContext& context) override;
193 void visit(Visitor&) const override;
194 void toXML(std::ostream&, uint32_t tabs) const override;
195- void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
196+
197 Quantifier getQuantifier() const override { return Quantifier::AND; }
198 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
199 private:
200@@ -726,7 +730,7 @@
201 Result evalAndSet(const EvaluationContext& context) override;
202 void visit(Visitor&) const override;
203 void toXML(std::ostream&, uint32_t tabs) const override;
204- void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
205+
206 Quantifier getQuantifier() const override { return Quantifier::OR; }
207 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
208 private:
209@@ -818,7 +822,7 @@
210 Result evaluate(const EvaluationContext& context) override;
211 Result evalAndSet(const EvaluationContext& context) override;
212 void visit(Visitor&) const override;
213- void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
214+
215 Quantifier getQuantifier() const override { return _negated ? Quantifier::OR : Quantifier::AND; }
216 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
217 bool isNegated() const { return _negated; }
218@@ -868,6 +872,17 @@
219 bool containsNext() const override { return false; }
220 bool nestedDeadlock() const override { return false; }
221 bool isTrivial() const;
222+
223+ const Expr_ptr &getExpr1() const
224+ {
225+ return _expr1;
226+ }
227+
228+ const Expr_ptr &getExpr2() const
229+ {
230+ return _expr2;
231+ }
232+
233 protected:
234 uint32_t _distance(DistanceContext& c,
235 std::function<uint32_t(uint32_t, uint32_t, bool)> d) const
236@@ -898,7 +913,7 @@
237 using CompareCondition::CompareCondition;
238 Retval simplify(SimplificationContext& context) const override;
239 void toXML(std::ostream&, uint32_t tabs) const override;
240- void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
241+
242 uint32_t distance(DistanceContext& context) const override;
243 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
244 void visit(Visitor&) const override;
245@@ -917,7 +932,7 @@
246 void toTAPAALQuery(std::ostream&,TAPAALConditionExportContext& context) const override;
247 Retval simplify(SimplificationContext& context) const override;
248 void toXML(std::ostream&, uint32_t tabs) const override;
249- void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
250+
251 uint32_t distance(DistanceContext& context) const override;
252 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
253 void visit(Visitor&) const override;
254@@ -935,7 +950,7 @@
255 using CompareCondition::CompareCondition;
256 Retval simplify(SimplificationContext& context) const override;
257 void toXML(std::ostream&, uint32_t tabs) const override;
258- void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
259+
260 uint32_t distance(DistanceContext& context) const override;
261 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
262 void visit(Visitor&) const override;
263@@ -953,7 +968,7 @@
264 using CompareCondition::CompareCondition;
265 Retval simplify(SimplificationContext& context) const override;
266 void toXML(std::ostream&, uint32_t tabs) const override;
267- void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
268+
269 uint32_t distance(DistanceContext& context) const override;
270 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
271 void visit(Visitor&) const override;
272@@ -971,7 +986,7 @@
273 using CompareCondition::CompareCondition;
274 Retval simplify(SimplificationContext& context) const override;
275 void toXML(std::ostream&, uint32_t tabs) const override;
276- void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
277+
278 uint32_t distance(DistanceContext& context) const override;
279 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
280 void visit(Visitor&) const override;
281@@ -988,7 +1003,7 @@
282 using CompareCondition::CompareCondition;
283 Retval simplify(SimplificationContext& context) const override;
284 void toXML(std::ostream&, uint32_t tabs) const override;
285- void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
286+
287 uint32_t distance(DistanceContext& context) const override;
288 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
289 void visit(Visitor&) const override;
290@@ -1029,7 +1044,7 @@
291 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
292 void toXML(std::ostream&, uint32_t tabs) const override;
293 void toBinary(std::ostream&) const override;
294- void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
295+
296 Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
297 Path getPath() const override { return Path::pError; }
298 CTLType getQueryType() const override { return CTLType::EVAL; }
299@@ -1062,7 +1077,7 @@
300 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
301 void toXML(std::ostream&, uint32_t tabs) const override;
302 void toBinary(std::ostream&) const override;
303- void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
304+
305 static Condition_ptr DEADLOCK;
306 Quantifier getQuantifier() const override { return Quantifier::DEADLOCK; }
307 Path getPath() const override { return Path::pError; }
308@@ -1188,7 +1203,7 @@
309 Condition_ptr prepareForReachability(bool negated) const override;
310 Condition_ptr pushNegation(negstat_t&, const EvaluationContext& context, bool nested, bool negated, bool initrw) override;
311 void toXML(std::ostream&, uint32_t tabs) const override;
312- void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
313+
314 Quantifier getQuantifier() const override { return Quantifier::UPPERBOUNDS; }
315 Path getPath() const override { return Path::pError; }
316 CTLType getQueryType() const override { return CTLType::EVAL; }
317
318=== modified file 'include/PetriEngine/PQL/PQL.h'
319--- include/PetriEngine/PQL/PQL.h 2020-04-22 07:57:20 +0000
320+++ include/PetriEngine/PQL/PQL.h 2021-03-04 07:47:28 +0000
321@@ -26,8 +26,8 @@
322 #include <memory>
323
324 #include "../PetriNet.h"
325-#include "../Structures/State.h"
326-#include "../ReducingSuccessorGenerator.h"
327+//#include "../Structures/State.h"
328+//#include "../ReducingSuccessorGenerator.h"
329 #include "../Simplification/LPCache.h"
330
331 namespace PetriEngine {
332@@ -120,9 +120,6 @@
333 /** Output the expression as it currently is to a file in XML */
334 virtual void toXML(std::ostream&, uint32_t tabs, bool tokencount = false) const = 0;
335 virtual void toBinary(std::ostream&) const = 0;
336- /** Stubborn reduction: increasing and decreasing sets */
337- virtual void incr(ReducingSuccessorGenerator& generator) const = 0;
338- virtual void decr(ReducingSuccessorGenerator& generator) const = 0;
339 /** Count size of the entire formula in number of nodes */
340 virtual int formulaSize() const = 0;
341
342@@ -230,8 +227,6 @@
343 virtual void toXML(std::ostream&, uint32_t tabs) const = 0;
344 virtual void toBinary(std::ostream& out) const = 0;
345
346- /** Find interesting transitions in stubborn reduction*/
347- virtual void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const = 0;
348 /** Checks if the condition is trivially true */
349 bool isTriviallyTrue();
350 /*** Checks if the condition is trivially false */
351
352=== modified file 'include/PetriEngine/PQL/Visitor.h'
353--- include/PetriEngine/PQL/Visitor.h 2020-06-02 16:20:24 +0000
354+++ include/PetriEngine/PQL/Visitor.h 2021-03-04 07:47:28 +0000
355@@ -62,8 +62,14 @@
356 virtual void _accept(const EUCondition*)
357 { assert(false); std::cerr << "No accept for EUCondition" << std::endl; exit(0);};
358 virtual void _accept(const AUCondition*)
359- { assert(false); std::cerr << "No accept for AUCondition" << std::endl; exit(0);};
360-
361+ { assert(false); std::cerr << "No accept for AUCondition" << std::endl; exit(0);};
362+
363+ virtual void _accept(const UntilCondition *) {
364+ assert(false);
365+ std::cerr << "No accept for UntilCondition" << std::endl;
366+ exit(0);
367+ };
368+
369 // shallow elements, neither of these should exist in a compiled expression
370 virtual void _accept(const UnfoldedFireableCondition* element)
371 { assert(false); std::cerr << "No accept for UnfoldedFireableCondition" << std::endl; exit(0);};
372@@ -93,7 +99,85 @@
373 // shallow expression, default to error
374 virtual void _accept(const IdentifierExpr* element)
375 { assert(false); std::cerr << "No accept for IdentifierExpr" << std::endl; exit(0);};
376- };
377+ };
378+
379+ class ExpressionVisitor : public Visitor {
380+ public:
381+
382+ private:
383+ void _accept(const NotCondition *element) override {
384+ assert(false);
385+ std::cerr << "No accept for NotCondition" << std::endl;
386+ exit(0);
387+ };
388+
389+ void _accept(const AndCondition *element) override {
390+ assert(false);
391+ std::cerr << "No accept for AndCondition" << std::endl;
392+ exit(0);
393+ };
394+
395+ void _accept(const OrCondition *element) override {
396+ assert(false);
397+ std::cerr << "No accept for OrCondition" << std::endl;
398+ exit(0);
399+ };
400+
401+ void _accept(const LessThanCondition *element) override {
402+ assert(false);
403+ std::cerr << "No accept for LessThanCondition" << std::endl;
404+ exit(0);
405+ };
406+
407+ void _accept(const LessThanOrEqualCondition *element) override {
408+ assert(false);
409+ std::cerr << "No accept for LessThanOrEqualCondition" << std::endl;
410+ exit(0);
411+ };
412+
413+ void _accept(const GreaterThanCondition *element) override {
414+ assert(false);
415+ std::cerr << "No accept for GreaterThanCondition" << std::endl;
416+ exit(0);
417+ };
418+
419+ void _accept(const GreaterThanOrEqualCondition *element) override {
420+ assert(false);
421+ std::cerr << "No accept for GreaterThanOrEqualCondition" << std::endl;
422+ exit(0);
423+ };
424+
425+ void _accept(const EqualCondition *element) override {
426+ assert(false);
427+ std::cerr << "No accept for EqualCondition" << std::endl;
428+ exit(0);
429+ };
430+
431+ void _accept(const NotEqualCondition *element) override {
432+ assert(false);
433+ std::cerr << "No accept for NotEqualCondition" << std::endl;
434+ exit(0);
435+ };
436+
437+ void _accept(const DeadlockCondition *element) override {
438+ assert(false);
439+ std::cerr << "No accept for DeadlockCondition" << std::endl;
440+ exit(0);
441+ };
442+
443+ void _accept(const CompareConjunction *element) override {
444+ assert(false);
445+ std::cerr << "No accept for CompareConjunction" << std::endl;
446+ exit(0);
447+ };
448+
449+ void _accept(const UnfoldedUpperBoundsCondition *element) override {
450+ assert(false);
451+ std::cerr << "No accept for UnfoldedUpperBoundsCondition" << std::endl;
452+ exit(0);
453+ };
454+ };
455+
456 }
457 }
458
459
460=== modified file 'include/PetriEngine/PetriNet.h'
461--- include/PetriEngine/PetriNet.h 2020-09-18 07:35:03 +0000
462+++ include/PetriEngine/PetriNet.h 2021-03-04 07:47:28 +0000
463@@ -132,6 +132,7 @@
464 friend class SuccessorGenerator;
465 friend class ReducingSuccessorGenerator;
466 friend class STSolver;
467+ friend class StubbornSet;
468 };
469
470 } // PetriEngine
471
472=== modified file 'include/PetriEngine/Reachability/ReachabilityResult.h'
473--- include/PetriEngine/Reachability/ReachabilityResult.h 2020-04-23 15:26:52 +0000
474+++ include/PetriEngine/Reachability/ReachabilityResult.h 2021-03-04 07:47:28 +0000
475@@ -66,8 +66,8 @@
476 std::vector<std::string>& querynames;
477 Reducer* reducer;
478 public:
479- const string techniques = "TECHNIQUES COLLATERAL_PROCESSING STRUCTURAL_REDUCTION QUERY_REDUCTION SAT_SMT ";
480- const string techniquesStateSpace = "TECHNIQUES EXPLICIT STATE_COMPRESSION";
481+ const std::string techniques = "TECHNIQUES COLLATERAL_PROCESSING STRUCTURAL_REDUCTION QUERY_REDUCTION SAT_SMT ";
482+ const std::string techniquesStateSpace = "TECHNIQUES EXPLICIT STATE_COMPRESSION";
483
484 ResultPrinter(PetriNetBuilder* b, options_t* o, std::vector<std::string>& querynames)
485 : builder(b), options(o), querynames(querynames), reducer(NULL)
486
487=== modified file 'include/PetriEngine/Reachability/ReachabilitySearch.h'
488--- include/PetriEngine/Reachability/ReachabilitySearch.h 2020-04-23 15:26:52 +0000
489+++ include/PetriEngine/Reachability/ReachabilitySearch.h 2021-03-04 07:47:28 +0000
490@@ -28,6 +28,7 @@
491 #include "../Structures/Queue.h"
492 #include "../SuccessorGenerator.h"
493 #include "../ReducingSuccessorGenerator.h"
494+#include "PetriEngine/Stubborn/ReachabilityStubbornSet.h"
495
496 #include <memory>
497 #include <vector>
498@@ -93,7 +94,16 @@
499 Structures::State _initial;
500 AbstractHandler& _callback;
501 };
502-
503+
504+ template <typename G>
505+ inline G _makeSucGen(PetriNet &net, std::vector<PQL::Condition_ptr> &queries) {
506+ return G{net, queries};
507+ }
508+ template <>
509+ inline ReducingSuccessorGenerator _makeSucGen(PetriNet &net, std::vector<PQL::Condition_ptr> &queries) {
510+ return ReducingSuccessorGenerator{net, queries, std::make_shared<ReachabilityStubbornSet>(net, queries)};
511+ }
512+
513 template<typename Q, typename W, typename G>
514 bool ReachabilitySearch::tryReach( std::vector<std::shared_ptr<PQL::Condition> >& queries,
515 std::vector<ResultPrinter::Result>& results, bool usequeries,
516@@ -117,7 +127,7 @@
517
518 W states(_net, _kbound); // stateset
519 Q queue(&states); // working queue
520- G generator(_net, queries); // successor generator
521+ G generator = _makeSucGen<G>(_net, queries); // successor generator
522 auto r = states.add(state);
523 // this can fail due to reductions; we push tokens around and violate K
524 if(r.first){
525
526=== modified file 'include/PetriEngine/ReducingSuccessorGenerator.h'
527--- include/PetriEngine/ReducingSuccessorGenerator.h 2020-03-02 21:03:24 +0000
528+++ include/PetriEngine/ReducingSuccessorGenerator.h 2021-03-04 07:47:28 +0000
529@@ -6,63 +6,34 @@
530 #include "Structures/light_deque.h"
531 #include "PQL/PQL.h"
532 #include <memory>
533+#include "PetriEngine/Stubborn/StubbornSet.h"
534
535 namespace PetriEngine {
536
537-class ReducingSuccessorGenerator : public SuccessorGenerator {
538-
539-public:
540- struct place_t {
541- uint32_t pre, post;
542- };
543- struct trans_t {
544- uint32_t index;
545- int8_t direction;
546- trans_t() = default;
547- trans_t(uint32_t id, int8_t dir) : index(id), direction(dir) {};
548- bool operator<(const trans_t& t) const
549- {
550- return index < t.index;
551- }
552- };
553- ReducingSuccessorGenerator(const PetriNet& net);
554- ReducingSuccessorGenerator(const PetriNet& net, std::vector<std::shared_ptr<PQL::Condition> >& queries);
555- virtual ~ReducingSuccessorGenerator();
556- void prepare(const Structures::State* state);
557- bool next(Structures::State& write);
558- void presetOf(uint32_t place, bool make_closure = false);
559- void postsetOf(uint32_t place, bool make_closure = false);
560- void postPresetOf(uint32_t t, bool make_closure = false);
561- void inhibitorPostsetOf(uint32_t place);
562- bool seenPre(uint32_t place) const;
563- bool seenPost(uint32_t place) const;
564- uint32_t leastDependentEnabled();
565- uint32_t fired()
566- {
567- return _current;
568- }
569- void setQuery(PQL::Condition* ptr) { _queries.clear(); _queries = {ptr};}
570- void reset();
571-
572-private:
573- inline void addToStub(uint32_t t);
574- void closure();
575- std::unique_ptr<bool[]> _enabled, _stubborn;
576- std::unique_ptr<uint8_t[]> _places_seen;
577- std::unique_ptr<place_t[]> _places;
578- std::unique_ptr<trans_t[]> _transitions;
579- light_deque<uint32_t> _unprocessed, _ordering;
580- std::unique_ptr<uint32_t[]> _dependency;
581- uint32_t _current;
582- bool _netContainsInhibitorArcs;
583- std::vector<std::vector<uint32_t>> _inhibpost;
584-
585- std::vector<PQL::Condition* > _queries;
586- void constructEnabled();
587- void constructPrePost();
588- void constructDependency();
589- void checkForInhibitor();
590-};
591+ class ReducingSuccessorGenerator : public SuccessorGenerator {
592+
593+ public:
594+ ReducingSuccessorGenerator(const PetriNet &net, std::shared_ptr<StubbornSet> stubbornSet);
595+
596+ ReducingSuccessorGenerator(const PetriNet &net, std::vector<std::shared_ptr<PQL::Condition> > &queries,
597+ std::shared_ptr<StubbornSet> stubbornSet);
598+
599+ void reset();
600+
601+ void setQuery(PQL::Condition *ptr) { _stubSet->setQuery(ptr); }
602+
603+ void prepare(const Structures::State *state);
604+
605+ bool next(Structures::State &write);
606+
607+ auto fired() const { return _current; }
608+ private:
609+ std::shared_ptr<StubbornSet> _stubSet;
610+ uint32_t _current;
611+
612+ std::vector<PQL::Condition *> _queries;
613+
614+ };
615 }
616
617 #endif /* PETRIENGINE_REDUCINGSUCCESSORGENERATOR_H_ */
618
619=== added directory 'include/PetriEngine/Stubborn'
620=== added file 'include/PetriEngine/Stubborn/InterestingTransitionVisitor.h'
621--- include/PetriEngine/Stubborn/InterestingTransitionVisitor.h 1970-01-01 00:00:00 +0000
622+++ include/PetriEngine/Stubborn/InterestingTransitionVisitor.h 2021-03-04 07:47:28 +0000
623@@ -0,0 +1,163 @@
624+/*
625+ * File: InterestingTransitionVisitor.h
626+ * Author: Nikolaj J. Ulrik <nikolaj@njulrik.dk>
627+ *
628+ * Created on 03/02/2021
629+ */
630+
631+#ifndef VERIFYPN_INTERESTINGTRANSITIONVISITOR_H
632+#define VERIFYPN_INTERESTINGTRANSITIONVISITOR_H
633+
634+#include "PetriEngine/PQL/Visitor.h"
635+#include "PetriEngine/Stubborn/StubbornSet.h"
636+
637+namespace PetriEngine {
638+ class InterestingTransitionVisitor : public PQL::Visitor {
639+ public:
640+ InterestingTransitionVisitor(PetriEngine::StubbornSet &stubbornSet)
641+ : _stubborn(stubbornSet), incr(stubbornSet), decr(stubbornSet) {
642+ incr.decr = &decr;
643+ decr.incr = &incr;
644+ }
645+
646+ private:
647+ PetriEngine::StubbornSet &_stubborn;
648+ bool negated = false;
649+
650+ void negate() { negated = !negated; }
651+
652+ protected:
653+ void _accept(const PQL::NotCondition *element) override;
654+
655+ void _accept(const PQL::AndCondition *element) override;
656+
657+ void _accept(const PQL::OrCondition *element) override;
658+
659+ void _accept(const PQL::LessThanCondition *element) override;
660+
661+ void _accept(const PQL::LessThanOrEqualCondition *element) override;
662+
663+ void _accept(const PQL::GreaterThanCondition *element) override;
664+
665+ void _accept(const PQL::GreaterThanOrEqualCondition *element) override;
666+
667+ void _accept(const PQL::EqualCondition *element) override;
668+
669+ void _accept(const PQL::NotEqualCondition *element) override;
670+
671+ void _accept(const PQL::DeadlockCondition *element) override;
672+
673+ void _accept(const PQL::CompareConjunction *element) override;
674+
675+ void _accept(const PQL::UnfoldedUpperBoundsCondition *element) override;
676+
677+ void _accept(const PQL::UnfoldedIdentifierExpr *element) override {
678+ assert(false);
679+ std::cerr << "No accept for UnfoldedIdentifierExpr" << std::endl;
680+ exit(0);
681+ };
682+
683+ void _accept(const PQL::LiteralExpr *element) override {
684+ assert(false);
685+ std::cerr << "No accept for LiteralExpr" << std::endl;
686+ exit(0);
687+ };
688+
689+ void _accept(const PQL::PlusExpr *element) override {
690+ assert(false);
691+ std::cerr << "No accept for PlusExpr" << std::endl;
692+ exit(0);
693+ };
694+
695+ void _accept(const PQL::MultiplyExpr *element) override {
696+ assert(false);
697+ std::cerr << "No accept for MultiplyExpr" << std::endl;
698+ exit(0);
699+ };
700+
701+ void _accept(const PQL::MinusExpr *element) override {
702+ assert(false);
703+ std::cerr << "No accept for MinusExpr" << std::endl;
704+ exit(0);
705+ };
706+
707+ void _accept(const PQL::SubtractExpr *element) override {
708+ assert(false);
709+ std::cerr << "No accept for SubtractExpr" << std::endl;
710+ exit(0);
711+ };
712+
713+ void _accept(const PQL::SimpleQuantifierCondition *element);
714+
715+ void _accept(const PQL::UntilCondition *element) override;
716+
717+ void _accept(const PQL::BooleanCondition *element) override;
718+
719+ private:
720+
721+ /*
722+ * Mutually recursive visitors for incrementing/decrementing of places.
723+ */
724+
725+ class DecrVisitor;
726+ class IncrVisitor : public PQL::ExpressionVisitor {
727+ public:
728+ IncrVisitor(StubbornSet &stubbornSet)
729+ : _stubborn(stubbornSet) {}
730+
731+ DecrVisitor *decr;
732+ private:
733+ StubbornSet &_stubborn;
734+
735+ void _accept(const PQL::IdentifierExpr *element) override {
736+ element->compiled()->visit(*this);
737+ }
738+
739+ void _accept(const PQL::UnfoldedIdentifierExpr *element) override;
740+
741+ void _accept(const PQL::LiteralExpr *element) override;
742+
743+ void _accept(const PQL::PlusExpr *element) override;
744+
745+ void _accept(const PQL::MultiplyExpr *element) override;
746+
747+ void _accept(const PQL::MinusExpr *element) override;
748+
749+ void _accept(const PQL::SubtractExpr *element) override;
750+ };
751+
752+ class DecrVisitor : public PQL::ExpressionVisitor {
753+ public:
754+ DecrVisitor(StubbornSet &stubbornSet)
755+ : _stubborn(stubbornSet) {}
756+
757+ IncrVisitor *incr;
758+
759+ private:
760+ StubbornSet &_stubborn;
761+
762+ void _accept(const PQL::IdentifierExpr *element) override {
763+ element->compiled()->visit(*this);
764+ }
765+
766+ void _accept(const PQL::UnfoldedIdentifierExpr *element) override;
767+
768+ void _accept(const PQL::LiteralExpr *element) override;
769+
770+ void _accept(const PQL::PlusExpr *element) override;
771+
772+ void _accept(const PQL::MultiplyExpr *element) override;
773+
774+ void _accept(const PQL::MinusExpr *element) override;
775+
776+ void _accept(const PQL::SubtractExpr *element) override;
777+ };
778+
779+ IncrVisitor incr;
780+ DecrVisitor decr;
781+ };
782+
783+}
784+
785+
786+#endif //VERIFYPN_INTERESTINGTRANSITIONVISITOR_H
787
788=== added file 'include/PetriEngine/Stubborn/ReachabilityStubbornSet.h'
789--- include/PetriEngine/Stubborn/ReachabilityStubbornSet.h 1970-01-01 00:00:00 +0000
790+++ include/PetriEngine/Stubborn/ReachabilityStubbornSet.h 2021-03-04 07:47:28 +0000
791@@ -0,0 +1,40 @@
792+/* Copyright (C) 2021 Nikolaj J. Ulrik <nikolaj@njulrik.dk>,
793+ * Simon M. Virenfeldt <simon@simwir.dk>
794+ *
795+ * This program is free software: you can redistribute it and/or modify
796+ * it under the terms of the GNU General Public License as published by
797+ * the Free Software Foundation, either version 3 of the License, or
798+ * (at your option) any later version.
799+ *
800+ * This program is distributed in the hope that it will be useful,
801+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
802+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
803+ * GNU General Public License for more details.
804+ *
805+ * You should have received a copy of the GNU General Public License
806+ * along with this program. If not, see <http://www.gnu.org/licenses/>.
807+ */
808+
809+#ifndef VERIFYPN_REACHABILITYSTUBBORNSET_H
810+#define VERIFYPN_REACHABILITYSTUBBORNSET_H
811+
812+
813+#include "PetriEngine/Stubborn/StubbornSet.h"
814+
815+namespace PetriEngine {
816+ class ReachabilityStubbornSet : public StubbornSet {
817+ public:
818+ ReachabilityStubbornSet(const PetriNet &net, const vector<PQL::Condition_ptr> &queries)
819+ : StubbornSet(net, queries) {}
820+
821+ ReachabilityStubbornSet(const PetriNet &net)
822+ : StubbornSet(net) {}
823+
824+ void prepare(const Structures::State *state) override;
825+
826+
827+ private:
828+ };
829+}
830+
831+#endif //VERIFYPN_REACHABILITYSTUBBORNSET_H
832
833=== added file 'include/PetriEngine/Stubborn/StubbornSet.h'
834--- include/PetriEngine/Stubborn/StubbornSet.h 1970-01-01 00:00:00 +0000
835+++ include/PetriEngine/Stubborn/StubbornSet.h 2021-03-04 07:47:28 +0000
836@@ -0,0 +1,146 @@
837+/* Copyright (C) 2021 Nikolaj J. Ulrik <nikolaj@njulrik.dk>,
838+ * Simon M. Virenfeldt <simon@simwir.dk>
839+ *
840+ * This program is free software: you can redistribute it and/or modify
841+ * it under the terms of the GNU General Public License as published by
842+ * the Free Software Foundation, either version 3 of the License, or
843+ * (at your option) any later version.
844+ *
845+ * This program is distributed in the hope that it will be useful,
846+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
847+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
848+ * GNU General Public License for more details.
849+ *
850+ * You should have received a copy of the GNU General Public License
851+ * along with this program. If not, see <http://www.gnu.org/licenses/>.
852+ */
853+
854+#ifndef VERIFYPN_STUBBORNSET_H
855+#define VERIFYPN_STUBBORNSET_H
856+
857+#include "PetriEngine/PetriNet.h"
858+#include "PetriEngine/Structures/State.h"
859+#include "PetriEngine/Structures/light_deque.h"
860+#include "PetriEngine/PQL/PQL.h"
861+
862+#include <memory>
863+#include <vector>
864+
865+namespace PetriEngine {
866+ class StubbornSet {
867+ public:
868+ StubbornSet(const PetriEngine::PetriNet &net)
869+ : _net(net), _inhibpost(net._nplaces) {
870+ _current = 0;
871+ _enabled = std::make_unique<bool[]>(net._ntransitions);
872+ _stubborn = std::make_unique<bool[]>(net._ntransitions);
873+ _dependency = std::make_unique<uint32_t[]>(net._ntransitions);
874+ _places_seen = std::make_unique<uint8_t[]>(_net.numberOfPlaces());
875+ StubbornSet::reset();
876+ constructPrePost();
877+ constructDependency();
878+ checkForInhibitor();
879+
880+ }
881+
882+ StubbornSet(const PetriEngine::PetriNet &net, const std::vector<PQL::Condition_ptr> &queries)
883+ : StubbornSet(net) {
884+ for (auto &q: queries) {
885+ _queries.push_back(q.get());
886+ }
887+ }
888+
889+ virtual void prepare(const Structures::State *marking) = 0;
890+
891+ uint32_t next();
892+
893+ virtual ~StubbornSet() = default;
894+
895+ virtual void reset();
896+
897+ [[nodiscard]] const MarkVal *getParent() const {
898+ return _parent->marking();
899+ }
900+
901+ uint32_t _current;
902+
903+ void presetOf(uint32_t place, bool make_closure = false);
904+
905+ void postsetOf(uint32_t place, bool make_closure = false);
906+
907+ void postPresetOf(uint32_t t, bool make_closure = false);
908+
909+ void inhibitorPostsetOf(uint32_t place);
910+
911+ bool seenPre(uint32_t place) const;
912+
913+ bool seenPost(uint32_t place) const;
914+
915+ uint32_t leastDependentEnabled();
916+
917+ uint32_t fired() {
918+ return _current;
919+ }
920+
921+ void setQuery(PQL::Condition *ptr) {
922+ _queries.clear();
923+ _queries = {ptr};
924+ }
925+
926+ protected:
927+ const PetriEngine::PetriNet &_net;
928+ const Structures::State *_parent;
929+
930+ struct place_t {
931+ uint32_t pre, post;
932+ };
933+
934+ struct trans_t {
935+ uint32_t index;
936+ int8_t direction;
937+
938+ trans_t() = default;
939+
940+ trans_t(uint32_t id, int8_t dir) : index(id), direction(dir) {};
941+
942+ bool operator<(const trans_t &t) const {
943+ return index < t.index;
944+ }
945+ };
946+
947+ size_t _tid = 0;
948+
949+ const std::vector<TransPtr> &transitions() { return _net._transitions; }
950+
951+ const std::vector<Invariant> &invariants() { return _net._invariants; }
952+
953+ const std::vector<uint32_t> &placeToPtrs() { return _net._placeToPtrs; }
954+
955+ bool checkPreset(uint32_t t);
956+
957+ inline void addToStub(uint32_t t);
958+
959+ void closure();
960+
961+ std::unique_ptr<bool[]> _enabled, _stubborn;
962+ std::unique_ptr<uint8_t[]> _places_seen;
963+ std::unique_ptr<place_t[]> _places;
964+ std::unique_ptr<trans_t[]> _transitions;
965+ light_deque<uint32_t> _unprocessed, _ordering;
966+ std::unique_ptr<uint32_t[]> _dependency;
967+ bool _netContainsInhibitorArcs;
968+ std::vector<std::vector<uint32_t>> _inhibpost;
969+
970+ std::vector<PQL::Condition *> _queries;
971+
972+ void constructEnabled();
973+
974+ void constructPrePost();
975+
976+ void constructDependency();
977+
978+ void checkForInhibitor();
979+ };
980+}
981+
982+#endif //VERIFYPN_STUBBORNSET_H
983
984=== modified file 'include/PetriEngine/TAR/Solver.h'
985--- include/PetriEngine/TAR/Solver.h 2020-04-21 21:01:42 +0000
986+++ include/PetriEngine/TAR/Solver.h 2021-03-04 07:47:28 +0000
987@@ -16,6 +16,7 @@
988 #include "range.h"
989 #include "PetriEngine/PQL/PQL.h"
990 #include "TraceSet.h"
991+#include "PetriEngine/SuccessorGenerator.h"
992
993 #include <utility>
994 #include <cinttypes>
995
996=== modified file 'include/PetriParse/QueryParser.h'
997--- include/PetriParse/QueryParser.h 2020-03-02 21:03:24 +0000
998+++ include/PetriParse/QueryParser.h 2021-03-04 07:47:28 +0000
999@@ -4,11 +4,10 @@
1000
1001
1002 #include "PetriEngine/PQL/PQL.h"
1003-using namespace PetriEngine::PQL;
1004
1005 struct QueryItem {
1006- string id; // query name
1007- Condition_ptr query;
1008+ std::string id; // query name
1009+ PetriEngine::PQL::Condition_ptr query;
1010
1011 enum {
1012 PARSING_OK,
1013
1014=== modified file 'include/PetriParse/QueryXMLParser.h'
1015--- include/PetriParse/QueryXMLParser.h 2020-03-13 13:35:25 +0000
1016+++ include/PetriParse/QueryXMLParser.h 2021-03-04 07:47:28 +0000
1017@@ -50,7 +50,7 @@
1018 Condition_ptr parseFormula(rapidxml::xml_node<>* element);
1019 Condition_ptr parseBooleanFormula(rapidxml::xml_node<>* element);
1020 Expr_ptr parseIntegerExpression(rapidxml::xml_node<>* element);
1021- string parsePlace(rapidxml::xml_node<>* element);
1022+ std::string parsePlace(rapidxml::xml_node<>* element);
1023 void fatal_error(const std::string& token);
1024 };
1025
1026
1027=== modified file 'src/CTL/PetriNets/OnTheFlyDG.cpp'
1028--- src/CTL/PetriNets/OnTheFlyDG.cpp 2020-03-02 22:05:53 +0000
1029+++ src/CTL/PetriNets/OnTheFlyDG.cpp 2021-03-04 07:47:28 +0000
1030@@ -7,6 +7,7 @@
1031 #include <limits>
1032
1033 #include "PetriEngine/SuccessorGenerator.h"
1034+#include "PetriEngine/Stubborn/ReachabilityStubbornSet.h"
1035 #include "PetriEngine/PQL/Expressions.h"
1036 #include "CTL/SearchStrategy/SearchStrategy.h"
1037
1038@@ -19,7 +20,7 @@
1039 OnTheFlyDG::OnTheFlyDG(PetriEngine::PetriNet *t_net, bool partial_order) : encoder(t_net->numberOfPlaces(), 0),
1040 edge_alloc(new linked_bucket_t<DependencyGraph::Edge,1024*10>(1)),
1041 conf_alloc(new linked_bucket_t<char[sizeof(PetriConfig)], 1024*1024>(1)),
1042- _redgen(*t_net), _partial_order(partial_order) {
1043+ _redgen(*t_net, std::make_shared<PetriEngine::ReachabilityStubbornSet>(*t_net)), _partial_order(partial_order) {
1044 net = t_net;
1045 n_places = t_net->numberOfPlaces();
1046 n_transitions = t_net->numberOfTransitions();
1047
1048=== modified file 'src/PetriEngine/CMakeLists.txt'
1049--- src/PetriEngine/CMakeLists.txt 2020-04-04 14:48:55 +0000
1050+++ src/PetriEngine/CMakeLists.txt 2021-03-04 07:47:28 +0000
1051@@ -3,6 +3,7 @@
1052 add_subdirectory(Colored)
1053 add_subdirectory(Structures)
1054 add_subdirectory(Simplification)
1055+add_subdirectory(Stubborn)
1056 add_subdirectory(Reachability)
1057 add_subdirectory(PQL)
1058 add_subdirectory(TAR)
1059@@ -16,4 +17,4 @@
1060 SuccessorGenerator.cpp
1061 )
1062
1063-target_link_libraries(PetriEngine PRIVATE Colored Structures Simplification Reachability PQL TAR)
1064+target_link_libraries(PetriEngine PRIVATE Colored Structures Simplification Stubborn Reachability PQL TAR)
1065
1066=== modified file 'src/PetriEngine/PQL/Expressions.cpp'
1067--- src/PetriEngine/PQL/Expressions.cpp 2020-07-02 13:57:17 +0000
1068+++ src/PetriEngine/PQL/Expressions.cpp 2021-03-04 07:47:28 +0000
1069@@ -500,8 +500,8 @@
1070 std::sort(_ids.begin(), _ids.end(), [](auto& a, auto& b){ return a.first < b.first; });
1071 std::sort(_exprs.begin(), _exprs.end(), [](auto& a, auto& b)
1072 {
1073- auto ida = dynamic_pointer_cast<PQL::UnfoldedIdentifierExpr>(a);
1074- auto idb = dynamic_pointer_cast<PQL::UnfoldedIdentifierExpr>(b);
1075+ auto ida = std::dynamic_pointer_cast<PQL::UnfoldedIdentifierExpr>(a);
1076+ auto idb = std::dynamic_pointer_cast<PQL::UnfoldedIdentifierExpr>(b);
1077 if(ida == NULL) return false;
1078 if(ida && !idb) return true;
1079 return ida->offset() < idb->offset();
1080@@ -3557,16 +3557,16 @@
1081 if(bi == b->_ids.end() || ai == a->_ids.end()) break;
1082 }
1083 };
1084- if(auto p1 = dynamic_pointer_cast<PlusExpr>(_expr1))
1085- if(auto p2 = dynamic_pointer_cast<PlusExpr>(_expr2))
1086+ if(auto p1 = std::dynamic_pointer_cast<PlusExpr>(_expr1))
1087+ if(auto p2 = std::dynamic_pointer_cast<PlusExpr>(_expr2))
1088 remdup(p1, p2);
1089
1090- if(auto m1 = dynamic_pointer_cast<MultiplyExpr>(_expr1))
1091- if(auto m2 = dynamic_pointer_cast<MultiplyExpr>(_expr2))
1092+ if(auto m1 = std::dynamic_pointer_cast<MultiplyExpr>(_expr1))
1093+ if(auto m2 = std::dynamic_pointer_cast<MultiplyExpr>(_expr2))
1094 remdup(m1, m2);
1095
1096- if(auto p1 = dynamic_pointer_cast<CommutativeExpr>(_expr1))
1097- if(auto p2 = dynamic_pointer_cast<CommutativeExpr>(_expr2))
1098+ if(auto p1 = std::dynamic_pointer_cast<CommutativeExpr>(_expr1))
1099+ if(auto p2 = std::dynamic_pointer_cast<CommutativeExpr>(_expr2))
1100 return p1->_exprs.size() + p1->_ids.size() + p2->_exprs.size() + p2->_ids.size() == 0;
1101 return _expr1->placeFree() && _expr2->placeFree();
1102 }
1103@@ -3658,324 +3658,6 @@
1104 }
1105
1106
1107- /******************** Stubborn reduction interesting transitions ********************/
1108-
1109- void PlusExpr::incr(ReducingSuccessorGenerator& generator) const {
1110- for(auto& i : _ids) generator.presetOf(i.first, true);
1111- for(auto& e : _exprs) e->incr(generator);
1112- }
1113-
1114- void PlusExpr::decr(ReducingSuccessorGenerator& generator) const {
1115- for(auto& i : _ids) generator.postsetOf(i.first, true);
1116- for(auto& e : _exprs) e->decr(generator);
1117- }
1118-
1119- void SubtractExpr::incr(ReducingSuccessorGenerator& generator) const {
1120- bool first = true;
1121- for(auto& e : _exprs)
1122- {
1123- if(first)
1124- e->incr(generator);
1125- else
1126- e->decr(generator);
1127- first = false;
1128- }
1129- }
1130-
1131- void SubtractExpr::decr(ReducingSuccessorGenerator& generator) const {
1132- bool first = true;
1133- for(auto& e : _exprs)
1134- {
1135- if(first)
1136- e->decr(generator);
1137- else
1138- e->incr(generator);
1139- first = false;
1140- }
1141- }
1142-
1143- void MultiplyExpr::incr(ReducingSuccessorGenerator& generator) const {
1144- if((_ids.size() + _exprs.size()) == 1)
1145- {
1146- for(auto& i : _ids) generator.presetOf(i.first, true);
1147- for(auto& e : _exprs) e->incr(generator);
1148- }
1149- else
1150- {
1151- for(auto& i : _ids)
1152- {
1153- generator.presetOf(i.first, true);
1154- generator.postsetOf(i.first, true);
1155- }
1156- for(auto& e : _exprs)
1157- {
1158- e->incr(generator);
1159- e->decr(generator);
1160- }
1161- }
1162- }
1163-
1164- void MultiplyExpr::decr(ReducingSuccessorGenerator& generator) const {
1165- if((_ids.size() + _exprs.size()) == 1)
1166- {
1167- for(auto& i : _ids) generator.postsetOf(i.first, true);
1168- for(auto& e : _exprs) e->decr(generator);
1169- }
1170- else
1171- incr(generator);
1172- }
1173-
1174- void MinusExpr::incr(ReducingSuccessorGenerator& generator) const {
1175- // TODO not implemented
1176- }
1177-
1178- void MinusExpr::decr(ReducingSuccessorGenerator& generator) const {
1179- // TODO not implemented
1180- }
1181-
1182- void LiteralExpr::incr(ReducingSuccessorGenerator& generator) const {
1183- // Add nothing
1184- }
1185-
1186- void LiteralExpr::decr(ReducingSuccessorGenerator& generator) const {
1187- // Add nothing
1188- }
1189-
1190- void UnfoldedIdentifierExpr::incr(ReducingSuccessorGenerator& generator) const {
1191- generator.presetOf(_offsetInMarking, true);
1192- }
1193-
1194- void UnfoldedIdentifierExpr::decr(ReducingSuccessorGenerator& generator) const {
1195- generator.postsetOf(_offsetInMarking, true);
1196- }
1197-
1198- void SimpleQuantifierCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const{
1199- _cond->findInteresting(generator, negated);
1200- }
1201-
1202- void UntilCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const{
1203- _cond1->findInteresting(generator, negated);
1204- _cond1->findInteresting(generator, !negated);
1205- _cond2->findInteresting(generator, negated);
1206- }
1207-
1208- void AndCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
1209- if(!negated){ // and
1210- for(auto& c : _conds)
1211- {
1212- if(!c->isSatisfied())
1213- {
1214- c->findInteresting(generator, negated);
1215- break;
1216- }
1217- }
1218- } else { // or
1219- for(auto& c : _conds) c->findInteresting(generator, negated);
1220- }
1221- }
1222-
1223- void OrCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
1224- if(!negated){ // or
1225- for(auto& c : _conds) c->findInteresting(generator, negated);
1226- } else { // and
1227- for(auto& c : _conds)
1228- {
1229- if(c->isSatisfied())
1230- {
1231- c->findInteresting(generator, negated);
1232- break;
1233- }
1234- }
1235- }
1236- }
1237-
1238- void CompareConjunction::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const{
1239-
1240- auto neg = negated != _negated;
1241- int32_t cand = std::numeric_limits<int32_t>::max();
1242- bool pre = false;
1243- for(auto& c : _constraints)
1244- {
1245- auto val = generator.parent()[c._place];
1246- if(c._lower == c._upper)
1247- {
1248- if(neg)
1249- {
1250- if(val != c._lower) continue;
1251- generator.postsetOf(c._place, true);
1252- generator.presetOf(c._place, true);
1253- }
1254- else
1255- {
1256- if(val == c._lower) continue;
1257- if(val > c._lower) {
1258- cand = c._place;
1259- pre = false;
1260- } else {
1261- cand = c._place;
1262- pre = true;
1263- }
1264- }
1265- }
1266- else
1267- {
1268- if(!neg)
1269- {
1270- if(val < c._lower && c._lower != 0)
1271- {
1272- assert(!neg);
1273- cand = c._place;
1274- pre = true;
1275- }
1276-
1277- if(val > c._upper && c._upper != std::numeric_limits<uint32_t>::max())
1278- {
1279- assert(!neg);
1280- cand = c._place;
1281- pre = false;
1282- }
1283- }
1284- else
1285- {
1286- if(val >= c._lower && c._lower != 0)
1287- {
1288- generator.postsetOf(c._place, true);
1289- }
1290-
1291- if(val <= c._upper && c._upper != std::numeric_limits<uint32_t>::max())
1292- {
1293- generator.presetOf(c._place, true);
1294- }
1295- }
1296- }
1297- if(cand != std::numeric_limits<int32_t>::max())
1298- {
1299- if(pre && generator.seenPre(cand))
1300- return;
1301- else if(!pre && generator.seenPost(cand))
1302- return;
1303- }
1304- }
1305- if(cand != std::numeric_limits<int32_t>::max())
1306- {
1307- if(pre)
1308- {
1309- generator.presetOf(cand, true);
1310- }
1311- else if(!pre)
1312- {
1313- generator.postsetOf(cand, true);
1314- }
1315- }
1316- }
1317-
1318- void EqualCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
1319- if(!negated){ // equal
1320- if(_expr1->getEval() == _expr2->getEval()) { return; }
1321- if(_expr1->getEval() > _expr2->getEval()){
1322- _expr1->decr(generator);
1323- _expr2->incr(generator);
1324- } else {
1325- _expr1->incr(generator);
1326- _expr2->decr(generator);
1327- }
1328- } else { // not equal
1329- if(_expr1->getEval() != _expr2->getEval()) { return; }
1330- _expr1->incr(generator);
1331- _expr1->decr(generator);
1332- _expr2->incr(generator);
1333- _expr2->decr(generator);
1334- }
1335- }
1336-
1337- void NotEqualCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
1338- if(!negated){ // not equal
1339- if(_expr1->getEval() != _expr2->getEval()) { return; }
1340- _expr1->incr(generator);
1341- _expr1->decr(generator);
1342- _expr2->incr(generator);
1343- _expr2->decr(generator);
1344- } else { // equal
1345- if(_expr1->getEval() == _expr2->getEval()) { return; }
1346- if(_expr1->getEval() > _expr2->getEval()){
1347- _expr1->decr(generator);
1348- _expr2->incr(generator);
1349- } else {
1350- _expr1->incr(generator);
1351- _expr2->decr(generator);
1352- }
1353- }
1354- }
1355-
1356- void LessThanCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
1357- if(!negated){ // less than
1358- if(_expr1->getEval() < _expr2->getEval()) { return; }
1359- _expr1->decr(generator);
1360- _expr2->incr(generator);
1361- } else { // greater than or equal
1362- if(_expr1->getEval() >= _expr2->getEval()) { return; }
1363- _expr1->incr(generator);
1364- _expr2->decr(generator);
1365- }
1366- }
1367-
1368- void LessThanOrEqualCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
1369- if(!negated){ // less than or equal
1370- if(_expr1->getEval() <= _expr2->getEval()) { return; }
1371- _expr1->decr(generator);
1372- _expr2->incr(generator);
1373- } else { // greater than
1374- if(_expr1->getEval() > _expr2->getEval()) { return; }
1375- _expr1->incr(generator);
1376- _expr2->decr(generator);
1377- }
1378- }
1379-
1380- void GreaterThanCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
1381- if(!negated){ // greater than
1382- if(_expr1->getEval() > _expr2->getEval()) { return; }
1383- _expr1->incr(generator);
1384- _expr2->decr(generator);
1385- } else { // less than or equal
1386- if(_expr1->getEval() <= _expr2->getEval()) { return; }
1387- _expr1->decr(generator);
1388- _expr2->incr(generator);
1389- }
1390- }
1391-
1392- void GreaterThanOrEqualCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
1393- if(!negated){ // greater than or equal
1394- if(_expr1->getEval() >= _expr2->getEval()) { return; }
1395- _expr1->incr(generator);
1396- _expr2->decr(generator);
1397- } else { // less than
1398- if(_expr1->getEval() < _expr2->getEval()) { return; }
1399- _expr1->decr(generator);
1400- _expr2->incr(generator);
1401- }
1402- }
1403-
1404- void NotCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
1405- _cond->findInteresting(generator, !negated);
1406- }
1407-
1408- void BooleanCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
1409- // Add nothing
1410- }
1411-
1412- void DeadlockCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
1413- if(!isSatisfied()){
1414- generator.postPresetOf(generator.leastDependentEnabled(), true);
1415- } // else add nothing
1416- }
1417-
1418- void UnfoldedUpperBoundsCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
1419- for(auto& p : _places)
1420- if(!p._maxed_out)
1421- generator.presetOf(p._place);
1422- }
1423-
1424-
1425 /********************** CONSTRUCTORS *********************************/
1426
1427 template<typename T>
1428@@ -4156,10 +3838,10 @@
1429 EvaluationContext c;
1430 _constant = apply(_constant, e->evaluate(c));
1431 }
1432- else if (auto id = dynamic_pointer_cast<PQL::UnfoldedIdentifierExpr>(e)) {
1433+ else if (auto id = std::dynamic_pointer_cast<PQL::UnfoldedIdentifierExpr>(e)) {
1434 _ids.emplace_back(id->offset(), id->name());
1435 }
1436- else if(auto c = dynamic_pointer_cast<CommutativeExpr>(e))
1437+ else if(auto c = std::dynamic_pointer_cast<CommutativeExpr>(e))
1438 {
1439 // we should move up plus/multiply here when possible;
1440 if(c->_ids.size() == 0 && c->_exprs.size() == 0)
1441
1442=== modified file 'src/PetriEngine/ReducingSuccessorGenerator.cpp'
1443--- src/PetriEngine/ReducingSuccessorGenerator.cpp 2020-03-02 21:03:24 +0000
1444+++ src/PetriEngine/ReducingSuccessorGenerator.cpp 2021-03-04 07:47:28 +0000
1445@@ -5,314 +5,43 @@
1446
1447 namespace PetriEngine {
1448
1449- ReducingSuccessorGenerator::ReducingSuccessorGenerator(const PetriNet& net) : SuccessorGenerator(net), _inhibpost(net._nplaces){
1450- _current = 0;
1451- _enabled = std::make_unique<bool[]>(net._ntransitions);
1452- _stubborn = std::make_unique<bool[]>(net._ntransitions);
1453- _dependency = std::make_unique<uint32_t[]>(net._ntransitions);
1454- _places_seen = std::make_unique<uint8_t[]>(_net.numberOfPlaces());
1455- reset();
1456- constructPrePost();
1457- constructDependency();
1458- checkForInhibitor();
1459+ ReducingSuccessorGenerator::ReducingSuccessorGenerator(const PetriNet &net,
1460+ std::shared_ptr<StubbornSet> stubbornSet)
1461+ : SuccessorGenerator(net), _stubSet(stubbornSet) {
1462+
1463 }
1464
1465- ReducingSuccessorGenerator::ReducingSuccessorGenerator(const PetriNet& net, std::vector<std::shared_ptr<PQL::Condition> >& queries) : ReducingSuccessorGenerator(net) {
1466+ ReducingSuccessorGenerator::ReducingSuccessorGenerator(const PetriNet &net,
1467+ std::vector<std::shared_ptr<PQL::Condition> > &queries,
1468+ std::shared_ptr<StubbornSet> stubbornSet)
1469+ : ReducingSuccessorGenerator(net, stubbornSet) {
1470 _queries.reserve(queries.size());
1471- for(auto& q : queries)
1472+ for (auto &q : queries)
1473 _queries.push_back(q.get());
1474 }
1475
1476- ReducingSuccessorGenerator::~ReducingSuccessorGenerator() {
1477- }
1478-
1479- void ReducingSuccessorGenerator::checkForInhibitor(){
1480- _netContainsInhibitorArcs=false;
1481- for (uint32_t t = 0; t < _net._ntransitions; t++) {
1482- const TransPtr& ptr = _net._transitions[t];
1483- uint32_t finv = ptr.inputs;
1484- uint32_t linv = ptr.outputs;
1485- for (; finv < linv; finv++) { // Post set of places
1486- if (_net._invariants[finv].inhibitor) {
1487- _netContainsInhibitorArcs=true;
1488- return;
1489- }
1490- }
1491- }
1492- }
1493-
1494- void ReducingSuccessorGenerator::constructPrePost() {
1495- std::vector<std::pair<std::vector<trans_t>, std::vector < trans_t>>> tmp_places(_net._nplaces);
1496-
1497- for (uint32_t t = 0; t < _net._ntransitions; t++) {
1498- const TransPtr& ptr = _net._transitions[t];
1499- uint32_t finv = ptr.inputs;
1500- uint32_t linv = ptr.outputs;
1501- for (; finv < linv; finv++) { // Post set of places
1502- if (_net._invariants[finv].inhibitor) {
1503- _inhibpost[_net._invariants[finv].place].push_back(t);
1504- _netContainsInhibitorArcs=true;
1505- } else {
1506- tmp_places[_net._invariants[finv].place].second.emplace_back(t, _net._invariants[finv].direction);
1507- }
1508- }
1509-
1510- finv = linv;
1511- linv = _net._transitions[t + 1].inputs;
1512- for (; finv < linv; finv++) { // Pre set of places
1513- if(_net._invariants[finv].direction > 0)
1514- tmp_places[_net._invariants[finv].place].first.emplace_back(t, _net._invariants[finv].direction);
1515- }
1516- }
1517-
1518- // flatten
1519- size_t ntrans = 0;
1520- for (auto p : tmp_places) {
1521- ntrans += p.first.size() + p.second.size();
1522- }
1523- _transitions.reset(new trans_t[ntrans]);
1524-
1525- _places.reset(new place_t[_net._nplaces + 1]);
1526- uint32_t offset = 0;
1527- uint32_t p = 0;
1528- for (; p < _net._nplaces; ++p) {
1529- auto& pre = tmp_places[p].first;
1530- auto& post = tmp_places[p].second;
1531-
1532- // keep things nice for caches
1533- std::sort(pre.begin(), pre.end());
1534- std::sort(post.begin(), post.end());
1535-
1536- _places.get()[p].pre = offset;
1537- offset += pre.size();
1538- _places.get()[p].post = offset;
1539- offset += post.size();
1540- for (size_t tn = 0; tn < pre.size(); ++tn) {
1541- _transitions.get()[tn + _places.get()[p].pre] = pre[tn];
1542- }
1543-
1544- for (size_t tn = 0; tn < post.size(); ++tn) {
1545- _transitions.get()[tn + _places.get()[p].post] = post[tn];
1546- }
1547-
1548- }
1549- assert(offset == ntrans);
1550- _places.get()[p].pre = offset;
1551- _places.get()[p].post = offset;
1552- }
1553-
1554- void ReducingSuccessorGenerator::constructDependency() {
1555- memset(_dependency.get(), 0, sizeof(uint32_t) * _net._ntransitions);
1556-
1557- for (uint32_t t = 0; t < _net._ntransitions; t++) {
1558- uint32_t finv = _net._transitions[t].inputs;
1559- uint32_t linv = _net._transitions[t].outputs;
1560-
1561- for (; finv < linv; finv++) {
1562- const Invariant& inv = _net._invariants[finv];
1563- uint32_t p = inv.place;
1564- uint32_t ntrans = (_places.get()[p + 1].pre - _places.get()[p].post);
1565-
1566- for (uint32_t tIndex = 0; tIndex < ntrans; tIndex++) {
1567- ++_dependency[t];
1568- }
1569- }
1570- }
1571- }
1572-
1573- void ReducingSuccessorGenerator::constructEnabled() {
1574- _ordering.clear();
1575- for (uint32_t p = 0; p < _net._nplaces; ++p) {
1576- // orphans are currently under "place 0" as a special case
1577- if (p == 0 || (*_parent).marking()[p] > 0) {
1578- uint32_t t = _net._placeToPtrs[p];
1579- uint32_t last = _net._placeToPtrs[p + 1];
1580-
1581- for (; t != last; ++t) {
1582- if (!checkPreset(t)) continue;
1583- _enabled[t] = true;
1584- _ordering.push_back(t);
1585- }
1586- }
1587- }
1588- }
1589-
1590- bool ReducingSuccessorGenerator::seenPre(uint32_t place) const
1591- {
1592- return (_places_seen.get()[place] & 1) != 0;
1593- }
1594-
1595- bool ReducingSuccessorGenerator::seenPost(uint32_t place) const
1596- {
1597- return (_places_seen.get()[place] & 2) != 0;
1598- }
1599-
1600- void ReducingSuccessorGenerator::presetOf(uint32_t place, bool make_closure) {
1601- if((_places_seen.get()[place] & 1) != 0) return;
1602- _places_seen.get()[place] = _places_seen.get()[place] | 1;
1603- for (uint32_t t = _places.get()[place].pre; t < _places.get()[place].post; t++)
1604- {
1605- auto& tr = _transitions.get()[t];
1606- addToStub(tr.index);
1607- }
1608- if(make_closure) closure();
1609- }
1610-
1611- void ReducingSuccessorGenerator::postsetOf(uint32_t place, bool make_closure) {
1612- if((_places_seen.get()[place] & 2) != 0) return;
1613- _places_seen.get()[place] = _places_seen.get()[place] | 2;
1614- for (uint32_t t = _places.get()[place].post; t < _places.get()[place + 1].pre; t++) {
1615- auto tr = _transitions.get()[t];
1616- if(tr.direction < 0)
1617- addToStub(tr.index);
1618- }
1619- if(make_closure) closure();
1620- }
1621-
1622- void ReducingSuccessorGenerator::addToStub(uint32_t t)
1623- {
1624- if(!_stubborn[t])
1625- {
1626- _stubborn[t] = true;
1627- _unprocessed.push_back(t);
1628- }
1629- }
1630-
1631- void ReducingSuccessorGenerator::inhibitorPostsetOf(uint32_t place){
1632- if((_places_seen.get()[place] & 4) != 0) return;
1633- _places_seen.get()[place] = _places_seen.get()[place] | 4;
1634- for(uint32_t& newstub : _inhibpost[place])
1635- addToStub(newstub);
1636- }
1637-
1638- void ReducingSuccessorGenerator::postPresetOf(uint32_t t, bool make_closure) {
1639- const TransPtr& ptr = _net._transitions[t];
1640- uint32_t finv = ptr.inputs;
1641- uint32_t linv = ptr.outputs;
1642- for (; finv < linv; finv++) { // pre-set of t
1643- if(_net._invariants[finv].inhibitor){
1644- presetOf(_net._invariants[finv].place, make_closure);
1645- } else {
1646- postsetOf(_net._invariants[finv].place, make_closure);
1647- }
1648- }
1649- }
1650-
1651-
1652- void ReducingSuccessorGenerator::prepare(const Structures::State* state) {
1653- _parent = state;
1654- memset(_places_seen.get(), 0, _net.numberOfPlaces());
1655- constructEnabled();
1656- if(_ordering.size() == 0) return;
1657- if(_ordering.size() == 1)
1658- {
1659- _stubborn[_ordering.front()] = true;
1660- return;
1661- }
1662- for (auto &q : _queries) {
1663- q->evalAndSet(PQL::EvaluationContext((*_parent).marking(), &_net));
1664- q->findInteresting(*this, false);
1665- }
1666-
1667- closure();
1668- }
1669-
1670- void ReducingSuccessorGenerator::closure()
1671- {
1672- while (!_unprocessed.empty()) {
1673- uint32_t tr = _unprocessed.front();
1674- _unprocessed.pop_front();
1675- const TransPtr& ptr = _net._transitions[tr];
1676- uint32_t finv = ptr.inputs;
1677- uint32_t linv = ptr.outputs;
1678- if(_enabled[tr]){
1679- for (; finv < linv; finv++) {
1680- if(_net._invariants[finv].direction < 0)
1681- {
1682- auto place = _net._invariants[finv].place;
1683- for (uint32_t t = _places.get()[place].post; t < _places.get()[place + 1].pre; t++)
1684- addToStub(_transitions.get()[t].index);
1685- }
1686- }
1687- if(_netContainsInhibitorArcs){
1688- uint32_t next_finv = _net._transitions[tr+1].inputs;
1689- for (; linv < next_finv; linv++)
1690- {
1691- if(_net._invariants[linv].direction > 0)
1692- inhibitorPostsetOf(_net._invariants[linv].place);
1693- }
1694- }
1695- } else {
1696- bool ok = false;
1697- bool inhib = false;
1698- uint32_t cand = std::numeric_limits<uint32_t>::max();
1699-
1700- // Lets try to see if we havent already added sufficient pre/post
1701- // for this transition.
1702- for (; finv < linv; ++finv) {
1703- const Invariant& inv = _net._invariants[finv];
1704- if ((*_parent).marking()[inv.place] < inv.tokens && !inv.inhibitor) {
1705- inhib = false;
1706- ok = (_places_seen.get()[inv.place] & 1) != 0;
1707- cand = inv.place;
1708- } else if ((*_parent).marking()[inv.place] >= inv.tokens && inv.inhibitor) {
1709- inhib = true;
1710- ok = (_places_seen.get()[inv.place] & 2) != 0;
1711- cand = inv.place;
1712- }
1713- if(ok) break;
1714-
1715- }
1716-
1717- // OK, we didnt have sufficient, we just pick whatever is left
1718- // in cand.
1719- assert(cand != std::numeric_limits<uint32_t>::max());
1720- if(!ok && cand != std::numeric_limits<uint32_t>::max())
1721- {
1722- if(!inhib) presetOf(cand);
1723- else postsetOf(cand);
1724- }
1725- }
1726- }
1727- }
1728-
1729- bool ReducingSuccessorGenerator::next(Structures::State& write) {
1730- while (!_ordering.empty()) {
1731- _current = _ordering.front();
1732- _ordering.pop_front();
1733- if (_stubborn[_current]) {
1734- assert(_enabled[_current]);
1735- memcpy(write.marking(), (*_parent).marking(), _net._nplaces*sizeof(MarkVal));
1736- consumePreset(write, _current);
1737- producePostset(write, _current);
1738- return true;
1739- }
1740- }
1741- reset();
1742- return false;
1743- }
1744-
1745- uint32_t ReducingSuccessorGenerator::leastDependentEnabled() {
1746- uint32_t tLeast = -1;
1747- bool foundLeast = false;
1748- for (uint32_t t = 0; t < _net._ntransitions; t++) {
1749- if (_enabled[t]) {
1750- if (!foundLeast) {
1751- tLeast = t;
1752- foundLeast = true;
1753- } else {
1754- if (_dependency[t] < _dependency[tLeast]) {
1755- tLeast = t;
1756- }
1757- }
1758- }
1759- }
1760- return tLeast;
1761- }
1762-
1763 void ReducingSuccessorGenerator::reset() {
1764 SuccessorGenerator::reset();
1765- memset(_enabled.get(), false, sizeof(bool) * _net._ntransitions);
1766- memset(_stubborn.get(), false, sizeof(bool) * _net._ntransitions);
1767- }
1768+ _stubSet->reset();
1769+ }
1770+
1771+
1772+ bool ReducingSuccessorGenerator::next(Structures::State &write) {
1773+ _current = _stubSet->next();
1774+ if (_current == std::numeric_limits<uint32_t>::max()) {
1775+ reset();
1776+ return false;
1777+ }
1778+ memcpy(write.marking(), (*_parent).marking(), _net._nplaces * sizeof(MarkVal));
1779+ consumePreset(write, _current);
1780+ producePostset(write, _current);
1781+ return true;
1782+ }
1783+
1784+ void ReducingSuccessorGenerator::prepare(const Structures::State *state) {
1785+ _parent = state;
1786+ _stubSet->prepare(state);
1787+ }
1788+
1789+
1790 }
1791
1792=== added directory 'src/PetriEngine/Stubborn'
1793=== added file 'src/PetriEngine/Stubborn/CMakeLists.txt'
1794--- src/PetriEngine/Stubborn/CMakeLists.txt 1970-01-01 00:00:00 +0000
1795+++ src/PetriEngine/Stubborn/CMakeLists.txt 2021-03-04 07:47:28 +0000
1796@@ -0,0 +1,3 @@
1797+set(CMAKE_INCLUDE_CURRENT_DIR ON)
1798+
1799+add_library(Stubborn ReachabilityStubbornSet.cpp InterestingTransitionVisitor.cpp StubbornSet.cpp)
1800
1801=== added file 'src/PetriEngine/Stubborn/InterestingTransitionVisitor.cpp'
1802--- src/PetriEngine/Stubborn/InterestingTransitionVisitor.cpp 1970-01-01 00:00:00 +0000
1803+++ src/PetriEngine/Stubborn/InterestingTransitionVisitor.cpp 2021-03-04 07:47:28 +0000
1804@@ -0,0 +1,311 @@
1805+/*
1806+ * File: InterestingTransitionVisitor.cpp.cc
1807+ * Author: Nikolaj J. Ulrik <nikolaj@njulrik.dk>
1808+ *
1809+ * Created on 03/02/2021
1810+ */
1811+
1812+#include "PetriEngine/Stubborn/InterestingTransitionVisitor.h"
1813+
1814+namespace PetriEngine {
1815+
1816+ void InterestingTransitionVisitor::_accept(const PQL::SimpleQuantifierCondition *element) {
1817+ (*element)[0]->visit(*this);
1818+ }
1819+
1820+ void InterestingTransitionVisitor::_accept(const PQL::UntilCondition *element) {
1821+ element->getCond1()->visit(*this);
1822+ negate();
1823+ element->getCond1()->visit(*this);
1824+ negate();
1825+ element->getCond2()->visit(*this);
1826+ }
1827+
1828+
1829+ void InterestingTransitionVisitor::_accept(const PQL::AndCondition *element) {
1830+ if (!negated) { // and
1831+ for (auto &c : *element) {
1832+ if (!c->isSatisfied()) {
1833+ c->visit(*this);
1834+ break;
1835+ }
1836+ }
1837+ } else { // or
1838+ for (auto &c : *element) c->visit(*this);
1839+ }
1840+ }
1841+
1842+ void InterestingTransitionVisitor::_accept(const PQL::OrCondition *element) {
1843+ if (!negated) { // or
1844+ for (auto &c : *element) c->visit(*this);
1845+ } else { // and
1846+ for (auto &c : *element) {
1847+ if (c->isSatisfied()) {
1848+ c->visit(*this);
1849+ break;
1850+ }
1851+ }
1852+ }
1853+ }
1854+
1855+ void InterestingTransitionVisitor::_accept(const PQL::CompareConjunction *element) {
1856+
1857+ auto neg = negated != element->isNegated();
1858+ int32_t cand = std::numeric_limits<int32_t>::max();
1859+ bool pre = false;
1860+ for (auto &c : *element) {
1861+ auto val = _stubborn.getParent()[c._place];
1862+ if (c._lower == c._upper) {
1863+ if (neg) {
1864+ if (val != c._lower) continue;
1865+ _stubborn.postsetOf(c._place, true);
1866+ _stubborn.presetOf(c._place, true);
1867+ } else {
1868+ if (val == c._lower) continue;
1869+ if (val > c._lower) {
1870+ cand = c._place;
1871+ pre = false;
1872+ } else {
1873+ cand = c._place;
1874+ pre = true;
1875+ }
1876+ }
1877+ } else {
1878+ if (!neg) {
1879+ if (val < c._lower && c._lower != 0) {
1880+ assert(!neg);
1881+ cand = c._place;
1882+ pre = true;
1883+ }
1884+
1885+ if (val > c._upper && c._upper != std::numeric_limits<uint32_t>::max()) {
1886+ assert(!neg);
1887+ cand = c._place;
1888+ pre = false;
1889+ }
1890+ } else {
1891+ if (val >= c._lower && c._lower != 0) {
1892+ _stubborn.postsetOf(c._place, true);
1893+ }
1894+
1895+ if (val <= c._upper && c._upper != std::numeric_limits<uint32_t>::max()) {
1896+ _stubborn.presetOf(c._place, true);
1897+ }
1898+ }
1899+ }
1900+ if (cand != std::numeric_limits<int32_t>::max()) {
1901+ if (pre && _stubborn.seenPre(cand))
1902+ return;
1903+ else if (!pre && _stubborn.seenPost(cand))
1904+ return;
1905+ }
1906+ }
1907+ if (cand != std::numeric_limits<int32_t>::max()) {
1908+ if (pre) {
1909+ _stubborn.presetOf(cand, true);
1910+ } else if (!pre) {
1911+ _stubborn.postsetOf(cand, true);
1912+ }
1913+ }
1914+ }
1915+
1916+ void InterestingTransitionVisitor::_accept(const PQL::EqualCondition *element) {
1917+ if (!negated) { // equal
1918+ if (element->getExpr1()->getEval() == element->getExpr2()->getEval()) { return; }
1919+ if (element->getExpr1()->getEval() > element->getExpr2()->getEval()) {
1920+ element->getExpr1()->visit(decr);
1921+ element->getExpr2()->visit(incr);
1922+ } else {
1923+ element->getExpr1()->visit(incr);
1924+ element->getExpr2()->visit(decr);
1925+ }
1926+ } else { // not equal
1927+ if (element->getExpr1()->getEval() != element->getExpr2()->getEval()) { return; }
1928+ element->getExpr1()->visit(incr);
1929+ element->getExpr1()->visit(decr);
1930+ element->getExpr2()->visit(incr);
1931+ element->getExpr2()->visit(decr);
1932+ }
1933+ }
1934+
1935+ void InterestingTransitionVisitor::_accept(const PQL::NotEqualCondition *element) {
1936+ if (!negated) { // not equal
1937+ if (element->getExpr1()->getEval() != element->getExpr2()->getEval()) { return; }
1938+ element->getExpr1()->visit(incr);
1939+ element->getExpr1()->visit(decr);
1940+ element->getExpr2()->visit(incr);
1941+ element->getExpr2()->visit(decr);
1942+ } else { // equal
1943+ if (element->getExpr1()->getEval() == element->getExpr2()->getEval()) { return; }
1944+ if (element->getExpr1()->getEval() > element->getExpr2()->getEval()) {
1945+ element->getExpr1()->visit(decr);
1946+ element->getExpr2()->visit(incr);
1947+ } else {
1948+ element->getExpr1()->visit(incr);
1949+ element->getExpr2()->visit(decr);
1950+ }
1951+ }
1952+ }
1953+
1954+ void InterestingTransitionVisitor::_accept(const PQL::LessThanCondition *element) {
1955+ if (!negated) { // less than
1956+ if (element->getExpr1()->getEval() < element->getExpr2()->getEval()) { return; }
1957+ element->getExpr1()->visit(decr);
1958+ element->getExpr2()->visit(incr);
1959+ } else { // greater than or equal
1960+ if (element->getExpr1()->getEval() >= element->getExpr2()->getEval()) { return; }
1961+ element->getExpr1()->visit(incr);
1962+ element->getExpr2()->visit(decr);
1963+ }
1964+ }
1965+
1966+ void InterestingTransitionVisitor::_accept(const PQL::LessThanOrEqualCondition *element) {
1967+ if (!negated) { // less than or equal
1968+ if (element->getExpr1()->getEval() <= element->getExpr2()->getEval()) { return; }
1969+ element->getExpr1()->visit(decr);
1970+ element->getExpr2()->visit(incr);
1971+ } else { // greater than
1972+ if (element->getExpr1()->getEval() > element->getExpr2()->getEval()) { return; }
1973+ element->getExpr1()->visit(incr);
1974+ element->getExpr2()->visit(decr);
1975+ }
1976+ }
1977+
1978+ void InterestingTransitionVisitor::_accept(const PQL::GreaterThanCondition *element) {
1979+ if (!negated) { // greater than
1980+ if (element->getExpr1()->getEval() > element->getExpr2()->getEval()) { return; }
1981+ element->getExpr1()->visit(incr);
1982+ element->getExpr2()->visit(decr);
1983+ } else { // less than or equal
1984+ if (element->getExpr1()->getEval() <= element->getExpr2()->getEval()) { return; }
1985+ element->getExpr1()->visit(decr);
1986+ element->getExpr2()->visit(incr);
1987+ }
1988+ }
1989+
1990+ void
1991+ InterestingTransitionVisitor::_accept(const PQL::GreaterThanOrEqualCondition *element) {
1992+ if (!negated) { // greater than or equal
1993+ if (element->getExpr1()->getEval() >= element->getExpr2()->getEval()) { return; }
1994+ element->getExpr1()->visit(incr);
1995+ element->getExpr2()->visit(decr);
1996+ } else { // less than
1997+ if (element->getExpr1()->getEval() < element->getExpr2()->getEval()) { return; }
1998+ element->getExpr1()->visit(decr);
1999+ element->getExpr2()->visit(incr);
2000+ }
2001+ }
2002+
2003+ void InterestingTransitionVisitor::_accept(const PQL::NotCondition *element) {
2004+ negate();
2005+ element->visit(*this);
2006+ negate();
2007+ }
2008+
2009+ void InterestingTransitionVisitor::_accept(const PQL::BooleanCondition *element) {
2010+ // Add nothing
2011+ }
2012+
2013+ void InterestingTransitionVisitor::_accept(const PQL::DeadlockCondition *element) {
2014+ if (!element->isSatisfied()) {
2015+ _stubborn.postPresetOf(_stubborn.leastDependentEnabled(), true);
2016+ } // else add nothing
2017+ }
2018+
2019+ void
2020+ InterestingTransitionVisitor::_accept(const PQL::UnfoldedUpperBoundsCondition *element) {
2021+ for (auto &p : element->places())
2022+ if (!p._maxed_out)
2023+ _stubborn.presetOf(p._place);
2024+ }
2025+
2026+ void InterestingTransitionVisitor::IncrVisitor::_accept(const PQL::PlusExpr *element) {
2027+ for(auto& i : element->places()) _stubborn.presetOf(i.first, true);
2028+ for(auto& e : element->expressions()) e->visit(*this);
2029+ }
2030+
2031+ void InterestingTransitionVisitor::DecrVisitor::_accept(const PQL::PlusExpr *element) {
2032+ for(auto& i : element->places()) _stubborn.postsetOf(i.first, true);
2033+ for(auto& e : element->expressions()) e->visit(*this);
2034+ }
2035+
2036+ void InterestingTransitionVisitor::IncrVisitor::_accept(const PQL::SubtractExpr *element) {
2037+ bool first = true;
2038+ for(auto& e : element->expressions())
2039+ {
2040+ if(first)
2041+ e->visit(*this);
2042+ else
2043+ e->visit(*decr);
2044+ first = false;
2045+ }
2046+ }
2047+
2048+ void InterestingTransitionVisitor::DecrVisitor::_accept(const PQL::SubtractExpr *element) {
2049+ bool first = true;
2050+ for(auto& e : element->expressions())
2051+ {
2052+ if(first)
2053+ e->visit(*this);
2054+ else
2055+ e->visit(*incr);
2056+ first = false;
2057+ }
2058+ }
2059+
2060+ void InterestingTransitionVisitor::IncrVisitor::_accept(const PQL::MultiplyExpr *element) {
2061+ if((element->places().size() + element->expressions().size()) == 1)
2062+ {
2063+ for(auto& i : element->places()) _stubborn.presetOf(i.first, true);
2064+ for(auto& e : element->expressions()) e->visit(*this);
2065+ }
2066+ else
2067+ {
2068+ for(auto& i : element->places())
2069+ {
2070+ _stubborn.presetOf(i.first, true);
2071+ _stubborn.postsetOf(i.first, true);
2072+ }
2073+ for(auto& e : element->expressions())
2074+ {
2075+ e->visit(*this);
2076+ e->visit(*decr);
2077+ }
2078+ }
2079+ }
2080+
2081+ void InterestingTransitionVisitor::DecrVisitor::_accept(const PQL::MultiplyExpr *element) {
2082+ if((element->places().size() + element->expressions().size()) == 1)
2083+ {
2084+ for(auto& i : element->places()) _stubborn.postsetOf(i.first, true);
2085+ for(auto& e : element->expressions()) e->visit(*this);
2086+ }
2087+ else
2088+ element->visit(*incr);
2089+ }
2090+
2091+ void InterestingTransitionVisitor::IncrVisitor::_accept(const PQL::MinusExpr *element) {
2092+ // TODO not implemented
2093+ }
2094+
2095+ void InterestingTransitionVisitor::DecrVisitor::_accept(const PQL::MinusExpr *element) {
2096+ // TODO not implemented
2097+ }
2098+
2099+ void InterestingTransitionVisitor::IncrVisitor::_accept(const PQL::LiteralExpr *element) {
2100+ // Add nothing
2101+ }
2102+
2103+ void InterestingTransitionVisitor::DecrVisitor::_accept(const PQL::LiteralExpr *element) {
2104+ // Add nothing
2105+ }
2106+
2107+ void InterestingTransitionVisitor::IncrVisitor::_accept(const PQL::UnfoldedIdentifierExpr *element) {
2108+ _stubborn.presetOf(element->offset(), true);
2109+ }
2110+
2111+ void InterestingTransitionVisitor::DecrVisitor::_accept(const PQL::UnfoldedIdentifierExpr *element) {
2112+ _stubborn.postsetOf(element->offset(), true);
2113+ }
2114+
2115+}
2116\ No newline at end of file
2117
2118=== added file 'src/PetriEngine/Stubborn/ReachabilityStubbornSet.cpp'
2119--- src/PetriEngine/Stubborn/ReachabilityStubbornSet.cpp 1970-01-01 00:00:00 +0000
2120+++ src/PetriEngine/Stubborn/ReachabilityStubbornSet.cpp 2021-03-04 07:47:28 +0000
2121@@ -0,0 +1,41 @@
2122+/* Copyright (C) 2021 Nikolaj J. Ulrik <nikolaj@njulrik.dk>,
2123+ * Simon M. Virenfeldt <simon@simwir.dk>
2124+ *
2125+ * This program is free software: you can redistribute it and/or modify
2126+ * it under the terms of the GNU General Public License as published by
2127+ * the Free Software Foundation, either version 3 of the License, or
2128+ * (at your option) any later version.
2129+ *
2130+ * This program is distributed in the hope that it will be useful,
2131+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
2132+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
2133+ * GNU General Public License for more details.
2134+ *
2135+ * You should have received a copy of the GNU General Public License
2136+ * along with this program. If not, see <http://www.gnu.org/licenses/>.
2137+ */
2138+
2139+#include "PetriEngine/Stubborn/ReachabilityStubbornSet.h"
2140+#include "PetriEngine/Stubborn/InterestingTransitionVisitor.h"
2141+#include "PetriEngine/PQL/Contexts.h"
2142+
2143+namespace PetriEngine {
2144+ void ReachabilityStubbornSet::prepare(const Structures::State *state) {
2145+ _parent = state;
2146+ memset(_places_seen.get(), 0, _net.numberOfPlaces());
2147+ constructEnabled();
2148+ if (_ordering.size() == 0) return;
2149+ if (_ordering.size() == 1) {
2150+ _stubborn[_ordering.front()] = true;
2151+ return;
2152+ }
2153+ for (auto &q : _queries) {
2154+ q->evalAndSet(PQL::EvaluationContext((*_parent).marking(), &_net));
2155+ InterestingTransitionVisitor interesting{*this};
2156+
2157+ q->visit(interesting);
2158+ }
2159+
2160+ closure();
2161+ }
2162+}
2163
2164=== added file 'src/PetriEngine/Stubborn/StubbornSet.cpp'
2165--- src/PetriEngine/Stubborn/StubbornSet.cpp 1970-01-01 00:00:00 +0000
2166+++ src/PetriEngine/Stubborn/StubbornSet.cpp 2021-03-04 07:47:28 +0000
2167@@ -0,0 +1,302 @@
2168+/* Copyright (C) 2021 Nikolaj J. Ulrik <nikolaj@njulrik.dk>,
2169+ * Simon M. Virenfeldt <simon@simwir.dk>
2170+ *
2171+ * This program is free software: you can redistribute it and/or modify
2172+ * it under the terms of the GNU General Public License as published by
2173+ * the Free Software Foundation, either version 3 of the License, or
2174+ * (at your option) any later version.
2175+ *
2176+ * This program is distributed in the hope that it will be useful,
2177+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
2178+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
2179+ * GNU General Public License for more details.
2180+ *
2181+ * You should have received a copy of the GNU General Public License
2182+ * along with this program. If not, see <http://www.gnu.org/licenses/>.
2183+ */
2184+
2185+
2186+#include <PetriEngine/Stubborn/InterestingTransitionVisitor.h>
2187+#include "PetriEngine/Stubborn/StubbornSet.h"
2188+#include "PetriEngine/PQL/Contexts.h"
2189+
2190+namespace PetriEngine {
2191+ uint32_t StubbornSet::next() {
2192+ while (!_ordering.empty()) {
2193+ _current = _ordering.front();
2194+ _ordering.pop_front();
2195+ if (_stubborn[_current] && _enabled[_current]) {
2196+ return _current;
2197+ }
2198+ }
2199+ reset();
2200+ return std::numeric_limits<uint32_t>::max();
2201+ }
2202+
2203+ bool StubbornSet::checkPreset(uint32_t t) {
2204+ const TransPtr &ptr = transitions()[t];
2205+ uint32_t finv = ptr.inputs;
2206+ uint32_t linv = ptr.outputs;
2207+
2208+ for (; finv < linv; ++finv) {
2209+ const Invariant &inv = _net._invariants[finv];
2210+ if (_parent->marking()[inv.place] < inv.tokens) {
2211+ if (!inv.inhibitor) {
2212+ return false;
2213+ }
2214+ } else {
2215+ if (inv.inhibitor) {
2216+ return false;
2217+ }
2218+ }
2219+ }
2220+ return true;
2221+ }
2222+
2223+ bool StubbornSet::seenPre(uint32_t place) const {
2224+ return (_places_seen.get()[place] & 1) != 0;
2225+ }
2226+
2227+ bool StubbornSet::seenPost(uint32_t place) const {
2228+ return (_places_seen.get()[place] & 2) != 0;
2229+ }
2230+
2231+ void StubbornSet::presetOf(uint32_t place, bool make_closure) {
2232+ if ((_places_seen.get()[place] & 1) != 0) return;
2233+ _places_seen.get()[place] = _places_seen.get()[place] | 1;
2234+ for (uint32_t t = _places.get()[place].pre; t < _places.get()[place].post; t++) {
2235+ auto &tr = _transitions.get()[t];
2236+ addToStub(tr.index);
2237+ }
2238+ if (make_closure) closure();
2239+ }
2240+
2241+ void StubbornSet::postsetOf(uint32_t place, bool make_closure) {
2242+ if ((_places_seen.get()[place] & 2) != 0) return;
2243+ _places_seen.get()[place] = _places_seen.get()[place] | 2;
2244+ for (uint32_t t = _places.get()[place].post; t < _places.get()[place + 1].pre; t++) {
2245+ auto tr = _transitions.get()[t];
2246+ if (tr.direction < 0)
2247+ addToStub(tr.index);
2248+ }
2249+ if (make_closure) closure();
2250+ }
2251+
2252+ void StubbornSet::inhibitorPostsetOf(uint32_t place) {
2253+ if ((_places_seen.get()[place] & 4) != 0) return;
2254+ _places_seen.get()[place] = _places_seen.get()[place] | 4;
2255+ for (uint32_t &newstub : _inhibpost[place])
2256+ addToStub(newstub);
2257+ }
2258+
2259+ void StubbornSet::postPresetOf(uint32_t t, bool make_closure) {
2260+ const TransPtr &ptr = transitions()[t];
2261+ uint32_t finv = ptr.inputs;
2262+ uint32_t linv = ptr.outputs;
2263+ for (; finv < linv; finv++) { // pre-set of t
2264+ if (invariants()[finv].inhibitor) {
2265+ presetOf(invariants()[finv].place, make_closure);
2266+ } else {
2267+ postsetOf(invariants()[finv].place, make_closure);
2268+ }
2269+ }
2270+ }
2271+
2272+ void StubbornSet::constructEnabled() {
2273+ _ordering.clear();
2274+ for (uint32_t p = 0; p < _net.numberOfPlaces(); ++p) {
2275+ // orphans are currently under "place 0" as a special case
2276+ if (p == 0 || _parent->marking()[p] > 0) {
2277+ uint32_t t = placeToPtrs()[p];
2278+ uint32_t last = placeToPtrs()[p + 1];
2279+
2280+ for (; t != last; ++t) {
2281+ if (!checkPreset(t)) continue;
2282+ _enabled[t] = true;
2283+ _ordering.push_back(t);
2284+ }
2285+ }
2286+ }
2287+ }
2288+
2289+ void StubbornSet::checkForInhibitor() {
2290+ _netContainsInhibitorArcs = false;
2291+ for (uint32_t t = 0; t < _net._ntransitions; t++) {
2292+ const TransPtr &ptr = _net._transitions[t];
2293+ uint32_t finv = ptr.inputs;
2294+ uint32_t linv = ptr.outputs;
2295+ for (; finv < linv; finv++) { // Post set of places
2296+ if (_net._invariants[finv].inhibitor) {
2297+ _netContainsInhibitorArcs = true;
2298+ return;
2299+ }
2300+ }
2301+ }
2302+ }
2303+
2304+ void StubbornSet::constructPrePost() {
2305+ std::vector<std::pair<std::vector<trans_t>, std::vector<trans_t>>> tmp_places(_net._nplaces);
2306+
2307+ for (uint32_t t = 0; t < _net._ntransitions; t++) {
2308+ const TransPtr &ptr = _net._transitions[t];
2309+ uint32_t finv = ptr.inputs;
2310+ uint32_t linv = ptr.outputs;
2311+ for (; finv < linv; finv++) { // Post set of places
2312+ if (_net._invariants[finv].inhibitor) {
2313+ _inhibpost[_net._invariants[finv].place].push_back(t);
2314+ _netContainsInhibitorArcs = true;
2315+ } else {
2316+ tmp_places[_net._invariants[finv].place].second.emplace_back(t, _net._invariants[finv].direction);
2317+ }
2318+ }
2319+
2320+ finv = linv;
2321+ linv = _net._transitions[t + 1].inputs;
2322+ for (; finv < linv; finv++) { // Pre set of places
2323+ if (_net._invariants[finv].direction > 0)
2324+ tmp_places[_net._invariants[finv].place].first.emplace_back(t, _net._invariants[finv].direction);
2325+ }
2326+ }
2327+
2328+ // flatten
2329+ size_t ntrans = 0;
2330+ for (auto p : tmp_places) {
2331+ ntrans += p.first.size() + p.second.size();
2332+ }
2333+ _transitions.reset(new trans_t[ntrans]);
2334+
2335+ _places.reset(new place_t[_net._nplaces + 1]);
2336+ uint32_t offset = 0;
2337+ uint32_t p = 0;
2338+ for (; p < _net._nplaces; ++p) {
2339+ auto &pre = tmp_places[p].first;
2340+ auto &post = tmp_places[p].second;
2341+
2342+ // keep things nice for caches
2343+ std::sort(pre.begin(), pre.end());
2344+ std::sort(post.begin(), post.end());
2345+
2346+ _places.get()[p].pre = offset;
2347+ offset += pre.size();
2348+ _places.get()[p].post = offset;
2349+ offset += post.size();
2350+ for (size_t tn = 0; tn < pre.size(); ++tn) {
2351+ _transitions.get()[tn + _places.get()[p].pre] = pre[tn];
2352+ }
2353+
2354+ for (size_t tn = 0; tn < post.size(); ++tn) {
2355+ _transitions.get()[tn + _places.get()[p].post] = post[tn];
2356+ }
2357+
2358+ }
2359+ assert(offset == ntrans);
2360+ _places.get()[p].pre = offset;
2361+ _places.get()[p].post = offset;
2362+ }
2363+
2364+ void StubbornSet::constructDependency() {
2365+ memset(_dependency.get(), 0, sizeof(uint32_t) * _net._ntransitions);
2366+
2367+ for (uint32_t t = 0; t < _net._ntransitions; t++) {
2368+ uint32_t finv = _net._transitions[t].inputs;
2369+ uint32_t linv = _net._transitions[t].outputs;
2370+
2371+ for (; finv < linv; finv++) {
2372+ const Invariant &inv = _net._invariants[finv];
2373+ uint32_t p = inv.place;
2374+ uint32_t ntrans = (_places.get()[p + 1].pre - _places.get()[p].post);
2375+
2376+ for (uint32_t tIndex = 0; tIndex < ntrans; tIndex++) {
2377+ ++_dependency[t];
2378+ }
2379+ }
2380+ }
2381+ }
2382+
2383+
2384+ void StubbornSet::addToStub(uint32_t t) {
2385+ if (!_stubborn[t]) {
2386+ _stubborn[t] = true;
2387+ _unprocessed.push_back(t);
2388+ }
2389+ }
2390+
2391+ void StubbornSet::closure() {
2392+ while (!_unprocessed.empty()) {
2393+ uint32_t tr = _unprocessed.front();
2394+ _unprocessed.pop_front();
2395+ const TransPtr &ptr = transitions()[tr];
2396+ uint32_t finv = ptr.inputs;
2397+ uint32_t linv = ptr.outputs;
2398+ if (_enabled[tr]) {
2399+ for (; finv < linv; finv++) {
2400+ if (invariants()[finv].direction < 0) {
2401+ auto place = invariants()[finv].place;
2402+ for (uint32_t t = _places.get()[place].post; t < _places.get()[place + 1].pre; t++)
2403+ addToStub(_transitions.get()[t].index);
2404+ }
2405+ }
2406+ if (_netContainsInhibitorArcs) {
2407+ uint32_t next_finv = transitions()[tr + 1].inputs;
2408+ for (; linv < next_finv; linv++) {
2409+ if (invariants()[linv].direction > 0)
2410+ inhibitorPostsetOf(invariants()[linv].place);
2411+ }
2412+ }
2413+ } else {
2414+ bool ok = false;
2415+ bool inhib = false;
2416+ uint32_t cand = std::numeric_limits<uint32_t>::max();
2417+
2418+ // Lets try to see if we havent already added sufficient pre/post
2419+ // for this transition.
2420+ for (; finv < linv; ++finv) {
2421+ const Invariant &inv = invariants()[finv];
2422+ if ((*_parent).marking()[inv.place] < inv.tokens && !inv.inhibitor) {
2423+ inhib = false;
2424+ ok = (_places_seen.get()[inv.place] & 1) != 0;
2425+ cand = inv.place;
2426+ } else if ((*_parent).marking()[inv.place] >= inv.tokens && inv.inhibitor) {
2427+ inhib = true;
2428+ ok = (_places_seen.get()[inv.place] & 2) != 0;
2429+ cand = inv.place;
2430+ }
2431+ if (ok) break;
2432+
2433+ }
2434+
2435+ // OK, we didnt have sufficient, we just pick whatever is left
2436+ // in cand.
2437+ assert(cand != std::numeric_limits<uint32_t>::max());
2438+ if (!ok && cand != std::numeric_limits<uint32_t>::max()) {
2439+ if (!inhib) presetOf(cand);
2440+ else postsetOf(cand);
2441+ }
2442+ }
2443+ }
2444+ }
2445+
2446+ uint32_t StubbornSet::leastDependentEnabled() {
2447+ uint32_t tLeast = -1;
2448+ bool foundLeast = false;
2449+ for (uint32_t t = 0; t < _net.numberOfTransitions(); t++) {
2450+ if (_enabled[t]) {
2451+ if (!foundLeast) {
2452+ tLeast = t;
2453+ foundLeast = true;
2454+ } else {
2455+ if (_dependency[t] < _dependency[tLeast]) {
2456+ tLeast = t;
2457+ }
2458+ }
2459+ }
2460+ }
2461+ return tLeast;
2462+ }
2463+
2464+ void StubbornSet::reset() {
2465+ memset(_enabled.get(), false, sizeof(bool) * _net.numberOfTransitions());
2466+ memset(_stubborn.get(), false, sizeof(bool) * _net.numberOfTransitions());
2467+ _tid = 0;
2468+ }
2469+}
2470
2471=== modified file 'src/PetriParse/QueryXMLParser.cpp'
2472--- src/PetriParse/QueryXMLParser.cpp 2020-03-13 13:36:32 +0000
2473+++ src/PetriParse/QueryXMLParser.cpp 2021-03-04 07:47:28 +0000
2474@@ -569,7 +569,7 @@
2475 return nullptr;
2476 }
2477
2478-string QueryXMLParser::parsePlace(rapidxml::xml_node<>* element) {
2479+std::string QueryXMLParser::parsePlace(rapidxml::xml_node<>* element) {
2480 if (strcmp(element->name(), "place") != 0) return ""; // missing place tag
2481 string placeName = element->value();
2482 placeName.erase(std::remove_if(placeName.begin(), placeName.end(), ::isspace), placeName.end());

Subscribers

People subscribed via source and target branches