verifypn

Merge lp:~verifypn-maintainers/verifypn/placeBoundStatistics into lp:~verifypn-maintainers/verifypn/trunk

  1. placeBoundStatistics
  2. Merge into trunk
Proposed by Jiri Srba
Status: Merged
Approved by: Jiri Srba
Approved revision: 47
Merged at revision: 45
Proposed branch: lp:~verifypn-maintainers/verifypn/placeBoundStatistics
Merge into: lp:~verifypn-maintainers/verifypn/trunk
Diff against target: 540 lines (+95/-47)
16 files modified
PetriEngine/PetriNet.cpp (+25/-17)
PetriEngine/PetriNet.h (+4/-0)
PetriEngine/Reachability/BestFSCooling.cpp (+2/-1)
PetriEngine/Reachability/BestFirstReachabilitySearch.cpp (+4/-4)
PetriEngine/Reachability/BreadthFirstReachabilitySearch.cpp (+4/-4)
PetriEngine/Reachability/DepthFirstReachabilitySearch.cpp (+4/-4)
PetriEngine/Reachability/HashUnderApproximation.cpp (+2/-2)
PetriEngine/Reachability/HeuristicDFS.cpp (+2/-2)
PetriEngine/Reachability/MagicSearch.cpp (+3/-1)
PetriEngine/Reachability/RandomDFS.cpp (+4/-4)
PetriEngine/Reachability/ReachabilityResult.h (+5/-0)
PetriEngine/Reachability/StateSearch.cpp (+3/-3)
PetriEngine/Reachability/UltimateSearch.cpp (+4/-4)
PetriEngine/Reducer.cpp (+4/-0)
PetriEngine/Structures/StateSet.h (+15/-1)
VerifyPN.cpp (+10/-0)
To merge this branch: bzr merge lp:~verifypn-maintainers/verifypn/placeBoundStatistics
Reviewer Review Type Date Requested Status
Jonas Finnemann Jensen Approve
Jiri Srba Approve
Review via email: mp+211222@code.launchpad.net

Commit message

Added place bound statistics (max number of tokens in every place during the search).

Description of the change

Added place bound statistics (max number of tokens in every place during the search).
TAPAAL GUI branch is also proposed for merge to TAPAAL trunk.

To post a comment you must log in.
Revision history for this message
Jiri Srba (srba) wrote :

tested and works fine

review: Approve
Revision history for this message
Jonas Finnemann Jensen (jopsen) wrote :

Looks about right...

review: Needs Fixing
Revision history for this message
Jiri Srba (srba) wrote :

So why do you say it needs fixing?

Revision history for this message
Jonas Finnemann Jensen (jopsen) wrote :

I didn't just hit the wrong button :)

review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'PetriEngine/PetriNet.cpp'
2--- PetriEngine/PetriNet.cpp 2014-03-10 20:08:13 +0000
3+++ PetriEngine/PetriNet.cpp 2014-03-16 21:01:52 +0000
4@@ -54,25 +54,33 @@
5 for (int i = 0; i < transitions; i++) {
6 skipTransitions[i] = false;
7 }
8+ skipPlaces = new bool[places];
9+ for (int i = 0; i < places; i++) {
10+ skipPlaces[i] = false;
11+ }
12 }
13
14-PetriNet::~PetriNet(){
15- if(_ranges)
16- delete[] _ranges;
17- _ranges = NULL;
18- if(_tm)
19- delete[] _tm;
20- _tm = NULL;
21- //Conditions and assignments is allocated in the same block
22- if(_conditions)
23- delete[] (char*)_conditions;
24- _conditions = NULL;
25- _assignments = NULL;
26- if (skipTransitions) {
27- delete[] skipTransitions;
28- }
29- skipTransitions = NULL;
30-}
31+ PetriNet::~PetriNet() {
32+ if (_ranges)
33+ delete[] _ranges;
34+ _ranges = NULL;
35+ if (_tm)
36+ delete[] _tm;
37+ _tm = NULL;
38+ //Conditions and assignments is allocated in the same block
39+ if (_conditions)
40+ delete[] (char*) _conditions;
41+ _conditions = NULL;
42+ _assignments = NULL;
43+ if (skipTransitions) {
44+ delete[] skipTransitions;
45+ }
46+ skipTransitions = NULL;
47+ if (skipPlaces) {
48+ delete[] skipPlaces;
49+ }
50+ skipPlaces = NULL;
51+ }
52
53 bool PetriNet::fire(unsigned int t,
54 const MarkVal* m,
55
56=== modified file 'PetriEngine/PetriNet.h'
57--- PetriEngine/PetriNet.h 2014-03-11 07:51:37 +0000
58+++ PetriEngine/PetriNet.h 2014-03-16 21:01:52 +0000
59@@ -84,6 +84,9 @@
60 const std::vector<std::string>& transitionNames() const {return _transitions;}
61 void skipTransition(unsigned int t) { skipTransitions[t]=true; }
62 bool isTransitionSkipped(unsigned int t) { return skipTransitions[t]; }
63+ void skipPlace(unsigned int p) { skipPlaces[p]=true; }
64+ bool isPlaceSkipped(unsigned int p) { return skipPlaces[p]; }
65+
66
67 private:
68 std::vector<std::string> _places;
69@@ -108,6 +111,7 @@
70 PQL::Condition** _conditions;
71 PQL::AssignmentExpression** _assignments;
72 bool* skipTransitions;
73+ bool* skipPlaces;
74
75 friend class PetriNetBuilder;
76 friend class Reducer;
77
78=== modified file 'PetriEngine/Reachability/BestFSCooling.cpp'
79--- PetriEngine/Reachability/BestFSCooling.cpp 2014-03-10 22:27:51 +0000
80+++ PetriEngine/Reachability/BestFSCooling.cpp 2014-03-16 21:01:52 +0000
81@@ -104,6 +104,7 @@
82 states.discovered(),
83 enabledTransitionsCount,
84 states.maxTokens(),
85+ states.maxPlaceBound(),
86 ns->pathLength(),
87 ns->trace());
88
89@@ -129,7 +130,7 @@
90 }
91
92 return ReachabilityResult(ReachabilityResult::NotSatisfied,
93- "Query cannot be satisfied!", expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens());
94+ "Query cannot be satisfied!", expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound());
95 }
96
97 double BestFSCooling::priority(const Structures::State *state,
98
99=== modified file 'PetriEngine/Reachability/BestFirstReachabilitySearch.cpp'
100--- PetriEngine/Reachability/BestFirstReachabilitySearch.cpp 2014-03-10 22:27:51 +0000
101+++ PetriEngine/Reachability/BestFirstReachabilitySearch.cpp 2014-03-16 21:01:52 +0000
102@@ -95,7 +95,7 @@
103 //ns->dumpTrace(net);
104 return ReachabilityResult(ReachabilityResult::Satisfied,
105 "Query was satified!", expandedStates, exploredStates,
106- states.discovered(), enabledTransitionsCount, states.maxTokens(), ns->pathLength(), ns->trace());
107+ states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound(), ns->pathLength(), ns->trace());
108 }
109
110 // Insert in queue, with given priority
111@@ -109,7 +109,7 @@
112 ns2->setParent(ns);
113 return ReachabilityResult(ReachabilityResult::Satisfied,
114 "Query was satified!", expandedStates, exploredStates,
115- states.discovered(), enabledTransitionsCount, states.maxTokens(), ns2->pathLength(), ns2->trace());
116+ states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound(), ns2->pathLength(), ns2->trace());
117 }
118 double p = priority(ns2, query, net);
119 if(p <= bestp){
120@@ -125,7 +125,7 @@
121 if(query->evaluate(*ns2, &net)){
122 return ReachabilityResult(ReachabilityResult::Satisfied,
123 "Query was satisfied!", expandedStates, exploredStates,
124- states.discovered(), enabledTransitionsCount, states.maxTokens(), ns2->pathLength(), ns2->trace());
125+ states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound(), ns2->pathLength(), ns2->trace());
126 }
127 }
128 if(states.add(ns2)){
129@@ -143,7 +143,7 @@
130 }
131
132 return ReachabilityResult(ReachabilityResult::NotSatisfied,
133- "Query cannot be satisfied!", expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens());
134+ "Query cannot be satisfied!", expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound());
135 }
136
137 double BestFirstReachabilitySearch::priority(const Structures::State *state,
138
139=== modified file 'PetriEngine/Reachability/BreadthFirstReachabilitySearch.cpp'
140--- PetriEngine/Reachability/BreadthFirstReachabilitySearch.cpp 2014-03-10 22:27:51 +0000
141+++ PetriEngine/Reachability/BreadthFirstReachabilitySearch.cpp 2014-03-16 21:01:52 +0000
142@@ -57,7 +57,7 @@
143
144 if(query->evaluate(*s0, &net)){
145 return ReachabilityResult(ReachabilityResult::Satisfied, "Query was satisfied",
146- expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens(), s0->pathLength(), s0->trace());
147+ expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound(), s0->pathLength(), s0->trace());
148 }
149
150 State* ns = allocator.createState();
151@@ -89,7 +89,7 @@
152 if(query->evaluate(*ns, &net)){
153 //ns->dumpTrace(net);
154 return ReachabilityResult(ReachabilityResult::Satisfied,
155- "A state satisfying the query was found", expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens(), ns->pathLength(), ns->trace());
156+ "A state satisfying the query was found", expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound(), ns->pathLength(), ns->trace());
157 }
158
159 queue.push_back(ns);
160@@ -97,7 +97,7 @@
161 if(!ns)
162 return ReachabilityResult(ReachabilityResult::Unknown,
163 "Memory bound exceeded",
164- expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens());
165+ expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound());
166 }
167 }
168 }
169@@ -105,7 +105,7 @@
170 }
171
172 return ReachabilityResult(ReachabilityResult::NotSatisfied,
173- "No state satisfying the query exists.", expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens());
174+ "No state satisfying the query exists.", expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound());
175 }
176
177 }}
178
179=== modified file 'PetriEngine/Reachability/DepthFirstReachabilitySearch.cpp'
180--- PetriEngine/Reachability/DepthFirstReachabilitySearch.cpp 2014-03-10 22:27:51 +0000
181+++ PetriEngine/Reachability/DepthFirstReachabilitySearch.cpp 2014-03-16 21:01:52 +0000
182@@ -60,7 +60,7 @@
183
184 if(query->evaluate(*s0, &net)){
185 return ReachabilityResult(ReachabilityResult::Satisfied, "Query was satisfied",
186- expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens(), s0->pathLength(), s0->trace());
187+ expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound(), s0->pathLength(), s0->trace());
188 }
189
190 State* ns = allocator.createState();
191@@ -95,7 +95,7 @@
192 if(query->evaluate(PQL::EvaluationContext(ns->marking(), ns->valuation(), &net)))
193 return ReachabilityResult(ReachabilityResult::Satisfied,
194 "A state satisfying the query was found", expandedStates, exploredStates,
195- states.discovered(), enabledTransitionsCount, states.maxTokens(), ns->pathLength(), ns->trace());
196+ states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound(), ns->pathLength(), ns->trace());
197 stack.back().t = t + 1;
198 stack.push_back(Step(ns, 0));
199 exploredStates++;
200@@ -104,7 +104,7 @@
201 if(!ns)
202 return ReachabilityResult(ReachabilityResult::Unknown,
203 "Memory bound exceeded",
204- expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens());
205+ expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound());
206 break;
207 }
208 }
209@@ -115,7 +115,7 @@
210 }
211 }
212 return ReachabilityResult(ReachabilityResult::NotSatisfied,
213- "No state satisfying the query exists.", expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens());
214+ "No state satisfying the query exists.", expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound());
215 }
216
217 } // Reachability
218
219=== modified file 'PetriEngine/Reachability/HashUnderApproximation.cpp'
220--- PetriEngine/Reachability/HashUnderApproximation.cpp 2014-03-10 20:08:13 +0000
221+++ PetriEngine/Reachability/HashUnderApproximation.cpp 2014-03-16 21:01:52 +0000
222@@ -90,7 +90,7 @@
223 ns->setTransition(t);
224 if(query->evaluate(PQL::EvaluationContext(ns->marking(), ns->valuation(), &net)))
225 return ReachabilityResult(ReachabilityResult::Satisfied,
226- "A state satisfying the query was found", expanded, explored, discovered, enabledTransitionsCount, -1, ns->pathLength(), ns->trace());
227+ "A state satisfying the query was found", expanded, explored, discovered, enabledTransitionsCount, -1, std::vector<unsigned int>(), ns->pathLength(), ns->trace());
228 stack.back().t = t + 1;
229 stack.push_back(Step(ns, 0));
230 foundSomething = true;
231@@ -104,7 +104,7 @@
232 }
233 }
234 return ReachabilityResult(ReachabilityResult::Unknown,
235- "Could not disprove the existence of a state not satisfying the query.", expanded, explored, discovered, enabledTransitionsCount, -1);
236+ "Could not disprove the existence of a state not satisfying the query.", expanded, explored, discovered, enabledTransitionsCount, -1, std::vector<unsigned int>());
237 }
238
239 }}
240
241=== modified file 'PetriEngine/Reachability/HeuristicDFS.cpp'
242--- PetriEngine/Reachability/HeuristicDFS.cpp 2014-03-10 22:27:51 +0000
243+++ PetriEngine/Reachability/HeuristicDFS.cpp 2014-03-16 21:01:52 +0000
244@@ -89,7 +89,7 @@
245 if(query->evaluate(*ns, &net))
246 return ReachabilityResult(ReachabilityResult::Satisfied,
247 "A state satisfying the query was found", expandedStates, exploredStates,
248- states.discovered(), enabledTransitionsCount, states.maxTokens(), ns->pathLength(), ns->trace());
249+ states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound(), ns->pathLength(), ns->trace());
250 PQL::DistanceContext context(net,
251 _distanceStrategy,
252 ns->marking(),
253@@ -122,7 +122,7 @@
254 }
255
256 return ReachabilityResult(ReachabilityResult::NotSatisfied,
257- "No state satisfying the query exists.", expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens());
258+ "No state satisfying the query exists.", expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound());
259 }
260
261 } // Reachability
262
263=== modified file 'PetriEngine/Reachability/MagicSearch.cpp'
264--- PetriEngine/Reachability/MagicSearch.cpp 2014-03-10 22:27:51 +0000
265+++ PetriEngine/Reachability/MagicSearch.cpp 2014-03-16 21:01:52 +0000
266@@ -129,6 +129,7 @@
267 states.discovered(),
268 enabledTransitionsCount,
269 -1,
270+ std::vector<unsigned int>(),
271 storeState->pathLength(),
272 storeState->trace());
273 }
274@@ -162,7 +163,8 @@
275 explored,
276 states.discovered(),
277 enabledTransitionsCount,
278- -1);
279+ -1,
280+ std::vector<unsigned int>());
281 }
282
283 double MagicSearch::priority(const MarkVal *marking,
284
285=== modified file 'PetriEngine/Reachability/RandomDFS.cpp'
286--- PetriEngine/Reachability/RandomDFS.cpp 2014-03-10 22:27:51 +0000
287+++ PetriEngine/Reachability/RandomDFS.cpp 2014-03-16 21:01:52 +0000
288@@ -65,7 +65,7 @@
289
290 if(query->evaluate(*s0, &net)){
291 return ReachabilityResult(ReachabilityResult::Satisfied, "Query was satisfied",
292- expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens(), s0->pathLength(), s0->trace());
293+ expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound(), s0->pathLength(), s0->trace());
294 }
295
296 State* s = s0;
297@@ -109,13 +109,13 @@
298 if(query && query->evaluate(*ns, &net))
299 return ReachabilityResult(ReachabilityResult::Satisfied,
300 "A state satisfying the query was found", expandedStates, exploredStates,
301- states.discovered(), enabledTransitionsCount, states.maxTokens(), ns->pathLength(), ns->trace());
302+ states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound(), ns->pathLength(), ns->trace());
303 succ[t] = ns;
304 ns = allocator.createState();
305 if(!ns)
306 return ReachabilityResult(ReachabilityResult::Unknown,
307 "Memory bound exceeded",
308- expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens());
309+ expandedStates, exploredStates, states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound());
310 }
311 }
312 }
313@@ -150,7 +150,7 @@
314
315 return ReachabilityResult(ReachabilityResult::NotSatisfied,
316 "No state satisfying the query exists.", expandedStates, exploredStates,
317- states.discovered(), enabledTransitionsCount, states.maxTokens());
318+ states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound());
319 }
320
321 }} // Namespaces
322
323=== modified file 'PetriEngine/Reachability/ReachabilityResult.h'
324--- PetriEngine/Reachability/ReachabilityResult.h 2014-03-10 20:08:13 +0000
325+++ PetriEngine/Reachability/ReachabilityResult.h 2014-03-16 21:01:52 +0000
326@@ -47,6 +47,7 @@
327 BigInt discoveredStates = 0,
328 const std::vector<BigInt> enabledTransitionsCount = std::vector<BigInt>(),
329 int maxTokens = 0,
330+ const std::vector<unsigned int> maxPlaceBound = std::vector<unsigned int>(),
331 int pathLength = 0,
332 const std::vector<unsigned int>& trace = std::vector<unsigned int>()){
333 _result = result;
334@@ -55,6 +56,7 @@
335 _exploredStates = exploredStates;
336 _discoveredStates = discoveredStates;
337 _enabledTransitionsCount = enabledTransitionsCount;
338+ _maxPlaceBound = maxPlaceBound;
339 _pathLength = pathLength;
340 _trace = trace;
341 _maxTokens = maxTokens;
342@@ -75,6 +77,8 @@
343 BigInt discoveredStates() const { return _discoveredStates; }
344 /** Gets the number of times each transition was enabled during the search*/
345 const std::vector<BigInt> enabledTransitionsCount() const { return _enabledTransitionsCount; }
346+ /** Gets the maximum number of tokens in each place of the net during the search*/
347+ const std::vector<unsigned int> maxPlaceBound() const { return _maxPlaceBound; }
348 /** Gets the length of the trace path. */
349 int pathLength() const { return _pathLength; }
350 /** Get trace, empty if no trace available or not provided by strategy */
351@@ -88,6 +92,7 @@
352 BigInt _exploredStates;
353 BigInt _discoveredStates;
354 std::vector<BigInt> _enabledTransitionsCount;
355+ std::vector<unsigned int> _maxPlaceBound;
356 int _pathLength;
357 std::vector<unsigned int> _trace;
358 int _maxTokens;
359
360=== modified file 'PetriEngine/Reachability/StateSearch.cpp'
361--- PetriEngine/Reachability/StateSearch.cpp 2014-03-10 22:27:51 +0000
362+++ PetriEngine/Reachability/StateSearch.cpp 2014-03-16 21:01:52 +0000
363@@ -120,7 +120,7 @@
364 if (query->evaluate(*ns, &net)) {
365 return ReachabilityResult(ReachabilityResult::Satisfied,
366 "Query was satisfied",
367- expanded, explored, states.discovered(), enabledTransitionsCount, states.maxTokens(), ns->pathLength(), ns->trace());
368+ expanded, explored, states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound(), ns->pathLength(), ns->trace());
369 }
370
371 bool isImpossible = true;
372@@ -143,7 +143,7 @@
373 if (!ns)
374 return ReachabilityResult(ReachabilityResult::Unknown,
375 "Memory bound exceeded",
376- expanded, explored, states.discovered(), enabledTransitionsCount, states.maxTokens());
377+ expanded, explored, states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound());
378 }
379 }
380 }
381@@ -151,7 +151,7 @@
382
383 return ReachabilityResult(ReachabilityResult::NotSatisfied,
384 "Query cannot be satisfied",
385- expanded, explored, states.discovered(), enabledTransitionsCount, states.maxTokens());
386+ expanded, explored, states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound());
387 }
388
389 } // Reachability
390
391=== modified file 'PetriEngine/Reachability/UltimateSearch.cpp'
392--- PetriEngine/Reachability/UltimateSearch.cpp 2014-03-10 22:27:51 +0000
393+++ PetriEngine/Reachability/UltimateSearch.cpp 2014-03-16 21:01:52 +0000
394@@ -67,7 +67,7 @@
395
396 if (query->evaluate(s0, &net)) {
397 return ReachabilityResult(ReachabilityResult::Satisfied, "Query was satisfied",
398- expanded, explored, states.discovered(), enabledTransitionsCount, states.maxTokens(), s0.pathLength(), s0.trace());
399+ expanded, explored, states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound(), s0.pathLength(), s0.trace());
400 }
401
402 // Main-loop
403@@ -100,7 +100,7 @@
404 if (query->evaluate(*ns, &net)) {
405 return ReachabilityResult(ReachabilityResult::Satisfied,
406 "Query was satisfied",
407- expanded, explored, states.discovered(), enabledTransitionsCount, states.maxTokens(), ns->pathLength(), ns->trace());
408+ expanded, explored, states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound(), ns->pathLength(), ns->trace());
409 }
410
411 // Push new state on the queue
412@@ -116,7 +116,7 @@
413 if (!ns)
414 return ReachabilityResult(ReachabilityResult::Unknown,
415 "Memory bound exceeded",
416- expanded, explored, states.discovered(), enabledTransitionsCount, states.maxTokens());
417+ expanded, explored, states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound());
418 }
419 }
420 }
421@@ -125,7 +125,7 @@
422
423 return ReachabilityResult(ReachabilityResult::NotSatisfied,
424 "Query cannot be satisfied",
425- expanded, explored, states.discovered(), enabledTransitionsCount, states.maxTokens());
426+ expanded, explored, states.discovered(), enabledTransitionsCount, states.maxTokens(), states.maxPlaceBound());
427 }
428
429 } // Reachability
430
431=== modified file 'PetriEngine/Reducer.cpp'
432--- PetriEngine/Reducer.cpp 2014-03-04 22:51:34 +0000
433+++ PetriEngine/Reducer.cpp 2014-03-16 21:01:52 +0000
434@@ -160,12 +160,14 @@
435 _removedTransitions++;
436 if (m0[pPre] == 0) { // removing pPre
437 _removedPlaces++;
438+ net->skipPlace(pPre);
439 for (size_t _t = 0; _t < net->numberOfTransitions(); _t++) {
440 net->updateoutArc(_t, pPost, net->outArc(_t, pPost) + net->outArc(_t, pPre));
441 net->updateoutArc(_t, pPre, 0);
442 }
443 } else if (m0[pPost] == 0) { // removing pPost
444 _removedPlaces++;
445+ net->skipPlace(pPost);
446 for (size_t _t = 0; _t < net->numberOfTransitions(); _t++) {
447 net->updateinArc(pPre, _t, net->inArc(pPost, _t));
448 net->updateoutArc(_t, pPre, net->outArc(_t, pPre) + net->outArc(_t, pPost));
449@@ -239,6 +241,7 @@
450 net->updateoutArc(tPre, p, 0);
451 net->updateinArc(p, tPost, 0);
452 _removedPlaces++;
453+ net->skipPlace(p);
454 _removedTransitions++;
455 for (size_t _p = 0; _p < net->numberOfPlaces(); _p++) { // remove tPost
456 net->updateoutArc(tPre, _p, net->outArc(tPre, _p) + net->outArc(tPost, _p));
457@@ -317,6 +320,7 @@
458 net->updateinArc(p1, t2, 0);
459 removePlace[p1] = false;
460 _removedPlaces++;
461+ net->skipPlace(p1);
462 }
463 }
464 return continueReductions;
465
466=== modified file 'PetriEngine/Structures/StateSet.h'
467--- PetriEngine/Structures/StateSet.h 2013-07-24 10:43:08 +0000
468+++ PetriEngine/Structures/StateSet.h 2014-03-16 21:01:52 +0000
469@@ -39,6 +39,7 @@
470 _maxTokens = 0;
471 _places = net.numberOfPlaces();
472 _variables = net.numberOfVariables();
473+ _maxPlaceBound = std::vector<unsigned int>(_places,0);
474 }
475 StateSet(unsigned int places, unsigned int variables, int kbound = 0)
476 : std::tr1::unordered_set<State*, State::hash, State::equal_to>
477@@ -49,7 +50,8 @@
478 _maxTokens = 0;
479 _places = places;
480 _variables = variables;
481- }
482+ _maxPlaceBound = std::vector<unsigned int>(_places,0);
483+ }
484 bool add(State* state) {
485 _discovered++;
486
487@@ -66,6 +68,12 @@
488 return false;
489
490 std::pair<iter, bool> result = this->insert(state);
491+ // update the max token bound for each place in the net (only for newly discovered markings)
492+ if (result.second) {
493+ for(size_t i = 0; i < _places; i++) {
494+ _maxPlaceBound[i] = std::max<unsigned int>(state->marking()[i],_maxPlaceBound[i]);
495+ }
496+ }
497 return result.second;
498 }
499 bool contains(State* state) {
500@@ -78,12 +86,18 @@
501 int maxTokens() const {
502 return _maxTokens;
503 }
504+
505+ std::vector<unsigned int> maxPlaceBound() const {
506+ return _maxPlaceBound;
507+ }
508+
509 private:
510 typedef std::tr1::unordered_set<State*, State::hash, State::equal_to>::const_iterator const_iter;
511 typedef std::tr1::unordered_set<State*, State::hash, State::equal_to>::iterator iter;
512 BigInt _discovered;
513 int _kbound;
514 int _maxTokens;
515+ std::vector<unsigned int> _maxPlaceBound;
516 unsigned int _places;
517 unsigned int _variables;
518 };
519
520=== modified file 'VerifyPN.cpp'
521--- VerifyPN.cpp 2014-03-11 20:42:22 +0000
522+++ VerifyPN.cpp 2014-03-16 21:01:52 +0000
523@@ -403,7 +403,17 @@
524 fprintf(stdout,"<%s:%lli> ", tnames[t].c_str(), result.enabledTransitionsCount()[t]);
525 }
526 }
527+ fprintf(stdout,"\n\nPLACE-BOUND STATISTICS\n");
528+ for(size_t p = 0; p < result.maxPlaceBound().size(); p++) {
529+ // report maximum bounds for each place (? means that the place was removed in net reduction)
530+ if (net->isPlaceSkipped(p)) {
531+ fprintf(stdout,"<%s;?> ", pnames[p].c_str());
532+ } else {
533+ fprintf(stdout,"<%s;%i> ", pnames[p].c_str(), result.maxPlaceBound()[p]);
534+ }
535+ }
536 fprintf(stdout,"\n\n");
537+
538 //----------------------- Output Result -----------------------//
539
540 ReturnValues retval = ErrorCode;

Subscribers

People subscribed via source and target branches