Merge lp:~verifypn-stub/verifypn/ctl-structural into lp:verifypn

Proposed by Peter Gjøl Jensen on 2018-01-04
Status: Merged
Approved by: Jiri Srba on 2018-01-04
Approved revision: 224
Merged at revision: 193
Proposed branch: lp:~verifypn-stub/verifypn/ctl-structural
Merge into: lp:verifypn
Diff against target: 872 lines (+240/-109)
16 files modified
CTL/CTLEngine.cpp (+2/-2)
CTL/CTLEngine.h (+1/-0)
CTL/PetriNets/OnTheFlyDG.cpp (+21/-22)
CTL/PetriNets/OnTheFlyDG.h (+26/-4)
PetriEngine/PQL/Expressions.cpp (+4/-2)
PetriEngine/PQL/Expressions.h (+15/-2)
PetriEngine/PQL/PQL.h (+1/-1)
PetriEngine/PetriNetBuilder.cpp (+2/-1)
PetriEngine/PetriNetBuilder.h (+4/-0)
PetriEngine/Reducer.cpp (+110/-45)
PetriEngine/Reducer.h (+7/-2)
PetriEngine/ReducingSuccessorGenerator.cpp (+9/-1)
PetriEngine/ReducingSuccessorGenerator.h (+4/-2)
PetriEngine/Structures/light_deque.h (+5/-0)
PetriEngine/SuccessorGenerator.h (+2/-1)
VerifyPN.cpp (+27/-24)
To merge this branch: bzr merge lp:~verifypn-stub/verifypn/ctl-structural
Reviewer Review Type Date Requested Status
Jiri Srba 2018-01-04 Approve on 2018-01-04
Review via email: mp+335697@code.launchpad.net

Description of the change

Adds structural reductions to the CTL verification -- only enabled if the formulas are next-free.
Also adds partial order reduction to EF leafs in CTL verification, although only yielding a minor speedup.

Consistent on 2017 models.
Improvements;

CTLCardinality:
r180: 3916
r187: 3922
r188: 3999
trunk: 4154
this: 4201

CTLFireability:
r180: 3111
r187: 3171
r188: 3248
trunk: 3575
this: 3655

To post a comment you must log in.
Jiri Srba (srba) wrote :

The switch that disables partial order reduction should be active also
for CTL verification for EF and AG leafs.

review: Needs Fixing
224. By Peter Gjøl Jensen on 2018-01-04

propagating switch for po-reduction to ctl-engine

Jiri Srba (srba) wrote :

Please, fix the warning:

CTL/PetriNets/OnTheFlyDG.cpp:24:9: warning: field '_redgen' will be initialized after field
      '_partial_order' [-Wreorder]
        _redgen(*t_net), _partial_order(partial_order) {
        ^

review: Needs Fixing
225. By Peter Gjøl Jensen on 2018-01-04

fixed reorder warning

Jiri Srba (srba) :
review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'CTL/CTLEngine.cpp'
2--- CTL/CTLEngine.cpp 2017-12-04 13:45:29 +0000
3+++ CTL/CTLEngine.cpp 2018-01-04 10:26:07 +0000
4@@ -66,7 +66,6 @@
5 cout << " Processed Edges : " << result.processedEdges << endl;
6 cout << " Processed N. Edges: " << result.processedNegationEdges << endl;
7 cout << " Explored Configs : " << result.exploredConfigurations << endl;
8- if(!only_stats) result.query->toString(cout);
9 std::cout << endl;
10 }
11 }
12@@ -77,6 +76,7 @@
13 bool gamemode,
14 bool printstatistics,
15 bool mccoutput,
16+ bool partial_order,
17 const std::vector<std::string>& querynames,
18 const std::vector<std::shared_ptr<Condition>>& queries,
19 const std::vector<size_t>& querynumbers
20@@ -90,7 +90,7 @@
21
22 for(auto qnum : querynumbers){
23 CTLResult result(queries[qnum]);
24- PetriNets::OnTheFlyDG graph(net);
25+ PetriNets::OnTheFlyDG graph(net, partial_order);
26 graph.setQuery(result.query);
27 std::shared_ptr<Algorithm::FixedPointAlgorithm> alg = nullptr;
28 bool solved = false;
29
30=== modified file 'CTL/CTLEngine.h'
31--- CTL/CTLEngine.h 2017-11-26 13:43:04 +0000
32+++ CTL/CTLEngine.h 2018-01-04 10:26:07 +0000
33@@ -16,6 +16,7 @@
34 bool gamemode,
35 bool printstatistics,
36 bool mccoutput,
37+ bool partial_order,
38 const std::vector<std::string>& querynames,
39 const std::vector<std::shared_ptr<PetriEngine::PQL::Condition>>& reducedQueries,
40 const std::vector<size_t>& ids);
41
42=== modified file 'CTL/PetriNets/OnTheFlyDG.cpp'
43--- CTL/PetriNets/OnTheFlyDG.cpp 2017-11-29 21:20:21 +0000
44+++ CTL/PetriNets/OnTheFlyDG.cpp 2018-01-04 10:26:07 +0000
45@@ -18,9 +18,10 @@
46
47 namespace PetriNets {
48
49-OnTheFlyDG::OnTheFlyDG(PetriEngine::PetriNet *t_net) : encoder(t_net->numberOfPlaces(), 0),
50+OnTheFlyDG::OnTheFlyDG(PetriEngine::PetriNet *t_net, bool partial_order) : encoder(t_net->numberOfPlaces(), 0),
51 edge_alloc(new linked_bucket_t<DependencyGraph::Edge,1024*10>(1)),
52- conf_alloc(new linked_bucket_t<char[sizeof(PetriConfig)], 1024*1024>(1)) {
53+ conf_alloc(new linked_bucket_t<char[sizeof(PetriConfig)], 1024*1024>(1)),
54+ _redgen(*t_net), _partial_order(partial_order) {
55 net = t_net;
56 n_places = t_net->numberOfPlaces();
57 n_transitions = t_net->numberOfTransitions();
58@@ -37,7 +38,6 @@
59 {
60 ((PetriConfig*)&(*conf_alloc)[i])->~PetriConfig();
61 }
62- std::cout << "NEDGES " << edge_alloc->size() << std::endl;
63 delete conf_alloc;
64 delete edge_alloc;
65 }
66@@ -176,7 +176,7 @@
67 if (valid || left != NULL) {
68 //if left side is guaranteed to be not satisfied, skip successor generation
69 Edge* leftEdge = NULL;
70- nextStates (query_marking,
71+ nextStates (query_marking, cond,
72 [&](){ leftEdge = newEdge(*v, std::numeric_limits<uint32_t>::max());},
73 [&](Marking& mark){
74 auto res = fastEval(cond, &mark);
75@@ -227,7 +227,7 @@
76 subquery->addTarget(c);
77 }
78 Edge* e1 = NULL;
79- nextStates(query_marking,
80+ nextStates(query_marking, cond,
81 [&](){e1 = newEdge(*v, std::numeric_limits<uint32_t>::max());},
82 [&](Marking& mark)
83 {
84@@ -264,7 +264,7 @@
85 auto cond = static_cast<AXCondition*>(v->query);
86 Edge* e = newEdge(*v, std::numeric_limits<uint32_t>::max());
87 Condition::Result allValid = Condition::RTRUE;
88- nextStates(query_marking,
89+ nextStates(query_marking, cond,
90 [](){},
91 [&](Marking& mark){
92 auto res = fastEval((*cond)[0], &mark);
93@@ -326,7 +326,7 @@
94
95 Configuration *left = NULL;
96 bool valid = false;
97- nextStates(query_marking,
98+ nextStates(query_marking, cond,
99 [&](){
100 auto r0 = fastEval((*cond)[0], &query_marking);
101 if (r0 == Condition::RUNKNOWN) {
102@@ -389,7 +389,7 @@
103 subquery->addTarget(c);
104 }
105
106- nextStates(query_marking,
107+ nextStates(query_marking, cond,
108 [](){},
109 [&](Marking& mark){
110 auto res = fastEval(cond, &mark);
111@@ -424,7 +424,7 @@
112 else if(v->query->getPath() == X){
113 auto cond = static_cast<EXCondition*>(v->query);
114 auto query = (*cond)[0];
115- nextStates(query_marking,
116+ nextStates(query_marking, cond,
117 [](){},
118 [&](Marking& marking) {
119 auto res = fastEval(query, &marking);
120@@ -478,25 +478,24 @@
121 return initial_config;
122 }
123
124-void OnTheFlyDG::nextStates(Marking& t_marking,
125+
126+void OnTheFlyDG::nextStates(Marking& t_marking, Condition* ptr,
127 std::function<void ()> pre,
128 std::function<bool (Marking&)> foreach,
129 std::function<void ()> post)
130 {
131-
132 bool first = true;
133- PetriEngine::SuccessorGenerator PNGen(*net);
134- PNGen.prepare(&query_marking);
135 memcpy(working_marking.marking(), query_marking.marking(), n_places*sizeof(PetriEngine::MarkVal));
136-
137-
138- while(PNGen.next(working_marking)){
139- if(first) pre();
140- first = false;
141- if(!foreach(working_marking))
142- {
143- break;
144- }
145+ auto qf = static_cast<QuantifierCondition*>(ptr);
146+ if(!_partial_order || ptr->getQuantifier() != E || ptr->getPath() != F || (*qf)[0]->isTemporal())
147+ {
148+ PetriEngine::SuccessorGenerator PNGen(*net);
149+ dowork<PetriEngine::SuccessorGenerator>(PNGen, first, pre, foreach);
150+ }
151+ else
152+ {
153+ _redgen.setQuery(ptr);
154+ dowork<PetriEngine::ReducingSuccessorGenerator>(_redgen, first, pre, foreach);
155 }
156
157 if(!first) post();
158
159=== modified file 'CTL/PetriNets/OnTheFlyDG.h'
160--- CTL/PetriNets/OnTheFlyDG.h 2017-11-26 22:46:37 +0000
161+++ CTL/PetriNets/OnTheFlyDG.h 2018-01-04 10:26:07 +0000
162@@ -12,6 +12,7 @@
163 #include "PetriEngine/Structures/ptrie_map.h"
164 #include "PetriEngine/Structures/AlignedEncoder.h"
165 #include "PetriEngine/Structures/linked_bucket.h"
166+#include "PetriEngine/ReducingSuccessorGenerator.h"
167
168 namespace PetriNets {
169 class OnTheFlyDG : public DependencyGraph::BasicDependencyGraph
170@@ -20,7 +21,7 @@
171 using Condition = PetriEngine::PQL::Condition;
172 using Condition_ptr = PetriEngine::PQL::Condition_ptr;
173 using Marking = PetriEngine::Structures::State;
174- OnTheFlyDG(PetriEngine::PetriNet *t_net);
175+ OnTheFlyDG(PetriEngine::PetriNet *t_net, bool partial_order);
176
177 virtual ~OnTheFlyDG();
178
179@@ -57,7 +58,6 @@
180 uint32_t n_places = 0;
181 size_t _markingCount = 0;
182 size_t _configurationCount = 0;
183-
184 //used after query is set
185 Condition_ptr query = nullptr;
186
187@@ -66,10 +66,27 @@
188 {
189 return fastEval(query.get(), unfolded);
190 }
191- void nextStates(Marking& t_marking,
192+ void nextStates(Marking& t_marking, Condition*,
193 std::function<void ()> pre,
194 std::function<bool (Marking&)> foreach,
195 std::function<void ()> post);
196+ template<typename T>
197+ void dowork(T& gen, bool& first,
198+ std::function<void ()>& pre,
199+ std::function<bool (Marking&)>& foreach)
200+ {
201+ gen.prepare(&query_marking);
202+
203+ while(gen.next(working_marking)){
204+ if(first) pre();
205+ first = false;
206+ if(!foreach(working_marking))
207+ {
208+ gen.reset();
209+ break;
210+ }
211+ }
212+ }
213 PetriConfig *createConfiguration(size_t marking, size_t own, Condition* query);
214 PetriConfig *createConfiguration(size_t marking, size_t own, const Condition_ptr& query)
215 {
216@@ -86,7 +103,12 @@
217
218 // Problem with linked bucket and complex constructor
219 linked_bucket_t<char[sizeof(PetriConfig)], 1024*1024>* conf_alloc = nullptr;
220-
221+
222+ PetriEngine::ReducingSuccessorGenerator _redgen;
223+ bool _partial_order = false;
224+
225 };
226+
227+
228 }
229 #endif // ONTHEFLYDG_H
230
231=== modified file 'PetriEngine/PQL/Expressions.cpp'
232--- PetriEngine/PQL/Expressions.cpp 2017-12-14 08:59:40 +0000
233+++ PetriEngine/PQL/Expressions.cpp 2018-01-04 10:26:07 +0000
234@@ -2997,11 +2997,13 @@
235 }
236
237 void SimpleQuantifierCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const{
238- // Not implemented
239+ _cond->findInteresting(generator, negated);
240 }
241
242 void UntilCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const{
243- // Not implemented
244+ _cond1->findInteresting(generator, negated);
245+ _cond1->findInteresting(generator, !negated);
246+ _cond2->findInteresting(generator, negated);
247 }
248
249 void AndCondition::findInteresting(ReducingSuccessorGenerator& generator, bool negated) const {
250
251=== modified file 'PetriEngine/PQL/Expressions.h'
252--- PetriEngine/PQL/Expressions.h 2017-12-13 14:17:08 +0000
253+++ PetriEngine/PQL/Expressions.h 2018-01-04 10:26:07 +0000
254@@ -254,6 +254,7 @@
255 bool isUpperBound() override;
256 void findInteresting(ReducingSuccessorGenerator& generator, bool negated) const override;
257 virtual const Condition_ptr& operator[] (size_t i) const override { return _cond;}
258+ virtual bool containsNext() const override { return _cond->containsNext(); }
259 private:
260 virtual std::string op() const = 0;
261
262@@ -272,7 +273,7 @@
263 Quantifier getQuantifier() const override { return Quantifier::E; }
264 Path getPath() const override { return Path::X; }
265 uint32_t distance(DistanceContext& context) const override;
266-
267+ bool containsNext() const override { return true; }
268 private:
269 std::string op() const override;
270 };
271@@ -324,6 +325,7 @@
272 Quantifier getQuantifier() const override { return Quantifier::A; }
273 Path getPath() const override { return Path::X; }
274 uint32_t distance(DistanceContext& context) const override;
275+ bool containsNext() const override { return true; }
276 private:
277 std::string op() const override;
278 };
279@@ -385,7 +387,7 @@
280 { if(i == 0) return _cond1; return _cond2;}
281 Path getPath() const override
282 { return Path::U; }
283-
284+ bool containsNext() const override { return _cond1->containsNext() || _cond2->containsNext(); }
285 private:
286 virtual std::string op() const = 0;
287
288@@ -463,6 +465,9 @@
289 { return _compiled->getQueryType(); }
290 int formulaSize() const override
291 { return _compiled->formulaSize(); }
292+ bool containsNext() const override
293+ { return false; }
294+
295 private:
296 std::string _name;
297 Condition_ptr _compiled;
298@@ -503,6 +508,8 @@
299 auto end() const { return _conds.end(); }
300 bool empty() const { return _conds.size() == 0; }
301 bool singular() const { return _conds.size() == 1; }
302+ bool containsNext() const override
303+ { return std::any_of(begin(), end(), [](auto& a){return a->containsNext();}); }
304 protected:
305 LogicalCondition() {};
306 Retval simplifyOr(SimplificationContext& context) const;
307@@ -632,6 +639,8 @@
308 (_constraints[0]._lower == 0 ||
309 _constraints[0]._upper == std::numeric_limits<uint32_t>::max());
310 };
311+ bool containsNext() const override { return false;}
312+
313 private:
314 std::vector<cons_t> _constraints;
315 bool _negated = false;
316@@ -665,6 +674,7 @@
317 if(id == 0) return _expr1;
318 else return _expr2;
319 }
320+ bool containsNext() const override { return false; }
321 protected:
322 uint32_t _distance(DistanceContext& c,
323 std::function<uint32_t(uint32_t, uint32_t, bool)> d) const
324@@ -825,6 +835,7 @@
325 CTLType getQueryType() const override { return CTLType::LOPERATOR; }
326 const Condition_ptr& operator[](size_t i) const { return _cond; };
327 virtual bool isTemporal() const override { return _temporal;}
328+ bool containsNext() const override { return _cond->containsNext(); }
329
330 private:
331 Condition_ptr _cond;
332@@ -864,6 +875,7 @@
333 Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
334 Path getPath() const override { return Path::pError; }
335 CTLType getQueryType() const override { return CTLType::EVAL; }
336+ bool containsNext() const override { return false; }
337 private:
338 const bool _value;
339 };
340@@ -894,6 +906,7 @@
341 Quantifier getQuantifier() const override { return Quantifier::EMPTY; }
342 Path getPath() const override { return Path::pError; }
343 CTLType getQueryType() const override { return CTLType::EVAL; }
344+ bool containsNext() const override { return false; }
345 };
346
347 }
348
349=== modified file 'PetriEngine/PQL/PQL.h'
350--- PetriEngine/PQL/PQL.h 2017-12-11 08:24:36 +0000
351+++ PetriEngine/PQL/PQL.h 2018-01-04 10:26:07 +0000
352@@ -289,7 +289,7 @@
353 virtual Path getPath() const = 0;
354 static std::shared_ptr<Condition>
355 initialMarkingRW(std::function<std::shared_ptr<Condition> ()> func, negstat_t& stats, const EvaluationContext& context, bool nested, bool negated);
356-
357+ virtual bool containsNext() const = 0;
358 protected:
359 //Value for checking if condition is trivially true or false.
360 //0 is undecided (default), 1 is true, 2 is false.
361
362=== modified file 'PetriEngine/PetriNetBuilder.cpp'
363--- PetriEngine/PetriNetBuilder.cpp 2017-12-08 12:21:38 +0000
364+++ PetriEngine/PetriNetBuilder.cpp 2018-01-04 10:26:07 +0000
365@@ -395,7 +395,8 @@
366 QueryPlaceAnalysisContext placecontext(getPlaceNames(), getTransitionNames(), net);
367 for(uint32_t i = 0; i < queries.size(); ++i)
368 {
369- if(results[i] == Reachability::ResultPrinter::Unknown)
370+ if(results[i] == Reachability::ResultPrinter::Unknown ||
371+ results[i] == Reachability::ResultPrinter::CTL )
372 {
373 queries[i]->analyze(placecontext);
374 }
375
376=== modified file 'PetriEngine/PetriNetBuilder.h'
377--- PetriEngine/PetriNetBuilder.h 2017-12-08 13:28:43 +0000
378+++ PetriEngine/PetriNetBuilder.h 2018-01-04 10:26:07 +0000
379@@ -112,6 +112,10 @@
380 return reducer.RuleE();
381 }
382
383+ size_t RuleF() const {
384+ return reducer.RuleF();
385+ }
386+
387 Reducer* getReducer() { return &reducer; }
388
389 std::vector<std::pair<std::string, uint32_t>> orphanPlaces() const {
390
391=== modified file 'PetriEngine/Reducer.cpp'
392--- PetriEngine/Reducer.cpp 2017-12-08 13:34:25 +0000
393+++ PetriEngine/Reducer.cpp 2018-01-04 10:26:07 +0000
394@@ -10,11 +10,12 @@
395 #include "PetriNetBuilder.h"
396 #include <PetriParse/PNMLParser.h>
397 #include <queue>
398+#include <set>
399
400 namespace PetriEngine {
401
402 Reducer::Reducer(PetriNetBuilder* p)
403- : _removedTransitions(0), _removedPlaces(0), _ruleA(0), _ruleB(0), _ruleC(0), _ruleD(0), _ruleE(0), parent(p) {
404+ : _removedTransitions(0), _removedPlaces(0), _ruleA(0), _ruleB(0), _ruleC(0), _ruleD(0), _ruleE(0), _ruleF(0), parent(p) {
405 }
406
407 Reducer::~Reducer() {
408@@ -180,12 +181,14 @@
409 assert(!t.skip || (t.pre.size() == 0 && t.post.size() == 0));
410 for(Arc& a : t.pre)
411 {
412+ assert(a.weight > 0);
413 Place& p = parent->_places[a.place];
414 assert(!p.skip);
415 assert(std::find(p.consumers.begin(), p.consumers.end(), i) != p.consumers.end());
416 }
417 for(Arc& a : t.post)
418 {
419+ assert(a.weight > 0);
420 Place& p = parent->_places[a.place];
421 assert(!p.skip);
422 assert(std::find(p.producers.begin(), p.producers.end(), i) != p.producers.end());
423@@ -239,14 +242,10 @@
424
425 // A2. we have more/less than one arc in pre or post
426 // checked first to avoid out-of-bounds when looking up indexes.
427- if(trans.pre.size() != 1 || trans.post.size() != 1) continue;
428+ if(trans.pre.size() != 1) continue;
429
430 uint32_t pPre = trans.pre[0].place;
431- uint32_t pPost = trans.post[0].place;
432-
433- // A1. continue if source and destination are the same
434- if (pPre == pPost) continue;
435-
436+
437 // A2. Check that pPre goes only to t
438 if(parent->_places[pPre].consumers.size() != 1) continue;
439
440@@ -255,10 +254,21 @@
441 if(trans.pre[0].weight != 1 || trans.post[0].weight < 1) continue;
442
443 // A4. Do inhibitor check, neither T, pPre or pPost can be involved with any inhibitor
444- if(parent->_places[pPre].inhib || parent->_places[pPost].inhib || trans.inhib) continue;
445-
446+ if(parent->_places[pPre].inhib|| trans.inhib) continue;
447+
448 // A5. dont mess with query!
449- if(placeInQuery[pPre] > 0 || placeInQuery[pPost]) continue;
450+ if(placeInQuery[pPre] > 0) continue;
451+ // check A1, A4 and A5 for post
452+ bool ok = true;
453+ for(auto& pPost : trans.post)
454+ {
455+ if(parent->_places[pPost.place].inhib || pPre == pPost.place || placeInQuery[pPost.place] > 0)
456+ {
457+ ok = false;
458+ break;
459+ }
460+ }
461+ if(!ok) continue;
462
463 continueReductions = true;
464 _ruleA++;
465@@ -280,40 +290,45 @@
466 }
467 }
468
469- size_t weight = trans.post[0].weight;
470-
471- // UA2. move the token for the initial marking, makes things simpler.
472- parent->initialMarking[pPost] += (parent->initialMarking[pPre] * weight);
473+ for(auto& pPost : trans.post)
474+ {
475+ // UA2. move the token for the initial marking, makes things simpler.
476+ parent->initialMarking[pPost.place] += (parent->initialMarking[pPre] * pPost.weight);
477+ }
478 parent->initialMarking[pPre] = 0;
479
480 // Remove transition t and the place that has no tokens in m0
481 // UA1. remove transition
482+ auto toMove = trans.post;
483 skipTransition(t);
484- assert(pPost != pPre);
485
486 // UA2. update arcs
487 for(auto& _t : parent->_places[pPre].producers)
488 {
489- assert(pPre != pPost);
490 assert(_t != t);
491 // move output-arcs to post.
492- Transition& trans = getTransition(_t);
493- auto source = getOutArc(trans, pPre);
494- assert(source != trans.pre.end());
495- auto dest = getOutArc(trans, pPost);
496- if(dest == trans.post.end())
497- {
498- source->place = pPost;
499- source->weight *= weight;
500- parent->_places[pPost].producers.push_back(_t);
501-
502- std::sort(trans.post.begin(), trans.post.end());
503- std::sort( parent->_places[pPost].producers.begin(),
504- parent->_places[pPost].producers.end());
505- }
506- else
507- {
508- dest->weight += (source->weight * weight);
509+ Transition& src = getTransition(_t);
510+ auto source = *getOutArc(src, pPre);
511+ for(auto& pPost : toMove)
512+ {
513+ Arc a;
514+ a.place = pPost.place;
515+ a.weight = source.weight * pPost.weight;
516+ assert(a.weight > 0);
517+ a.inhib = false;
518+ auto dest = std::lower_bound(src.post.begin(), src.post.end(), a);
519+ if(dest == src.post.end() || dest->place != pPost.place)
520+ {
521+ dest = src.post.insert(dest, a);
522+ auto& prod = parent->_places[pPost.place].producers;
523+ auto lb = std::lower_bound(prod.begin(), prod.end(), _t);
524+ prod.insert(lb, _t);
525+ }
526+ else
527+ {
528+ dest->weight += (source.weight * pPost.weight);
529+ }
530+ assert(dest->weight > 0);
531 }
532 }
533 // UA1. remove place
534@@ -714,7 +729,8 @@
535 if(placeInQuery[p] > 0) continue;
536 if(place.producers.size() > place.consumers.size()) continue;
537
538- bool ok = true;
539+ std::set<uint32_t> notenabled;
540+ bool ok = true;
541 for(uint cons : place.consumers)
542 {
543 Transition& t = getTransition(cons);
544@@ -723,12 +739,21 @@
545 ok = false;
546 break;
547 }
548+ else
549+ {
550+ notenabled.insert(cons);
551+ }
552 }
553
554 if(!ok) continue;
555-
556+
557 for(uint prod : place.producers)
558 {
559+ if(notenabled.count(prod) == 0)
560+ {
561+ ok = false;
562+ break;
563+ }
564 // check that producing arcs originate from transition also
565 // consuming. If so, we know it will never fire.
566 Transition& t = getTransition(prod);
567@@ -741,24 +766,63 @@
568 }
569
570 if(!ok) continue;
571+
572+ _ruleE++;
573+ continueReductions = true;
574
575 parent->initialMarking[p] = 0;
576
577- auto torem = place.consumers;
578- for(uint cons : torem)
579- {
580+ bool skipplace = notenabled.size() == place.consumers.size();
581+ for(uint cons : notenabled)
582 skipTransition(cons);
583+
584+ if(skipplace)
585+ skipPlace(p);
586+
587+ }
588+ assert(consistent());
589+ return continueReductions;
590+ }
591+
592+ bool Reducer::ReducebyRuleF(uint32_t* placeInQuery) {
593+ bool continueReductions = false;
594+ const size_t numberofplaces = parent->numberOfPlaces();
595+ for(uint32_t p = 0; p < numberofplaces; ++p)
596+ {
597+ if(hasTimedout()) return false;
598+ Place& place = parent->_places[p];
599+ if(place.skip) continue;
600+ if(place.inhib) continue;
601+ if(placeInQuery[p] > 0) continue;
602+ if(place.consumers.size() > 0) continue;
603+
604+ ++_ruleF;
605+ continueReductions = true;
606+ skipPlace(p);
607+ std::vector<uint32_t> torem;
608+ for(auto& t : place.producers)
609+ {
610+ auto& trans = parent->_transitions[t];
611+ if(trans.post.size() != 0)
612+ continue;
613+ bool ok = true;
614+ for(auto& a : trans.pre)
615+ {
616+ if(placeInQuery[a.place] > 0)
617+ {
618+ ok = false;
619+ }
620+ }
621+ if(ok) torem.push_back(t);
622 }
623-
624- skipPlace(p);
625- _ruleE++;
626- continueReductions = true;
627+
628+ for(auto t : torem)
629+ skipTransition(t);
630+ assert(consistent());
631 }
632- assert(consistent());
633 return continueReductions;
634 }
635
636-
637 void Reducer::Reduce(QueryPlaceAnalysisContext& context, int enablereduction, bool reconstructTrace, int timeout) {
638 this->_timeout = timeout;
639 _timer = std::chrono::high_resolution_clock::now();
640@@ -773,11 +837,12 @@
641 changed |= ReducebyRuleA(context.getQueryPlaceCount());
642 changed |= ReducebyRuleB(context.getQueryPlaceCount());
643 changed |= ReducebyRuleE(context.getQueryPlaceCount());
644+ changed |= ReducebyRuleF(context.getQueryPlaceCount());
645 } while(changed && !hasTimedout());
646 // RuleC and RuleD are expensive, so wait with those till nothing else changes
647 changed |= ReducebyRuleD(context.getQueryPlaceCount());
648 changed |= ReducebyRuleC(context.getQueryPlaceCount());
649- } while(changed);
650+ } while(!hasTimedout() && changed);
651
652 } else if (enablereduction == 2) { // for k-boundedness checking only rules A and D are applicable
653 while ( (
654
655=== modified file 'PetriEngine/Reducer.h'
656--- PetriEngine/Reducer.h 2017-12-13 14:17:08 +0000
657+++ PetriEngine/Reducer.h 2018-01-04 10:26:07 +0000
658@@ -114,7 +114,11 @@
659 size_t RuleE() const {
660 return _ruleE;
661 }
662-
663+
664+ size_t RuleF() const {
665+ return _ruleF;
666+ }
667+
668 void postFire(std::ostream&, const std::string& transition);
669 void extraConsume(std::ostream&, const std::string& transition);
670 void initFire(std::ostream&);
671@@ -122,7 +126,7 @@
672 private:
673 size_t _removedTransitions;
674 size_t _removedPlaces;
675- size_t _ruleA, _ruleB, _ruleC, _ruleD, _ruleE;
676+ size_t _ruleA, _ruleB, _ruleC, _ruleD, _ruleE, _ruleF;
677 PetriNetBuilder* parent;
678 bool reconstructTrace = false;
679 std::chrono::high_resolution_clock::time_point _timer;
680@@ -134,6 +138,7 @@
681 bool ReducebyRuleC(uint32_t* placeInQuery);
682 bool ReducebyRuleD(uint32_t* placeInQuery);
683 bool ReducebyRuleE(uint32_t* placeInQuery);
684+ bool ReducebyRuleF(uint32_t* placeInQuery);
685
686 std::string getTransitionName(uint32_t transition);
687 std::string getPlaceName(uint32_t place);
688
689=== modified file 'PetriEngine/ReducingSuccessorGenerator.cpp'
690--- PetriEngine/ReducingSuccessorGenerator.cpp 2017-12-05 15:13:40 +0000
691+++ PetriEngine/ReducingSuccessorGenerator.cpp 2018-01-04 10:26:07 +0000
692@@ -18,7 +18,9 @@
693 }
694
695 ReducingSuccessorGenerator::ReducingSuccessorGenerator(const PetriNet& net, std::vector<std::shared_ptr<PQL::Condition> >& queries) : ReducingSuccessorGenerator(net) {
696- _queries = queries;
697+ _queries.reserve(queries.size());
698+ for(auto& q : queries)
699+ _queries.push_back(q.get());
700 }
701
702 ReducingSuccessorGenerator::~ReducingSuccessorGenerator() {
703@@ -182,6 +184,12 @@
704 void ReducingSuccessorGenerator::prepare(const Structures::State* state) {
705 _parent = state;
706 constructEnabled();
707+ if(_ordering.size() == 0) return;
708+ if(_ordering.size() == 1)
709+ {
710+ _stubborn[_ordering.front()] = true;
711+ return;
712+ }
713 for (auto &q : _queries) {
714 q->evalAndSet(PQL::EvaluationContext((*_parent).marking(), &_net));
715 q->findInteresting(*this, false);
716
717=== modified file 'PetriEngine/ReducingSuccessorGenerator.h'
718--- PetriEngine/ReducingSuccessorGenerator.h 2017-05-10 11:10:00 +0000
719+++ PetriEngine/ReducingSuccessorGenerator.h 2018-01-04 10:26:07 +0000
720@@ -29,6 +29,9 @@
721 {
722 return _current;
723 }
724+ void setQuery(PQL::Condition* ptr) { _queries.clear(); _queries = {ptr};}
725+ void reset();
726+
727 private:
728 bool *_enabled, *_stubborn;
729 std::unique_ptr<place_t[]> _places;
730@@ -39,8 +42,7 @@
731 bool _netContainsInhibitorArcs;
732 std::vector<std::vector<uint32_t>> _inhibpost;
733
734- std::vector<std::shared_ptr<PQL::Condition> > _queries;
735- void reset();
736+ std::vector<PQL::Condition* > _queries;
737 void constructEnabled();
738 void constructPrePost();
739 void constructDependency();
740
741=== modified file 'PetriEngine/Structures/light_deque.h'
742--- PetriEngine/Structures/light_deque.h 2017-03-05 16:08:26 +0000
743+++ PetriEngine/Structures/light_deque.h 2018-01-04 10:26:07 +0000
744@@ -48,6 +48,11 @@
745 return _front == _back;
746 }
747
748+ size_t size()
749+ {
750+ return _back - _front;
751+ }
752+
753 T front()
754 {
755 return _data.get()[_front];
756
757=== modified file 'PetriEngine/SuccessorGenerator.h'
758--- PetriEngine/SuccessorGenerator.h 2017-12-05 02:09:55 +0000
759+++ PetriEngine/SuccessorGenerator.h 2018-01-04 10:26:07 +0000
760@@ -35,6 +35,8 @@
761 return _parent->marking();
762 }
763
764+ void reset();
765+
766 protected:
767 /**
768 * Checks if the conditions are met for fireing t, if write != NULL,
769@@ -63,7 +65,6 @@
770 const Structures::State* _parent;
771 uint32_t _suc_pcounter;
772 uint32_t _suc_tcounter;
773- void reset();
774
775 friend class ReducingSuccessorGenerator;
776 };
777
778=== modified file 'VerifyPN.cpp'
779--- VerifyPN.cpp 2017-12-12 10:13:45 +0000
780+++ VerifyPN.cpp 2018-01-04 10:26:07 +0000
781@@ -478,7 +478,8 @@
782 << "Applications of rule B: " << builder.RuleB() << std::endl
783 << "Applications of rule C: " << builder.RuleC() << std::endl
784 << "Applications of rule D: " << builder.RuleD() << std::endl
785- << "Applications of rule E: " << builder.RuleE() << std::endl;
786+ << "Applications of rule E: " << builder.RuleE() << std::endl
787+ << "Applications of rule F: " << builder.RuleF() << std::endl;
788 }
789 }
790 }
791@@ -656,7 +657,26 @@
792
793 if(alldone) return SuccessCode;
794 }
795-
796+
797+ //--------------------- Apply Net Reduction ---------------//
798+
799+ if ( (options.enablereduction == 1 || options.enablereduction == 2)
800+ && std::all_of(queries.begin(), queries.end(), [](auto& a){ return !a->containsNext(); })) {
801+ // Compute how many times each place appears in the query
802+ builder.startTimer();
803+ builder.reduce(queries, results, options.enablereduction, options.trace, nullptr, options.reductionTimeout);
804+ printer.setReducer(builder.getReducer());
805+ }
806+
807+ printStats(builder, options);
808+
809+ auto net = std::unique_ptr<PetriNet>(builder.makePetriNet());
810+
811+ for(auto& q : queries)
812+ {
813+ q->indexPlaces(builder.getPlaceNames());
814+ }
815+
816 //----------------------- Verify CTL queries -----------------------//
817 std::vector<size_t> ctl_ids;
818 for(size_t i = 0; i < queries.size(); ++i)
819@@ -670,24 +690,25 @@
820 if (ctl_ids.size() > 0) {
821 options.isctl=true;
822 PetriEngine::Reachability::Strategy reachabilityStrategy=options.strategy;
823- std::unique_ptr<PetriNet> ctlnet(builder.makePetriNet());
824+
825 // Assign indexes
826- if(queries.size() == 0 || contextAnalysis(builder, ctlnet.get(), queries) != ContinueCode) return ErrorCode;
827+ if(queries.size() == 0 || contextAnalysis(builder, net.get(), queries) != ContinueCode) return ErrorCode;
828 if(options.strategy == DEFAULT) options.strategy = PetriEngine::Reachability::DFS;
829 if(options.strategy != PetriEngine::Reachability::DFS){
830 fprintf(stdout, "Search strategy was changed to DFS as the CTL engine is called.\n");
831 options.strategy = PetriEngine::Reachability::DFS;
832 }
833- v = CTLMain(ctlnet.get(),
834+ v = CTLMain(net.get(),
835 options.ctlalgorithm,
836 options.strategy,
837 options.gamemode,
838 options.printstatistics,
839 true,
840+ options.stubbornreduction,
841 querynames,
842 queries,
843 ctl_ids);
844-
845+
846 if (std::find(results.begin(), results.end(), ResultPrinter::Unknown) == results.end()) {
847 return v;
848 }
849@@ -695,24 +716,6 @@
850 options.strategy=reachabilityStrategy;
851 }
852 options.isctl=false;
853- //--------------------- Apply Net Reduction ---------------//
854-
855- if (options.enablereduction == 1 || options.enablereduction == 2) {
856- // Compute how many times each place appears in the query
857- builder.startTimer();
858- std::unique_ptr<PetriNet> net(builder.makePetriNet(false));
859- builder.reduce(queries, results, options.enablereduction, options.trace, net.get(), options.reductionTimeout);
860- printer.setReducer(builder.getReducer());
861- }
862-
863- printStats(builder, options);
864-
865- std::unique_ptr<PetriNet> net(builder.makePetriNet());
866-
867- for(auto& q : queries)
868- {
869- q->indexPlaces(builder.getPlaceNames());
870- }
871
872 //----------------------- Siphon Trap ------------------------//
873

Subscribers

People subscribed via source and target branches