Merge lp:~peter-gjoel/verifydtapn/PTrieWorkflow into lp:verifydtapn
- PTrieWorkflow
- Merge into trunk
Status: | Merged |
---|---|
Approved by: | Jiri Srba |
Approved revision: | 364 |
Merged at revision: | 333 |
Proposed branch: | lp:~peter-gjoel/verifydtapn/PTrieWorkflow |
Merge into: | lp:verifydtapn |
Prerequisite: | lp:~peter-gjoel/verifydtapn/WorkflowRefactor |
Diff against target: |
1810 lines (+1104/-120) 15 files modified
makefile.linux64 (+2/-2) src/DiscreteVerification/DataStructures/CoveredMarkingVisitor.cpp (+190/-0) src/DiscreteVerification/DataStructures/CoveredMarkingVisitor.h (+57/-0) src/DiscreteVerification/DataStructures/MarkingEncoder.h (+31/-9) src/DiscreteVerification/DataStructures/NonStrictMarking.hpp (+12/-0) src/DiscreteVerification/DataStructures/WorkflowPWList.cpp (+130/-10) src/DiscreteVerification/DataStructures/WorkflowPWList.hpp (+23/-0) src/DiscreteVerification/DataStructures/binarywrapper.h (+168/-56) src/DiscreteVerification/DataStructures/ptrie.h (+158/-12) src/DiscreteVerification/DataStructures/visitor.h (+30/-0) src/DiscreteVerification/DiscreteVerification.cpp (+44/-23) src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp (+109/-4) src/DiscreteVerification/VerificationTypes/WorkflowSoundness.hpp (+18/-0) src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.cpp (+112/-4) src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.hpp (+20/-0) |
To merge this branch: | bzr merge lp:~peter-gjoel/verifydtapn/PTrieWorkflow |
Related bugs: |
Reviewer | Review Type | Date Requested | Status |
---|---|---|---|
Jiri Srba | Approve | ||
Jakob Taankvist | Pending | ||
Mathias Grund Sørensen | Pending | ||
Review via email: mp+262676@code.launchpad.net |
Commit message
Description of the change
Implementation of ptries for workflow verification.
- 358. By Peter Gjøl Jensen
-
merged with trunk
Peter Gjøl Jensen (peter-gjoel) wrote : | # |
Fixed.
Jiri Srba (srba) wrote : | # |
Thanks. I am still getting some warnings:
In file included from src/DiscreteVer
src/DiscreteVer
is uninitialized when used within its own initialization [-Wuninitialized]
src/DiscreteVer
instantiation of member function
'
requested here
In file included from src/DiscreteVer
src/DiscreteVer
private field 'last' is not used [-Wunused-
2 warnings generated.
- 359. By Peter Gjøl Jensen
-
fixed warnings
- 360. By Peter Gjøl Jensen
-
fixed covered marking visitor
- 361. By Peter Gjøl Jensen
-
readded limit on cover-check
- 362. By Peter Gjøl Jensen
-
fixed problem with ptries and unbounded markings
- 363. By Peter Gjøl Jensen
-
merged with trunk
- 364. By Peter Gjøl Jensen
-
changed comparison function for ptries, simplifying code and giving a speedup on VERY large markings
Peter Gjøl Jensen (peter-gjoel) wrote : | # |
Minor re-factoring, improving on code-quality and possibly giving speedup on very large markings (several hundreds of tokens).
Jiri Srba (srba) wrote : | # |
Extensively tested and it works flawlessly on all my examples.
Preview Diff
1 | === modified file 'makefile.linux64' | |||
2 | --- makefile.linux64 2015-06-17 10:05:28 +0000 | |||
3 | +++ makefile.linux64 2015-08-20 13:27:24 +0000 | |||
4 | @@ -8,9 +8,9 @@ | |||
5 | 8 | CUT = cut | 8 | CUT = cut |
6 | 9 | 9 | ||
7 | 10 | # Compiler and linker flags | 10 | # Compiler and linker flags |
9 | 11 | CFLAGS = -fpermissive -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -static -O3 -Wall -mtune=core2 | 11 | CFLAGS = -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -static -O3 -Wall -mtune=core2 |
10 | 12 | 12 | ||
12 | 13 | LDFLAGS = -fpermissive -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -static -O3 -Wall -mtune=core2 | 13 | LDFLAGS = -DBOOST_DISABLE_THREADS -DNDEBUG -DDISABLE_ASSERTX -static -O3 -Wall -mtune=core2 |
13 | 14 | 14 | ||
14 | 15 | # Input files | 15 | # Input files |
15 | 16 | SOURCES = $(shell find * -name "*.cpp") | 16 | SOURCES = $(shell find * -name "*.cpp") |
16 | 17 | 17 | ||
17 | === added file 'src/DiscreteVerification/DataStructures/CoveredMarkingVisitor.cpp' | |||
18 | --- src/DiscreteVerification/DataStructures/CoveredMarkingVisitor.cpp 1970-01-01 00:00:00 +0000 | |||
19 | +++ src/DiscreteVerification/DataStructures/CoveredMarkingVisitor.cpp 2015-08-20 13:27:24 +0000 | |||
20 | @@ -0,0 +1,190 @@ | |||
21 | 1 | /* | ||
22 | 2 | * File: CoveredMarkingVisitor.cpp | ||
23 | 3 | * Author: Peter G. Jensen | ||
24 | 4 | * | ||
25 | 5 | * Created on 18 June 2015, 14:23 | ||
26 | 6 | */ | ||
27 | 7 | |||
28 | 8 | #include "CoveredMarkingVisitor.h" | ||
29 | 9 | |||
30 | 10 | |||
31 | 11 | using namespace ptrie; | ||
32 | 12 | namespace VerifyTAPN { | ||
33 | 13 | namespace DiscreteVerification { | ||
34 | 14 | |||
35 | 15 | CoveredMarkingVisitor::CoveredMarkingVisitor( | ||
36 | 16 | MarkingEncoder<MetaData*, NonStrictMarking>& enc) | ||
37 | 17 | : encoder(enc), scratchpad(0) | ||
38 | 18 | { | ||
39 | 19 | |||
40 | 20 | } | ||
41 | 21 | |||
42 | 22 | |||
43 | 23 | CoveredMarkingVisitor::~CoveredMarkingVisitor() | ||
44 | 24 | { | ||
45 | 25 | scratchpad.release(); | ||
46 | 26 | } | ||
47 | 27 | |||
48 | 28 | void CoveredMarkingVisitor::set_target(NonStrictMarking* m, ptriepointer_t<MetaData*> me) | ||
49 | 29 | { | ||
50 | 30 | target = m; | ||
51 | 31 | _found=false; | ||
52 | 32 | _targetencoding = me; | ||
53 | 33 | |||
54 | 34 | if(encoder.scratchpad.size() > scratchpad.size()) | ||
55 | 35 | { | ||
56 | 36 | scratchpad.release(); | ||
57 | 37 | scratchpad = encoder.scratchpad.clone(); | ||
58 | 38 | } | ||
59 | 39 | } | ||
60 | 40 | |||
61 | 41 | bool CoveredMarkingVisitor::set(int index, bool value) | ||
62 | 42 | { | ||
63 | 43 | if(_found) return true; // end | ||
64 | 44 | scratchpad.set(index, value); | ||
65 | 45 | // If we have enough bits to constitute a single token (with placement) | ||
66 | 46 | if((index + 1) % encoder.offsetBitSize == 0 && index > 0) | ||
67 | 47 | { | ||
68 | 48 | size_t begin = (index / encoder.offsetBitSize) * encoder.offsetBitSize; | ||
69 | 49 | unsigned long long data = 0; | ||
70 | 50 | uint count = 0; | ||
71 | 51 | uint cbit = index; | ||
72 | 52 | |||
73 | 53 | while (cbit >= begin + encoder.countBitSize) { | ||
74 | 54 | data = data << 1; | ||
75 | 55 | if(scratchpad.at(cbit)) | ||
76 | 56 | { | ||
77 | 57 | data |= 1; | ||
78 | 58 | } | ||
79 | 59 | --cbit; | ||
80 | 60 | } | ||
81 | 61 | |||
82 | 62 | while(cbit >= begin) | ||
83 | 63 | { | ||
84 | 64 | count = count << 1; | ||
85 | 65 | if(scratchpad.at(cbit)) | ||
86 | 66 | { | ||
87 | 67 | count |= 1; | ||
88 | 68 | } | ||
89 | 69 | if(cbit == 0) break; | ||
90 | 70 | cbit--; | ||
91 | 71 | } | ||
92 | 72 | |||
93 | 73 | if (count) { | ||
94 | 74 | return !target_contains_token(data, count); | ||
95 | 75 | } | ||
96 | 76 | // should not really happen | ||
97 | 77 | assert(false); | ||
98 | 78 | return true; // skip if happens! | ||
99 | 79 | } | ||
100 | 80 | else | ||
101 | 81 | { | ||
102 | 82 | return false; // not enough info | ||
103 | 83 | } | ||
104 | 84 | } | ||
105 | 85 | |||
106 | 86 | bool CoveredMarkingVisitor::set_remainder(int index, | ||
107 | 87 | ptriepointer_t<MetaData*> pointer) | ||
108 | 88 | { | ||
109 | 89 | // special case, marking cannot cover itself | ||
110 | 90 | if(pointer.index == _targetencoding.index) return false; | ||
111 | 91 | if(_found) return true; // end | ||
112 | 92 | |||
113 | 93 | encoding_t remainder = pointer.remainder(); | ||
114 | 94 | uint offset = index - (index % 8); // offset matches on a byte | ||
115 | 95 | uint begin = (index / encoder.offsetBitSize ) * encoder.offsetBitSize; // start from whole token | ||
116 | 96 | // check inclusion | ||
117 | 97 | |||
118 | 98 | bool bit; | ||
119 | 99 | |||
120 | 100 | while(true) | ||
121 | 101 | { | ||
122 | 102 | uint cbit = begin; | ||
123 | 103 | unsigned long long data = 0; | ||
124 | 104 | uint count = 0; | ||
125 | 105 | cbit += encoder.offsetBitSize - 1; | ||
126 | 106 | // unpack place/age/count | ||
127 | 107 | while (cbit >= begin + encoder.countBitSize) { | ||
128 | 108 | data = data << 1; | ||
129 | 109 | |||
130 | 110 | if(cbit < offset) bit = scratchpad.at(cbit); | ||
131 | 111 | else bit = remainder.at(cbit - offset); | ||
132 | 112 | |||
133 | 113 | if(bit) | ||
134 | 114 | { | ||
135 | 115 | data |= 1; | ||
136 | 116 | } | ||
137 | 117 | --cbit; | ||
138 | 118 | } | ||
139 | 119 | |||
140 | 120 | while(cbit >= begin) | ||
141 | 121 | { | ||
142 | 122 | count = count << 1; | ||
143 | 123 | |||
144 | 124 | if(cbit < offset) bit = scratchpad.at(cbit); | ||
145 | 125 | else bit = remainder.at(cbit - offset); | ||
146 | 126 | |||
147 | 127 | if(bit) | ||
148 | 128 | { | ||
149 | 129 | count |= 1; | ||
150 | 130 | } | ||
151 | 131 | if(cbit == 0) break; | ||
152 | 132 | cbit--; | ||
153 | 133 | } | ||
154 | 134 | begin += encoder.offsetBitSize; | ||
155 | 135 | if (count) | ||
156 | 136 | { | ||
157 | 137 | if(!target_contains_token(data, count)) | ||
158 | 138 | { | ||
159 | 139 | return false; | ||
160 | 140 | } | ||
161 | 141 | } | ||
162 | 142 | else | ||
163 | 143 | { | ||
164 | 144 | break; | ||
165 | 145 | } | ||
166 | 146 | } | ||
167 | 147 | |||
168 | 148 | match = pointer; | ||
169 | 149 | _found = true; | ||
170 | 150 | return true; | ||
171 | 151 | } | ||
172 | 152 | |||
173 | 153 | bool CoveredMarkingVisitor::back(int index) | ||
174 | 154 | { | ||
175 | 155 | return false; | ||
176 | 156 | } | ||
177 | 157 | |||
178 | 158 | bool CoveredMarkingVisitor::target_contains_token(unsigned long long placeage, uint count) | ||
179 | 159 | { | ||
180 | 160 | if(count == 0) return true; | ||
181 | 161 | |||
182 | 162 | int age = floor(placeage / encoder.numberOfPlaces); | ||
183 | 163 | int place = (placeage % encoder.numberOfPlaces); | ||
184 | 164 | int cnt = count; | ||
185 | 165 | const TokenList& tokens = target->getTokenList(place); | ||
186 | 166 | |||
187 | 167 | |||
188 | 168 | for( TokenList::const_iterator it = tokens.begin(); | ||
189 | 169 | it != tokens.end(); ++it) | ||
190 | 170 | { | ||
191 | 171 | if(it->getAge() == age) | ||
192 | 172 | { | ||
193 | 173 | if(it->getCount() >= cnt) return true; // continue | ||
194 | 174 | else return false; // skip branch | ||
195 | 175 | } | ||
196 | 176 | else if(it->getAge() > age) return false; // skip branch | ||
197 | 177 | } | ||
198 | 178 | |||
199 | 179 | return false; // skip branch | ||
200 | 180 | } | ||
201 | 181 | |||
202 | 182 | NonStrictMarking* CoveredMarkingVisitor::decode() | ||
203 | 183 | { | ||
204 | 184 | NonStrictMarking* m = encoder.decode(match); | ||
205 | 185 | m->meta = match.get_meta(); | ||
206 | 186 | return m; | ||
207 | 187 | } | ||
208 | 188 | |||
209 | 189 | } | ||
210 | 190 | } | ||
211 | 0 | \ No newline at end of file | 191 | \ No newline at end of file |
212 | 1 | 192 | ||
213 | === added file 'src/DiscreteVerification/DataStructures/CoveredMarkingVisitor.h' | |||
214 | --- src/DiscreteVerification/DataStructures/CoveredMarkingVisitor.h 1970-01-01 00:00:00 +0000 | |||
215 | +++ src/DiscreteVerification/DataStructures/CoveredMarkingVisitor.h 2015-08-20 13:27:24 +0000 | |||
216 | @@ -0,0 +1,57 @@ | |||
217 | 1 | /* | ||
218 | 2 | * File: CoveredMarkingVisitor.h | ||
219 | 3 | * Author: Peter G. Jensen | ||
220 | 4 | * | ||
221 | 5 | * Created on 17 June 2015, 00:04 | ||
222 | 6 | */ | ||
223 | 7 | |||
224 | 8 | #ifndef COVEREDMARKINGVISITOR_H | ||
225 | 9 | #define COVEREDMARKINGVISITOR_H | ||
226 | 10 | |||
227 | 11 | #include "binarywrapper.h" | ||
228 | 12 | #include <limits> | ||
229 | 13 | #include <vector> | ||
230 | 14 | #include "ptrie.h" | ||
231 | 15 | #include "visitor.h" | ||
232 | 16 | #include "MarkingEncoder.h" | ||
233 | 17 | #include "NonStrictMarkingBase.hpp" | ||
234 | 18 | #include "NonStrictMarking.hpp" | ||
235 | 19 | |||
236 | 20 | |||
237 | 21 | using namespace ptrie; | ||
238 | 22 | namespace VerifyTAPN { | ||
239 | 23 | namespace DiscreteVerification { | ||
240 | 24 | |||
241 | 25 | class CoveredMarkingVisitor | ||
242 | 26 | : public visitor_t<MetaData*> | ||
243 | 27 | { | ||
244 | 28 | typedef binarywrapper_t<MetaData*> encoding_t; | ||
245 | 29 | private: | ||
246 | 30 | MarkingEncoder<MetaData*, NonStrictMarking>& encoder; | ||
247 | 31 | NonStrictMarking* target; | ||
248 | 32 | encoding_t scratchpad; | ||
249 | 33 | ptriepointer_t<MetaData*> match; | ||
250 | 34 | bool _found; | ||
251 | 35 | ptriepointer_t<MetaData*> _targetencoding; | ||
252 | 36 | |||
253 | 37 | private: | ||
254 | 38 | bool target_contains_token(unsigned long long placeage, uint count); | ||
255 | 39 | |||
256 | 40 | public: | ||
257 | 41 | CoveredMarkingVisitor( | ||
258 | 42 | MarkingEncoder<MetaData*, NonStrictMarking>& enc); | ||
259 | 43 | ~CoveredMarkingVisitor(); | ||
260 | 44 | virtual bool back(int index); | ||
261 | 45 | virtual bool set(int index, bool value); | ||
262 | 46 | virtual bool set_remainder(int index, | ||
263 | 47 | ptriepointer_t<MetaData*> pointer); | ||
264 | 48 | void set_target(NonStrictMarking* m, ptriepointer_t<MetaData*> me); | ||
265 | 49 | NonStrictMarking* decode(); | ||
266 | 50 | bool found(){return _found;} | ||
267 | 51 | }; | ||
268 | 52 | |||
269 | 53 | } | ||
270 | 54 | } | ||
271 | 55 | |||
272 | 56 | #endif /* BINARYMARKINGVISITOR_H */ | ||
273 | 57 | |||
274 | 0 | 58 | ||
275 | === modified file 'src/DiscreteVerification/DataStructures/MarkingEncoder.h' | |||
276 | --- src/DiscreteVerification/DataStructures/MarkingEncoder.h 2015-06-22 21:03:26 +0000 | |||
277 | +++ src/DiscreteVerification/DataStructures/MarkingEncoder.h 2015-08-20 13:27:24 +0000 | |||
278 | @@ -20,9 +20,12 @@ | |||
279 | 20 | namespace VerifyTAPN { | 20 | namespace VerifyTAPN { |
280 | 21 | namespace DiscreteVerification { | 21 | namespace DiscreteVerification { |
281 | 22 | 22 | ||
282 | 23 | class CoveredMarkingVisitor; | ||
283 | 24 | |||
284 | 23 | template<typename T, typename M = NonStrictMarkingBase> | 25 | template<typename T, typename M = NonStrictMarkingBase> |
285 | 24 | class MarkingEncoder | 26 | class MarkingEncoder |
286 | 25 | { | 27 | { |
287 | 28 | friend class CoveredMarkingVisitor; | ||
288 | 26 | typedef binarywrapper_t<T> encoding_t; | 29 | typedef binarywrapper_t<T> encoding_t; |
289 | 27 | 30 | ||
290 | 28 | private: | 31 | private: |
291 | @@ -32,10 +35,9 @@ | |||
292 | 32 | const uint countBitSize; | 35 | const uint countBitSize; |
293 | 33 | const uint placeAgeBitSize; | 36 | const uint placeAgeBitSize; |
294 | 34 | const uint offsetBitSize; | 37 | const uint offsetBitSize; |
296 | 35 | uint markingBitSize; | 38 | const uint markingBitSize; |
297 | 36 | TAPN::TimedArcPetriNet& tapn; | 39 | TAPN::TimedArcPetriNet& tapn; |
298 | 37 | encoding_t scratchpad; | 40 | encoding_t scratchpad; |
299 | 38 | void* raw; | ||
300 | 39 | public: | 41 | public: |
301 | 40 | MarkingEncoder(TAPN::TimedArcPetriNet& tapn, int knumber, | 42 | MarkingEncoder(TAPN::TimedArcPetriNet& tapn, int knumber, |
302 | 41 | int nplaces, int mage); | 43 | int nplaces, int mage); |
303 | @@ -58,8 +60,7 @@ | |||
304 | 58 | markingBitSize(offsetBitSize * (knumber ? knumber : 1)), | 60 | markingBitSize(offsetBitSize * (knumber ? knumber : 1)), |
305 | 59 | tapn(tapn) | 61 | tapn(tapn) |
306 | 60 | { | 62 | { |
309 | 61 | scratchpad = encoding_t(markingBitSize); | 63 | scratchpad = encoding_t(0); |
308 | 62 | raw = (void*)scratchpad.raw(); | ||
310 | 63 | } | 64 | } |
311 | 64 | 65 | ||
312 | 65 | template<typename T, typename M> | 66 | template<typename T, typename M> |
313 | @@ -71,7 +72,10 @@ | |||
314 | 71 | template<typename T, typename M> | 72 | template<typename T, typename M> |
315 | 72 | M* MarkingEncoder<T, M>::decode(const ptriepointer_t<T>& pointer) | 73 | M* MarkingEncoder<T, M>::decode(const ptriepointer_t<T>& pointer) |
316 | 73 | { | 74 | { |
318 | 74 | assert(scratchpad.raw() == raw); | 75 | // we allready know here that the scratchpad is large enough, |
319 | 76 | // it is monotonically increased when we encode, ie; no marking | ||
320 | 77 | // taking up more bits are currently in the ptrie. | ||
321 | 78 | |||
322 | 75 | M* m = new M(); | 79 | M* m = new M(); |
323 | 76 | assert(pointer.container->consistent()); | 80 | assert(pointer.container->consistent()); |
324 | 77 | const encoding_t remainder = pointer.remainder(); | 81 | const encoding_t remainder = pointer.remainder(); |
325 | @@ -81,12 +85,13 @@ | |||
326 | 81 | 85 | ||
327 | 82 | uint cbit = 0; | 86 | uint cbit = 0; |
328 | 83 | // foreach token | 87 | // foreach token |
331 | 84 | uint data = 0; | 88 | |
330 | 85 | uint count = 0; | ||
332 | 86 | bool bit; | 89 | bool bit; |
333 | 87 | for (uint i = 0; i < maxNumberOfTokens; i++) { | 90 | for (uint i = 0; i < maxNumberOfTokens; i++) { |
334 | 88 | uint offset = offsetBitSize * i; | 91 | uint offset = offsetBitSize * i; |
335 | 89 | cbit = offset + offsetBitSize - 1; | 92 | cbit = offset + offsetBitSize - 1; |
336 | 93 | unsigned long long data = 0; | ||
337 | 94 | uint count = 0; | ||
338 | 90 | 95 | ||
339 | 91 | while (cbit >= offset + countBitSize) { | 96 | while (cbit >= offset + countBitSize) { |
340 | 92 | data = data << 1; | 97 | data = data << 1; |
341 | @@ -137,8 +142,6 @@ | |||
342 | 137 | uint place = (data % this->numberOfPlaces); | 142 | uint place = (data % this->numberOfPlaces); |
343 | 138 | Token t = Token(age, count); | 143 | Token t = Token(age, count); |
344 | 139 | m->addTokenInPlace(tapn.getPlace(place), t); | 144 | m->addTokenInPlace(tapn.getPlace(place), t); |
345 | 140 | data = 0; | ||
346 | 141 | count = 0; | ||
347 | 142 | } | 145 | } |
348 | 143 | else | 146 | else |
349 | 144 | { | 147 | { |
350 | @@ -157,6 +160,25 @@ | |||
351 | 157 | template<typename T, typename M> | 160 | template<typename T, typename M> |
352 | 158 | binarywrapper_t<T> MarkingEncoder<T, M>::encode(M* marking) | 161 | binarywrapper_t<T> MarkingEncoder<T, M>::encode(M* marking) |
353 | 159 | { | 162 | { |
354 | 163 | // make sure we have space to encode marking | ||
355 | 164 | size_t count = 0; | ||
356 | 165 | for (vector<Place>::const_iterator pi = marking->getPlaceList().begin(); | ||
357 | 166 | pi != marking->getPlaceList().end(); | ||
358 | 167 | pi++) { | ||
359 | 168 | count += pi->tokens.size(); | ||
360 | 169 | } | ||
361 | 170 | count *= offsetBitSize; | ||
362 | 171 | count /= 8; | ||
363 | 172 | count += 1; | ||
364 | 173 | |||
365 | 174 | if(scratchpad.size() < count) | ||
366 | 175 | { | ||
367 | 176 | scratchpad.release(); | ||
368 | 177 | scratchpad = encoding_t(count * 8); | ||
369 | 178 | } | ||
370 | 179 | |||
371 | 180 | |||
372 | 181 | |||
373 | 160 | scratchpad.zero(); | 182 | scratchpad.zero(); |
374 | 161 | int tc = 0; | 183 | int tc = 0; |
375 | 162 | uint bitcount = 0; | 184 | uint bitcount = 0; |
376 | 163 | 185 | ||
377 | === modified file 'src/DiscreteVerification/DataStructures/NonStrictMarking.hpp' | |||
378 | --- src/DiscreteVerification/DataStructures/NonStrictMarking.hpp 2015-06-22 21:03:26 +0000 | |||
379 | +++ src/DiscreteVerification/DataStructures/NonStrictMarking.hpp 2015-08-20 13:27:24 +0000 | |||
380 | @@ -48,6 +48,18 @@ | |||
381 | 48 | MetaDataWithTraceAndEncoding* parent; | 48 | MetaDataWithTraceAndEncoding* parent; |
382 | 49 | }; | 49 | }; |
383 | 50 | 50 | ||
384 | 51 | struct WorkflowSoundnessMetaDataWithEncoding : public MetaDataWithTraceAndEncoding { | ||
385 | 52 | public: | ||
386 | 53 | WorkflowSoundnessMetaDataWithEncoding() : MetaDataWithTraceAndEncoding(), parents() | ||
387 | 54 | { totalDelay = INT_MAX;}; | ||
388 | 55 | virtual ~WorkflowSoundnessMetaDataWithEncoding() | ||
389 | 56 | { | ||
390 | 57 | parents.clear(); | ||
391 | 58 | } | ||
392 | 59 | |||
393 | 60 | vector<MetaData*> parents; | ||
394 | 61 | }; | ||
395 | 62 | |||
396 | 51 | class NonStrictMarking : public NonStrictMarkingBase{ | 63 | class NonStrictMarking : public NonStrictMarkingBase{ |
397 | 52 | public: | 64 | public: |
398 | 53 | NonStrictMarking():NonStrictMarkingBase(), meta(NULL){} | 65 | NonStrictMarking():NonStrictMarkingBase(), meta(NULL){} |
399 | 54 | 66 | ||
400 | === modified file 'src/DiscreteVerification/DataStructures/WorkflowPWList.cpp' | |||
401 | --- src/DiscreteVerification/DataStructures/WorkflowPWList.cpp 2015-06-22 22:10:16 +0000 | |||
402 | +++ src/DiscreteVerification/DataStructures/WorkflowPWList.cpp 2015-08-20 13:27:24 +0000 | |||
403 | @@ -88,7 +88,8 @@ | |||
404 | 88 | } | 88 | } |
405 | 89 | 89 | ||
406 | 90 | bool isFirst = true; | 90 | bool isFirst = true; |
408 | 91 | for (vector<NonStrictMarking*>::iterator iter = coveredMarkings.begin(); iter != coveredMarkings.end(); ++iter) { | 91 | for (vector<NonStrictMarking*>::iterator iter = coveredMarkings.begin(); |
409 | 92 | iter != coveredMarkings.end(); ++iter) { | ||
410 | 92 | if (isFirst) { | 93 | if (isFirst) { |
411 | 93 | isFirst = false; | 94 | isFirst = false; |
412 | 94 | continue; | 95 | continue; |
413 | @@ -96,22 +97,15 @@ | |||
414 | 96 | NonStrictMarking* covered = lookup(*iter); | 97 | NonStrictMarking* covered = lookup(*iter); |
415 | 97 | if (covered != NULL) { | 98 | if (covered != NULL) { |
416 | 98 | // cleanup | 99 | // cleanup |
419 | 99 | for (vector<NonStrictMarking*>::iterator del = coveredMarkings.begin(); | 100 | for (;iter != coveredMarkings.end(); ++iter) |
418 | 100 | del != coveredMarkings.end(); ++del) | ||
420 | 101 | { | 101 | { |
422 | 102 | delete *del; | 102 | delete *iter; |
423 | 103 | } | 103 | } |
424 | 104 | return covered; | 104 | return covered; |
425 | 105 | } | 105 | } |
426 | 106 | delete *iter; | 106 | delete *iter; |
427 | 107 | } | 107 | } |
428 | 108 | 108 | ||
429 | 109 | // Cleanup | ||
430 | 110 | for (vector<NonStrictMarking*>::iterator del = coveredMarkings.begin(); | ||
431 | 111 | del != coveredMarkings.end(); ++del) | ||
432 | 112 | { | ||
433 | 113 | delete *del; | ||
434 | 114 | } | ||
435 | 115 | } | 109 | } |
436 | 116 | return NULL; | 110 | return NULL; |
437 | 117 | } | 111 | } |
438 | @@ -163,6 +157,132 @@ | |||
439 | 163 | } | 157 | } |
440 | 164 | 158 | ||
441 | 165 | 159 | ||
442 | 160 | WorkflowPWListHybrid::WorkflowPWListHybrid( | ||
443 | 161 | TAPN::TimedArcPetriNet& tapn, | ||
444 | 162 | WaitingList<ptriepointer_t<MetaData*> >* w_l, | ||
445 | 163 | int knumber, | ||
446 | 164 | int nplaces, | ||
447 | 165 | int mage) | ||
448 | 166 | : PWListHybrid(tapn, w_l, knumber, nplaces, mage, false, true), | ||
449 | 167 | visitor(encoder) | ||
450 | 168 | { | ||
451 | 169 | |||
452 | 170 | } | ||
453 | 171 | |||
454 | 172 | WorkflowPWListHybrid::~WorkflowPWListHybrid() | ||
455 | 173 | { | ||
456 | 174 | ptriepointer_t<MetaData*> begin = passed.begin(); | ||
457 | 175 | while(begin != passed.end()) | ||
458 | 176 | { | ||
459 | 177 | delete begin.get_meta(); | ||
460 | 178 | ++ begin; | ||
461 | 179 | } | ||
462 | 180 | } | ||
463 | 181 | |||
464 | 182 | NonStrictMarking* WorkflowPWListHybrid::getCoveredMarking | ||
465 | 183 | (NonStrictMarking* marking, bool useLinearSweep) | ||
466 | 184 | { | ||
467 | 185 | visitor.set_target(marking, last_pointer); | ||
468 | 186 | passed.visit(visitor); | ||
469 | 187 | if(visitor.found()) | ||
470 | 188 | { | ||
471 | 189 | NonStrictMarking* m = visitor.decode(); | ||
472 | 190 | return m; | ||
473 | 191 | } | ||
474 | 192 | else | ||
475 | 193 | { | ||
476 | 194 | return NULL; | ||
477 | 195 | } | ||
478 | 196 | } | ||
479 | 197 | |||
480 | 198 | NonStrictMarking* WorkflowPWListHybrid::getUnpassed() | ||
481 | 199 | { | ||
482 | 200 | ptriepointer_t<MetaData*> it = passed.last(); | ||
483 | 201 | for(; it != passed.rend(); --it) | ||
484 | 202 | { | ||
485 | 203 | if(!it.get_meta()->passed) | ||
486 | 204 | { | ||
487 | 205 | NonStrictMarking* m = encoder.decode(it); | ||
488 | 206 | m->meta = it.get_meta(); | ||
489 | 207 | return m; | ||
490 | 208 | } | ||
491 | 209 | } | ||
492 | 210 | return NULL; | ||
493 | 211 | } | ||
494 | 212 | |||
495 | 213 | bool WorkflowPWListHybrid::add(NonStrictMarking* marking) | ||
496 | 214 | { | ||
497 | 215 | discoveredMarkings++; | ||
498 | 216 | std::pair<bool, ptriepointer_t<MetaData*> > res = | ||
499 | 217 | passed.insert(encoder.encode(marking)); | ||
500 | 218 | |||
501 | 219 | if (!res.first) { | ||
502 | 220 | return false; | ||
503 | 221 | } | ||
504 | 222 | else | ||
505 | 223 | { | ||
506 | 224 | MetaDataWithTraceAndEncoding* meta = | ||
507 | 225 | new MetaDataWithTraceAndEncoding(); | ||
508 | 226 | meta->generatedBy = marking->getGeneratedBy(); | ||
509 | 227 | meta->ep = res.second; | ||
510 | 228 | meta->parent = parent; | ||
511 | 229 | meta->totalDelay = marking->calculateTotalDelay(); | ||
512 | 230 | |||
513 | 231 | res.second.set_meta(meta); | ||
514 | 232 | |||
515 | 233 | stored++; | ||
516 | 234 | |||
517 | 235 | // using min first waiting-list, weight is allready in pointer | ||
518 | 236 | waiting_list->add(NULL, res.second); | ||
519 | 237 | return true; | ||
520 | 238 | } | ||
521 | 239 | } | ||
522 | 240 | |||
523 | 241 | NonStrictMarking* WorkflowPWListHybrid::addToPassed | ||
524 | 242 | (NonStrictMarking* marking, bool strong) | ||
525 | 243 | { | ||
526 | 244 | discoveredMarkings++; | ||
527 | 245 | std::pair<bool, ptriepointer_t<MetaData*> > res = | ||
528 | 246 | passed.insert(encoder.encode(marking)); | ||
529 | 247 | |||
530 | 248 | |||
531 | 249 | |||
532 | 250 | if (!res.first) { | ||
533 | 251 | NonStrictMarking* old = encoder.decode(res.second); | ||
534 | 252 | |||
535 | 253 | MetaDataWithTraceAndEncoding* meta = | ||
536 | 254 | (MetaDataWithTraceAndEncoding*)res.second.get_meta(); | ||
537 | 255 | old->setGeneratedBy(meta->generatedBy); | ||
538 | 256 | old->meta = meta; | ||
539 | 257 | last_pointer = res.second; | ||
540 | 258 | return old; | ||
541 | 259 | } else { | ||
542 | 260 | stored++; | ||
543 | 261 | |||
544 | 262 | if(strong) marking->meta = new MetaDataWithTraceAndEncoding(); | ||
545 | 263 | else marking->meta = new WorkflowSoundnessMetaDataWithEncoding(); | ||
546 | 264 | |||
547 | 265 | MetaDataWithTraceAndEncoding* meta = | ||
548 | 266 | (MetaDataWithTraceAndEncoding*) marking->meta; | ||
549 | 267 | meta->ep = res.second; | ||
550 | 268 | meta->parent = this->parent; | ||
551 | 269 | meta->generatedBy = marking->getGeneratedBy(); | ||
552 | 270 | meta->totalDelay = marking->meta->totalDelay; | ||
553 | 271 | |||
554 | 272 | res.second.set_meta(meta); | ||
555 | 273 | last_pointer = res.second; | ||
556 | 274 | return NULL; | ||
557 | 275 | } | ||
558 | 276 | } | ||
559 | 277 | |||
560 | 278 | void WorkflowPWListHybrid::addLastToWaiting() | ||
561 | 279 | { | ||
562 | 280 | // using min first waiting-list, weight is allready in pointer | ||
563 | 281 | waiting_list->add(NULL, last_pointer); | ||
564 | 282 | } | ||
565 | 283 | |||
566 | 284 | |||
567 | 285 | |||
568 | 166 | 286 | ||
569 | 167 | } | 287 | } |
570 | 168 | } | 288 | } |
571 | 169 | 289 | ||
572 | === modified file 'src/DiscreteVerification/DataStructures/WorkflowPWList.hpp' | |||
573 | --- src/DiscreteVerification/DataStructures/WorkflowPWList.hpp 2015-06-22 22:10:16 +0000 | |||
574 | +++ src/DiscreteVerification/DataStructures/WorkflowPWList.hpp 2015-08-20 13:27:24 +0000 | |||
575 | @@ -15,6 +15,7 @@ | |||
576 | 15 | #include "NonStrictMarking.hpp" | 15 | #include "NonStrictMarking.hpp" |
577 | 16 | #include "WaitingList.hpp" | 16 | #include "WaitingList.hpp" |
578 | 17 | #include "PWList.hpp" | 17 | #include "PWList.hpp" |
579 | 18 | #include "CoveredMarkingVisitor.h" | ||
580 | 18 | 19 | ||
581 | 19 | namespace VerifyTAPN { | 20 | namespace VerifyTAPN { |
582 | 20 | namespace DiscreteVerification { | 21 | namespace DiscreteVerification { |
583 | @@ -51,6 +52,28 @@ | |||
584 | 51 | } | 52 | } |
585 | 52 | 53 | ||
586 | 53 | }; | 54 | }; |
587 | 55 | |||
588 | 56 | class WorkflowPWListHybrid : public WorkflowPWListBasic, public PWListHybrid { | ||
589 | 57 | private: | ||
590 | 58 | CoveredMarkingVisitor visitor; | ||
591 | 59 | ptriepointer_t<MetaData*> last_pointer; | ||
592 | 60 | public: | ||
593 | 61 | WorkflowPWListHybrid(TAPN::TimedArcPetriNet& tapn, | ||
594 | 62 | WaitingList<ptriepointer_t<MetaData*> >* w_l, | ||
595 | 63 | int knumber, | ||
596 | 64 | int nplaces, | ||
597 | 65 | int mage); | ||
598 | 66 | ~WorkflowPWListHybrid(); | ||
599 | 67 | virtual NonStrictMarking* getCoveredMarking(NonStrictMarking* marking, bool useLinearSweep); | ||
600 | 68 | virtual NonStrictMarking* getUnpassed(); | ||
601 | 69 | virtual bool add(NonStrictMarking* marking); | ||
602 | 70 | virtual NonStrictMarking* addToPassed(NonStrictMarking* marking, bool strong); | ||
603 | 71 | virtual void addLastToWaiting(); | ||
604 | 72 | virtual void setParent(NonStrictMarking* marking, NonStrictMarking*) | ||
605 | 73 | { | ||
606 | 74 | ((MetaDataWithTraceAndEncoding*)marking->meta)->parent = parent; | ||
607 | 75 | } | ||
608 | 76 | }; | ||
609 | 54 | 77 | ||
610 | 55 | } /* namespace DiscreteVerification */ | 78 | } /* namespace DiscreteVerification */ |
611 | 56 | } /* namespace VerifyTAPN */ | 79 | } /* namespace VerifyTAPN */ |
612 | 57 | 80 | ||
613 | === modified file 'src/DiscreteVerification/DataStructures/binarywrapper.h' | |||
614 | --- src/DiscreteVerification/DataStructures/binarywrapper.h 2015-06-17 09:03:12 +0000 | |||
615 | +++ src/DiscreteVerification/DataStructures/binarywrapper.h 2015-08-20 13:27:24 +0000 | |||
616 | @@ -9,6 +9,8 @@ | |||
617 | 9 | #include <stdio.h> | 9 | #include <stdio.h> |
618 | 10 | #include <iostream> | 10 | #include <iostream> |
619 | 11 | #include <string.h> | 11 | #include <string.h> |
620 | 12 | #include <assert.h> | ||
621 | 13 | #include <stdint.h> | ||
622 | 12 | 14 | ||
623 | 13 | #ifndef BINARYWRAPPER_H | 15 | #ifndef BINARYWRAPPER_H |
624 | 14 | #define BINARYWRAPPER_H | 16 | #define BINARYWRAPPER_H |
625 | @@ -17,44 +19,175 @@ | |||
626 | 17 | typedef unsigned int uint; | 19 | typedef unsigned int uint; |
627 | 18 | typedef unsigned char uchar; | 20 | typedef unsigned char uchar; |
628 | 19 | 21 | ||
629 | 22 | /** | ||
630 | 23 | * Wrapper for binary data. This provides easy access to individual bits, | ||
631 | 24 | * heap allocation and comparison. Notice that one has to make sure to | ||
632 | 25 | * explicitly call release() if one wishes to deallocate (possibly shared data). | ||
633 | 26 | * | ||
634 | 27 | */ | ||
635 | 20 | template<class T> | 28 | template<class T> |
636 | 21 | class binarywrapper_t | 29 | class binarywrapper_t |
637 | 22 | { | 30 | { |
638 | 23 | public: | 31 | public: |
639 | 24 | // Constructors | 32 | // Constructors |
640 | 33 | /** | ||
641 | 34 | * Empty constructor, no data is allocated | ||
642 | 35 | */ | ||
643 | 36 | inline | ||
644 | 25 | binarywrapper_t(); | 37 | binarywrapper_t(); |
645 | 38 | |||
646 | 39 | /** | ||
647 | 40 | Allocates a room for at least size bits | ||
648 | 41 | */ | ||
649 | 42 | inline | ||
650 | 26 | binarywrapper_t(uint size); | 43 | binarywrapper_t(uint size); |
651 | 44 | |||
652 | 45 | /** | ||
653 | 46 | * Constructor for copying over data from latest the offset'th bit. | ||
654 | 47 | * Detects overflows. | ||
655 | 48 | * @param other: wrapper to copy from | ||
656 | 49 | * @param offset: maximal number of bits to skip. | ||
657 | 50 | */ | ||
658 | 51 | inline | ||
659 | 27 | binarywrapper_t(const binarywrapper_t& other, uint offset); | 52 | binarywrapper_t(const binarywrapper_t& other, uint offset); |
660 | 28 | binarywrapper_t(const binarywrapper_t& other, uint size, uint offset, | 53 | binarywrapper_t(const binarywrapper_t& other, uint size, uint offset, |
661 | 29 | uint encodingsize); | 54 | uint encodingsize); |
662 | 30 | binarywrapper_t(uchar* raw, uint size, uint offset, uint encsize); | 55 | binarywrapper_t(uchar* raw, uint size, uint offset, uint encsize); |
663 | 56 | |||
664 | 57 | /** | ||
665 | 58 | * Assign (not copy) raw data to pointer. Set number of bytes to size | ||
666 | 59 | * @param raw: some memory to point to | ||
667 | 60 | * @param size: number of bytes. | ||
668 | 61 | */ | ||
669 | 62 | inline | ||
670 | 31 | binarywrapper_t(uchar* raw, uint size); | 63 | binarywrapper_t(uchar* raw, uint size); |
671 | 32 | 64 | ||
673 | 33 | // Destructor | 65 | /** |
674 | 66 | * Empty destructor. Does NOT deallocate data - do this with explicit | ||
675 | 67 | * call to release(). | ||
676 | 68 | */ | ||
677 | 69 | inline | ||
678 | 34 | ~binarywrapper_t(); | 70 | ~binarywrapper_t(); |
679 | 35 | 71 | ||
681 | 36 | // Copy and clones | 72 | /** |
682 | 73 | * Makes a complete copy, including new heap-allocation | ||
683 | 74 | * @return an exact copy, but in a different area of the heap. | ||
684 | 75 | */ | ||
685 | 76 | inline | ||
686 | 37 | binarywrapper_t clone() const; | 77 | binarywrapper_t clone() const; |
687 | 78 | |||
688 | 79 | /** | ||
689 | 80 | * Copy over data and meta-data from other, but insert only into target | ||
690 | 81 | * after offset bits. | ||
691 | 82 | * Notice that this can cause memory-corruption if there is not enough | ||
692 | 83 | * room in target, or to many bits are skipped. | ||
693 | 84 | * @param other: wrapper to copy from | ||
694 | 85 | * @param offset: bits to skip | ||
695 | 86 | */ | ||
696 | 87 | inline | ||
697 | 38 | void copy(const binarywrapper_t& other, uint offset); | 88 | void copy(const binarywrapper_t& other, uint offset); |
698 | 89 | |||
699 | 90 | /** | ||
700 | 91 | * Copy over size bytes form raw data. Assumes that current wrapper has | ||
701 | 92 | * enough room. | ||
702 | 93 | * @param raw: source data | ||
703 | 94 | * @param size: number of bytes to copy | ||
704 | 95 | */ | ||
705 | 96 | inline | ||
706 | 39 | void copy(const uchar* raw, uint size); | 97 | void copy(const uchar* raw, uint size); |
707 | 40 | 98 | ||
708 | 41 | // accessors | 99 | // accessors |
709 | 100 | /** | ||
710 | 101 | * Get value of the place'th bit | ||
711 | 102 | * @param place: bit index | ||
712 | 103 | * @return | ||
713 | 104 | */ | ||
714 | 105 | inline | ||
715 | 42 | bool at(const uint place) const; | 106 | bool at(const uint place) const; |
716 | 107 | |||
717 | 108 | /** | ||
718 | 109 | * number of bytes allocated in heap | ||
719 | 110 | * @return | ||
720 | 111 | */ | ||
721 | 112 | inline | ||
722 | 43 | uint size() const; | 113 | uint size() const; |
724 | 44 | uchar* raw() const; | 114 | |
725 | 115 | /** | ||
726 | 116 | * Raw access to data | ||
727 | 117 | * @return | ||
728 | 118 | */ | ||
729 | 119 | inline | ||
730 | 120 | uchar*& raw(); | ||
731 | 121 | |||
732 | 122 | /** | ||
733 | 123 | * Raw access to data when in const setting | ||
734 | 124 | * @return | ||
735 | 125 | */ | ||
736 | 126 | inline | ||
737 | 127 | uchar* const_raw() const; | ||
738 | 128 | |||
739 | 129 | /** | ||
740 | 130 | * pretty print of content | ||
741 | 131 | */ | ||
742 | 132 | inline | ||
743 | 45 | void print() const; | 133 | void print() const; |
744 | 134 | |||
745 | 135 | /** | ||
746 | 136 | * finds the overhead (unused number of bits) when allocating for size | ||
747 | 137 | * bits. | ||
748 | 138 | * @param size: number of bits | ||
749 | 139 | * @return | ||
750 | 140 | */ | ||
751 | 141 | inline | ||
752 | 46 | static size_t overhead(uint size); | 142 | static size_t overhead(uint size); |
753 | 47 | 143 | ||
754 | 48 | // modifiers | 144 | // modifiers |
755 | 145 | /** | ||
756 | 146 | * Change value of place'th bit | ||
757 | 147 | * @param place: index of bit to change | ||
758 | 148 | * @param value: desired value | ||
759 | 149 | */ | ||
760 | 150 | inline | ||
761 | 49 | void set(const uint place, const bool value) const; | 151 | void set(const uint place, const bool value) const; |
762 | 152 | |||
763 | 153 | /** | ||
764 | 154 | * Sets all memory on heap to 0 | ||
765 | 155 | */ | ||
766 | 156 | inline | ||
767 | 50 | void zero() const; | 157 | void zero() const; |
769 | 51 | void release() const; | 158 | |
770 | 159 | /** | ||
771 | 160 | * Deallocates memory stored on heap | ||
772 | 161 | */ | ||
773 | 162 | inline | ||
774 | 163 | void release(); | ||
775 | 164 | |||
776 | 52 | void set_meta(T data); | 165 | void set_meta(T data); |
777 | 53 | T get_meta() const; | 166 | T get_meta() const; |
778 | 167 | |||
779 | 168 | /** | ||
780 | 169 | * Nice access to single bits | ||
781 | 170 | * @param i: index to access | ||
782 | 171 | * @return | ||
783 | 172 | */ | ||
784 | 173 | inline | ||
785 | 54 | uchar operator[](int i); | 174 | uchar operator[](int i); |
786 | 175 | |||
787 | 176 | /** | ||
788 | 177 | * Removes a number of bytes from end of heap-allocated data if any is | ||
789 | 178 | * allocated nothing happens if not. Bound-checks. | ||
790 | 179 | * @param number of bytes to remove. | ||
791 | 180 | */ | ||
792 | 181 | inline | ||
793 | 55 | void pop_front(unsigned short); | 182 | void pop_front(unsigned short); |
794 | 56 | 183 | ||
796 | 57 | inline int cmp(const binarywrapper_t &other) | 184 | /** |
797 | 185 | * Compares two wrappers. Assumes that smaller number of bytes also means | ||
798 | 186 | * a smaller wrapper. Otherwise compares byte by byte. | ||
799 | 187 | * @param other: wrapper to compare to | ||
800 | 188 | * @return -1 if other is smaller, 0 if same, 1 if other is larger | ||
801 | 189 | */ | ||
802 | 190 | inline int cmp(const binarywrapper_t &other) const | ||
803 | 58 | { | 191 | { |
804 | 59 | if(_nbytes != other._nbytes) | 192 | if(_nbytes != other._nbytes) |
805 | 60 | { | 193 | { |
806 | @@ -62,63 +195,33 @@ | |||
807 | 62 | else return 1; | 195 | else return 1; |
808 | 63 | } | 196 | } |
809 | 64 | 197 | ||
817 | 65 | for(int i = _nbytes - 1; i >= 0; i--) | 198 | return memcmp(_blob, other.const_raw(), other._nbytes ); |
818 | 66 | { | 199 | } |
812 | 67 | if(_blob[i] < other._blob[i]) | ||
813 | 68 | return -1; | ||
814 | 69 | else if (_blob[i] > other._blob[i]) | ||
815 | 70 | return 1; | ||
816 | 71 | } | ||
819 | 72 | 200 | ||
824 | 73 | return 0; | 201 | /** |
825 | 74 | } | 202 | * Compares wrappers bytes by bytes. If sizes do not match, they are not |
826 | 75 | 203 | * equal. If sizes match, compares byte by byte. | |
827 | 76 | // Operators | 204 | * @param enc1 |
828 | 205 | * @param enc2 | ||
829 | 206 | * @return true if a match, false otherwise | ||
830 | 207 | */ | ||
831 | 77 | inline friend bool operator==( const binarywrapper_t &enc1, | 208 | inline friend bool operator==( const binarywrapper_t &enc1, |
832 | 78 | const binarywrapper_t &enc2) { | 209 | const binarywrapper_t &enc2) { |
870 | 79 | if(enc1._nbytes != enc2._nbytes) | 210 | return enc1.cmp(enc2) == 0; |
834 | 80 | return false; | ||
835 | 81 | |||
836 | 82 | for(size_t i = 0; i < enc1._nbytes; i++) | ||
837 | 83 | if(enc1._blob[i] != enc2._blob[i]) | ||
838 | 84 | return false; | ||
839 | 85 | |||
840 | 86 | return true; | ||
841 | 87 | } | ||
842 | 88 | |||
843 | 89 | /* inline friend bool operator <=( const binarywrapper &enc1, | ||
844 | 90 | const binarywrapper &enc2) | ||
845 | 91 | { | ||
846 | 92 | if(enc1.numberOfBytes != enc2.numberOfBytes) | ||
847 | 93 | return enc1.numberOfBytes < enc2.numberOfBytes; | ||
848 | 94 | |||
849 | 95 | for(size_t i = 0; i < enc1.numberOfBytes; i++) | ||
850 | 96 | if(enc1.blob[i] < enc2.blob[i]) | ||
851 | 97 | return true; | ||
852 | 98 | else if (enc1.blob[i] > enc2.blob[i]) | ||
853 | 99 | return false; | ||
854 | 100 | |||
855 | 101 | return true; | ||
856 | 102 | }*/ | ||
857 | 103 | |||
858 | 104 | inline friend bool operator<( const binarywrapper_t &enc1, | ||
859 | 105 | const binarywrapper_t &enc2) { | ||
860 | 106 | if(enc1._nbytes != enc2._nbytes) | ||
861 | 107 | return enc1._nbytes < enc2._nbytes; | ||
862 | 108 | |||
863 | 109 | for(size_t i = 0; i < enc1._nbytes; i++) | ||
864 | 110 | if(enc1._blob[i] < enc2._blob[i]) | ||
865 | 111 | return true; | ||
866 | 112 | else if (enc1._blob[i] > enc2._blob[i]) | ||
867 | 113 | return false; | ||
868 | 114 | |||
869 | 115 | return false; | ||
871 | 116 | } | 211 | } |
872 | 117 | 212 | ||
873 | 118 | private: | 213 | private: |
874 | 214 | |||
875 | 215 | // blob of heap-allocated data | ||
876 | 119 | uchar* _blob; | 216 | uchar* _blob; |
878 | 120 | unsigned short _nbytes; | 217 | |
879 | 218 | // number of bytes allocated on heap | ||
880 | 219 | unsigned short _nbytes; | ||
881 | 220 | |||
882 | 221 | // meta data to carry | ||
883 | 121 | T _meta; | 222 | T _meta; |
884 | 223 | |||
885 | 224 | // masks for single-bit access | ||
886 | 122 | const static uchar _masks[8]; | 225 | const static uchar _masks[8]; |
887 | 123 | }; | 226 | }; |
888 | 124 | 227 | ||
889 | @@ -273,7 +376,13 @@ | |||
890 | 273 | } | 376 | } |
891 | 274 | 377 | ||
892 | 275 | template<class T> | 378 | template<class T> |
894 | 276 | uchar* binarywrapper_t<T>::raw() const | 379 | uchar*& binarywrapper_t<T>::raw() |
895 | 380 | { | ||
896 | 381 | return _blob; | ||
897 | 382 | } | ||
898 | 383 | |||
899 | 384 | template<class T> | ||
900 | 385 | uchar* binarywrapper_t<T>::const_raw() const | ||
901 | 277 | { | 386 | { |
902 | 278 | return _blob; | 387 | return _blob; |
903 | 279 | } | 388 | } |
904 | @@ -292,6 +401,8 @@ | |||
905 | 292 | { | 401 | { |
906 | 293 | if(_nbytes == 0) return; // Special case, nothing to do! | 402 | if(_nbytes == 0) return; // Special case, nothing to do! |
907 | 294 | unsigned short int nbytes; | 403 | unsigned short int nbytes; |
908 | 404 | |||
909 | 405 | // make sure we do not remove to much, but as much as we can. | ||
910 | 295 | if(topop >= _nbytes) | 406 | if(topop >= _nbytes) |
911 | 296 | { | 407 | { |
912 | 297 | topop = _nbytes; | 408 | topop = _nbytes; |
913 | @@ -340,9 +451,10 @@ | |||
914 | 340 | } | 451 | } |
915 | 341 | 452 | ||
916 | 342 | template<class T> | 453 | template<class T> |
918 | 343 | void binarywrapper_t<T>::release() const | 454 | void binarywrapper_t<T>::release() |
919 | 344 | { | 455 | { |
920 | 345 | delete[] _blob; | 456 | delete[] _blob; |
921 | 457 | _blob = NULL; | ||
922 | 346 | } | 458 | } |
923 | 347 | 459 | ||
924 | 348 | template<class T> | 460 | template<class T> |
925 | 349 | 461 | ||
926 | === modified file 'src/DiscreteVerification/DataStructures/ptrie.h' | |||
927 | --- src/DiscreteVerification/DataStructures/ptrie.h 2015-06-22 21:03:26 +0000 | |||
928 | +++ src/DiscreteVerification/DataStructures/ptrie.h 2015-08-20 13:27:24 +0000 | |||
929 | @@ -1,5 +1,5 @@ | |||
930 | 1 | /* | 1 | /* |
932 | 2 | * File: PTrie.h | 2 | * File: ptrie.h |
933 | 3 | * Author: Peter G. Jensen | 3 | * Author: Peter G. Jensen |
934 | 4 | * | 4 | * |
935 | 5 | * Created on 10 June 2015, 18:44 | 5 | * Created on 10 June 2015, 18:44 |
936 | @@ -9,10 +9,12 @@ | |||
937 | 9 | #define PTRIE_H | 9 | #define PTRIE_H |
938 | 10 | 10 | ||
939 | 11 | #include "binarywrapper.h" | 11 | #include "binarywrapper.h" |
940 | 12 | #include "visitor.h" | ||
941 | 12 | #include <assert.h> | 13 | #include <assert.h> |
942 | 13 | #include <limits> | 14 | #include <limits> |
943 | 14 | #include <vector> | 15 | #include <vector> |
944 | 15 | #include <stdint.h> | 16 | #include <stdint.h> |
945 | 17 | #include <stack> | ||
946 | 16 | 18 | ||
947 | 17 | namespace ptrie | 19 | namespace ptrie |
948 | 18 | { | 20 | { |
949 | @@ -35,7 +37,15 @@ | |||
950 | 35 | void set_meta(T); | 37 | void set_meta(T); |
951 | 36 | uint write_partial_encoding(encoding_t&) const; | 38 | uint write_partial_encoding(encoding_t&) const; |
952 | 37 | encoding_t& remainder() const; | 39 | encoding_t& remainder() const; |
953 | 40 | |||
954 | 38 | ptriepointer_t() : container(NULL), index(0) {}; | 41 | ptriepointer_t() : container(NULL), index(0) {}; |
955 | 42 | |||
956 | 43 | ptriepointer_t<T>& operator=(const ptriepointer_t<T>&); | ||
957 | 44 | ptriepointer_t<T>& operator++(); | ||
958 | 45 | ptriepointer_t<T>& operator--(); | ||
959 | 46 | bool operator==(const ptriepointer_t<T>& other); | ||
960 | 47 | bool operator!=(const ptriepointer_t<T>& other); | ||
961 | 48 | |||
962 | 39 | }; | 49 | }; |
963 | 40 | 50 | ||
964 | 41 | template<typename T> | 51 | template<typename T> |
965 | @@ -45,6 +55,55 @@ | |||
966 | 45 | } | 55 | } |
967 | 46 | 56 | ||
968 | 47 | template<typename T> | 57 | template<typename T> |
969 | 58 | |||
970 | 59 | ptriepointer_t<T>& ptriepointer_t<T>::operator= | ||
971 | 60 | (const ptriepointer_t<T>& other) | ||
972 | 61 | { | ||
973 | 62 | container = other.container; | ||
974 | 63 | index = other.index; | ||
975 | 64 | return *this; | ||
976 | 65 | } | ||
977 | 66 | |||
978 | 67 | template<typename T> | ||
979 | 68 | ptriepointer_t<T>& ptriepointer_t<T>::operator++() | ||
980 | 69 | { | ||
981 | 70 | ++index; | ||
982 | 71 | assert(index <= container->_next_free_entry); | ||
983 | 72 | return *this; | ||
984 | 73 | } | ||
985 | 74 | |||
986 | 75 | template<typename T> | ||
987 | 76 | ptriepointer_t<T>& ptriepointer_t<T>::operator--() | ||
988 | 77 | { | ||
989 | 78 | --index; | ||
990 | 79 | return *this; | ||
991 | 80 | } | ||
992 | 81 | |||
993 | 82 | template<typename T> | ||
994 | 83 | bool ptriepointer_t<T>::operator==(const ptriepointer_t<T>& other) | ||
995 | 84 | { | ||
996 | 85 | return other.container == container && other.index == index; | ||
997 | 86 | } | ||
998 | 87 | |||
999 | 88 | template<typename T> | ||
1000 | 89 | bool ptriepointer_t<T>::operator!=(const ptriepointer_t<T>& other) | ||
1001 | 90 | { | ||
1002 | 91 | return !(*this == other); | ||
1003 | 92 | } | ||
1004 | 93 | |||
1005 | 94 | /* | ||
1006 | 95 | template<typename T> | ||
1007 | 96 | void swap(ptriepointer<T>& lhs, ptriepointer<T>& rhs) | ||
1008 | 97 | { | ||
1009 | 98 | ptrie<T>* container = lhs.container; | ||
1010 | 99 | uint index = lhs.index; | ||
1011 | 100 | lhs.container = rhs.container; | ||
1012 | 101 | lhs.index = rhs.index; | ||
1013 | 102 | rhs.index = index; | ||
1014 | 103 | rhs.container = container; | ||
1015 | 104 | }*/ | ||
1016 | 105 | |||
1017 | 106 | template<typename T> | ||
1018 | 48 | T ptriepointer_t<T>::get_meta() const | 107 | T ptriepointer_t<T>::get_meta() const |
1019 | 49 | { | 108 | { |
1020 | 50 | return container->get_entry(index)->_data.get_meta(); | 109 | return container->get_entry(index)->_data.get_meta(); |
1021 | @@ -72,7 +131,7 @@ | |||
1022 | 72 | class ptrie_t { | 131 | class ptrie_t { |
1023 | 73 | typedef binarywrapper_t<T> encoding_t; | 132 | typedef binarywrapper_t<T> encoding_t; |
1024 | 74 | friend class ptriepointer_t<T>; | 133 | friend class ptriepointer_t<T>; |
1026 | 75 | public: | 134 | private: |
1027 | 76 | 135 | ||
1028 | 77 | // nodes in the tree | 136 | // nodes in the tree |
1029 | 78 | struct node_t | 137 | struct node_t |
1030 | @@ -123,6 +182,12 @@ | |||
1031 | 123 | std::pair<bool, ptriepointer_t<T> > find(const encoding_t& encoding); | 182 | std::pair<bool, ptriepointer_t<T> > find(const encoding_t& encoding); |
1032 | 124 | bool consistent() const; | 183 | bool consistent() const; |
1033 | 125 | uint size() const { return _next_free_entry; } | 184 | uint size() const { return _next_free_entry; } |
1034 | 185 | ptriepointer_t<T> begin(); | ||
1035 | 186 | ptriepointer_t<T> end(); | ||
1036 | 187 | ptriepointer_t<T> last(); | ||
1037 | 188 | ptriepointer_t<T> rend(); | ||
1038 | 189 | |||
1039 | 190 | void visit(visitor_t<T>&); | ||
1040 | 126 | }; | 191 | }; |
1041 | 127 | 192 | ||
1042 | 128 | template<typename T> | 193 | template<typename T> |
1043 | @@ -173,6 +238,30 @@ | |||
1044 | 173 | } | 238 | } |
1045 | 174 | 239 | ||
1046 | 175 | template<typename T> | 240 | template<typename T> |
1047 | 241 | ptriepointer_t<T> ptrie_t<T>::begin() | ||
1048 | 242 | { | ||
1049 | 243 | return ptriepointer_t<T>(this, 0); | ||
1050 | 244 | } | ||
1051 | 245 | |||
1052 | 246 | template<typename T> | ||
1053 | 247 | ptriepointer_t<T> ptrie_t<T>::end() | ||
1054 | 248 | { | ||
1055 | 249 | return ptriepointer_t<T>(this, _next_free_entry); | ||
1056 | 250 | } | ||
1057 | 251 | |||
1058 | 252 | template<typename T> | ||
1059 | 253 | ptriepointer_t<T> ptrie_t<T>::last() | ||
1060 | 254 | { | ||
1061 | 255 | return ptriepointer_t<T>(this, _next_free_entry-1); | ||
1062 | 256 | } | ||
1063 | 257 | |||
1064 | 258 | template<typename T> | ||
1065 | 259 | ptriepointer_t<T> ptrie_t<T>::rend() | ||
1066 | 260 | { | ||
1067 | 261 | return ptriepointer_t<T>(this, std::numeric_limits<uint>::max()); | ||
1068 | 262 | } | ||
1069 | 263 | |||
1070 | 264 | template<typename T> | ||
1071 | 176 | typename ptrie_t<T>::node_t* | 265 | typename ptrie_t<T>::node_t* |
1072 | 177 | ptrie_t<T>::get_node(uint index) const | 266 | ptrie_t<T>::get_node(uint index) const |
1073 | 178 | { | 267 | { |
1074 | @@ -218,6 +307,8 @@ | |||
1075 | 218 | bool ptrie_t<T>::consistent() const | 307 | bool ptrie_t<T>::consistent() const |
1076 | 219 | { | 308 | { |
1077 | 220 | return true; | 309 | return true; |
1078 | 310 | assert(_next_free_node >= _nodevector.size()); | ||
1079 | 311 | assert(_next_free_entry >= _entryvector.size()); | ||
1080 | 221 | for(size_t i = 0; i < _next_free_node; ++i) | 312 | for(size_t i = 0; i < _next_free_node; ++i) |
1081 | 222 | { | 313 | { |
1082 | 223 | node_t* node = get_node(i); | 314 | node_t* node = get_node(i); |
1083 | @@ -269,6 +360,61 @@ | |||
1084 | 269 | } | 360 | } |
1085 | 270 | 361 | ||
1086 | 271 | template<typename T> | 362 | template<typename T> |
1087 | 363 | void ptrie_t<T>::visit(visitor_t<T>& visitor) | ||
1088 | 364 | { | ||
1089 | 365 | std::stack<std::pair<uint, uint> > waiting; | ||
1090 | 366 | waiting.push(std::pair<int, uint>(-1, 0)); | ||
1091 | 367 | |||
1092 | 368 | bool stop = false; | ||
1093 | 369 | do{ | ||
1094 | 370 | int distance = waiting.top().first; | ||
1095 | 371 | uint n_index = waiting.top().second; | ||
1096 | 372 | waiting.pop(); | ||
1097 | 373 | |||
1098 | 374 | if(distance > -1) | ||
1099 | 375 | { | ||
1100 | 376 | visitor.back(distance); | ||
1101 | 377 | visitor.set(distance, true); // only high on stack | ||
1102 | 378 | } | ||
1103 | 379 | |||
1104 | 380 | node_t* node = get_node(n_index); | ||
1105 | 381 | bool skip = false; | ||
1106 | 382 | do | ||
1107 | 383 | { | ||
1108 | 384 | |||
1109 | 385 | if(node->_highpos != 0) | ||
1110 | 386 | { | ||
1111 | 387 | waiting.push(std::pair<uint, uint>(distance + 1, node->_highpos)); | ||
1112 | 388 | } | ||
1113 | 389 | |||
1114 | 390 | if(node->_lowpos == 0) break; | ||
1115 | 391 | else | ||
1116 | 392 | { | ||
1117 | 393 | ++distance; | ||
1118 | 394 | node = get_node(node->_lowpos); | ||
1119 | 395 | skip = visitor.set(distance, false); | ||
1120 | 396 | } | ||
1121 | 397 | |||
1122 | 398 | } while(!skip); | ||
1123 | 399 | |||
1124 | 400 | distance += 1; | ||
1125 | 401 | |||
1126 | 402 | uint bucketsize = 0; | ||
1127 | 403 | if(!skip) | ||
1128 | 404 | { | ||
1129 | 405 | if(node->_highcount > 0) bucketsize += node->_highcount; | ||
1130 | 406 | if(node->_lowcount > 0) bucketsize += node->_lowcount; | ||
1131 | 407 | |||
1132 | 408 | for(uint i = 0; i < bucketsize && !stop; ++i) | ||
1133 | 409 | { | ||
1134 | 410 | stop = visitor.set_remainder(distance, | ||
1135 | 411 | ptriepointer_t<T>(this, node->_entries[i])); | ||
1136 | 412 | } | ||
1137 | 413 | } | ||
1138 | 414 | } while(!waiting.empty() && !stop); | ||
1139 | 415 | } | ||
1140 | 416 | |||
1141 | 417 | template<typename T> | ||
1142 | 272 | bool ptrie_t<T>::best_match(const encoding_t& encoding, uint& tree_pos, | 418 | bool ptrie_t<T>::best_match(const encoding_t& encoding, uint& tree_pos, |
1143 | 273 | uint& e_index, uint& enc_pos, uint& b_index, uint& bucketsize) | 419 | uint& e_index, uint& enc_pos, uint& b_index, uint& bucketsize) |
1144 | 274 | { | 420 | { |
1145 | @@ -316,7 +462,7 @@ | |||
1146 | 316 | // start by creating an encoding that "points" to the "unmatched" | 462 | // start by creating an encoding that "points" to the "unmatched" |
1147 | 317 | // part of the encoding. Notice, this is a shallow copy, no actual | 463 | // part of the encoding. Notice, this is a shallow copy, no actual |
1148 | 318 | // heap-allocation happens! | 464 | // heap-allocation happens! |
1150 | 319 | encoding_t s_enc = encoding_t( encoding.raw(), | 465 | encoding_t s_enc = encoding_t( encoding.const_raw(), |
1151 | 320 | (encsize - enc_pos), | 466 | (encsize - enc_pos), |
1152 | 321 | enc_pos, | 467 | enc_pos, |
1153 | 322 | encsize); | 468 | encsize); |
1154 | @@ -341,18 +487,18 @@ | |||
1155 | 341 | e_index = node->_entries[b_index]; | 487 | e_index = node->_entries[b_index]; |
1156 | 342 | break; | 488 | break; |
1157 | 343 | } | 489 | } |
1159 | 344 | else if(cmp == 1) | 490 | else if(cmp > 0) |
1160 | 345 | { | 491 | { |
1161 | 346 | low = b_index + 1; | 492 | low = b_index + 1; |
1162 | 347 | } | 493 | } |
1164 | 348 | else //if cmp == -1 | 494 | else //if cmp < 0 |
1165 | 349 | { | 495 | { |
1166 | 350 | high = b_index - 1; | 496 | high = b_index - 1; |
1167 | 351 | } | 497 | } |
1168 | 352 | 498 | ||
1169 | 353 | if(low > high) | 499 | if(low > high) |
1170 | 354 | { | 500 | { |
1172 | 355 | if(cmp == 1) | 501 | if(cmp > 0) |
1173 | 356 | b_index += 1; | 502 | b_index += 1; |
1174 | 357 | break; | 503 | break; |
1175 | 358 | } | 504 | } |
1176 | @@ -367,13 +513,13 @@ | |||
1177 | 367 | /*int tmp;// refference debug code! | 513 | /*int tmp;// refference debug code! |
1178 | 368 | for(tmp = 0; tmp < bucketsize; ++tmp) | 514 | for(tmp = 0; tmp < bucketsize; ++tmp) |
1179 | 369 | { | 515 | { |
1182 | 370 | entry_t* ent = getEntry(node->entries[tmp]); | 516 | entry_t* ent = get_entry(node->_entries[tmp]); |
1183 | 371 | if(ent->data < s_enc) | 517 | if(ent->_data.cmp(s_enc) < 0) |
1184 | 372 | { | 518 | { |
1185 | 373 | continue; | 519 | continue; |
1186 | 374 | } | 520 | } |
1187 | 375 | else | 521 | else |
1189 | 376 | if(ent->data == s_enc) | 522 | if(ent->_data == s_enc) |
1190 | 377 | { | 523 | { |
1191 | 378 | assert(found); | 524 | assert(found); |
1192 | 379 | break; | 525 | break; |
1193 | @@ -491,8 +637,8 @@ | |||
1194 | 491 | uint enc_pos; | 637 | uint enc_pos; |
1195 | 492 | uint bucketsize; | 638 | uint bucketsize; |
1196 | 493 | uint e_index; | 639 | uint e_index; |
1199 | 494 | 640 | uint b_index; | |
1200 | 495 | if(best_match(encoding, tree_pos, e_index, enc_pos, bucketsize)) | 641 | if(best_match(encoding, tree_pos, e_index, enc_pos, b_index, bucketsize)) |
1201 | 496 | { | 642 | { |
1202 | 497 | return std::pair<bool, ptriepointer_t<T> >(true, | 643 | return std::pair<bool, ptriepointer_t<T> >(true, |
1203 | 498 | ptriepointer_t<T>(this, e_index)); | 644 | ptriepointer_t<T>(this, e_index)); |
1204 | @@ -534,7 +680,7 @@ | |||
1205 | 534 | remainder_size, | 680 | remainder_size, |
1206 | 535 | enc_pos, | 681 | enc_pos, |
1207 | 536 | encsize); | 682 | encsize); |
1209 | 537 | assert(n_entry->_data.raw() != encoding.raw()); | 683 | //assert(n_entry->_data.const_raw() != encoding.const_raw()); |
1210 | 538 | 684 | ||
1211 | 539 | n_entry->_nodeindex = tree_pos; | 685 | n_entry->_nodeindex = tree_pos; |
1212 | 540 | 686 | ||
1213 | 541 | 687 | ||
1214 | === added file 'src/DiscreteVerification/DataStructures/visitor.h' | |||
1215 | --- src/DiscreteVerification/DataStructures/visitor.h 1970-01-01 00:00:00 +0000 | |||
1216 | +++ src/DiscreteVerification/DataStructures/visitor.h 2015-08-20 13:27:24 +0000 | |||
1217 | @@ -0,0 +1,30 @@ | |||
1218 | 1 | /* | ||
1219 | 2 | * File: visitor.h | ||
1220 | 3 | * Author: Peter G. Jensen | ||
1221 | 4 | * | ||
1222 | 5 | * Created on 16 June 2015, 23:15 | ||
1223 | 6 | */ | ||
1224 | 7 | |||
1225 | 8 | #ifndef VISITOR_H | ||
1226 | 9 | #define VISITOR_H | ||
1227 | 10 | |||
1228 | 11 | #include <stdint.h> | ||
1229 | 12 | |||
1230 | 13 | namespace ptrie | ||
1231 | 14 | { | ||
1232 | 15 | template<typename T> | ||
1233 | 16 | class ptriepointer_t; | ||
1234 | 17 | |||
1235 | 18 | template<typename T> | ||
1236 | 19 | class visitor_t | ||
1237 | 20 | { | ||
1238 | 21 | public: | ||
1239 | 22 | virtual bool back(int index) = 0; | ||
1240 | 23 | virtual bool set(int index, bool value) = 0; | ||
1241 | 24 | virtual bool set_remainder(int index, ptriepointer_t<T> pointer) = 0; | ||
1242 | 25 | }; | ||
1243 | 26 | } | ||
1244 | 27 | |||
1245 | 28 | |||
1246 | 29 | #endif /* VISITOR_H */ | ||
1247 | 30 | |||
1248 | 0 | 31 | ||
1249 | === modified file 'src/DiscreteVerification/DiscreteVerification.cpp' | |||
1250 | --- src/DiscreteVerification/DiscreteVerification.cpp 2015-06-17 09:03:12 +0000 | |||
1251 | +++ src/DiscreteVerification/DiscreteVerification.cpp 2015-08-20 13:27:24 +0000 | |||
1252 | @@ -53,42 +53,63 @@ | |||
1253 | 53 | exit(1); | 53 | exit(1); |
1254 | 54 | } | 54 | } |
1255 | 55 | 55 | ||
1256 | 56 | if (options.getMemoryOptimization() != VerificationOptions::NO_MEMORY_OPTIMIZATION) { | ||
1257 | 57 | cout << "Workflow analysis currently does not support any memory optimizations (i.e. no PTries)." << endl; | ||
1258 | 58 | exit(1); | ||
1259 | 59 | } | ||
1260 | 60 | WaitingList<NonStrictMarking*>* strategy = getWaitingList<NonStrictMarking* > (query, options); | ||
1261 | 61 | if(options.getWorkflowMode() == VerificationOptions::WORKFLOW_SOUNDNESS){ | 56 | if(options.getWorkflowMode() == VerificationOptions::WORKFLOW_SOUNDNESS){ |
1263 | 62 | WorkflowSoundness* verifier = new WorkflowSoundness(tapn, *initialMarking, query, options, strategy); | 57 | WorkflowSoundness* verifier; |
1264 | 58 | if(options.getMemoryOptimization() == VerificationOptions::NO_MEMORY_OPTIMIZATION) | ||
1265 | 59 | { | ||
1266 | 60 | verifier = new WorkflowSoundness(tapn, *initialMarking, query, options, | ||
1267 | 61 | getWaitingList<NonStrictMarking* > (query, options)); | ||
1268 | 62 | } | ||
1269 | 63 | else | ||
1270 | 64 | { | ||
1271 | 65 | verifier = new WorkflowSoundnessPTrie(tapn, *initialMarking, query, options, | ||
1272 | 66 | getWaitingList<ptriepointer_t<MetaData*> > (query, options)); | ||
1273 | 67 | } | ||
1274 | 63 | 68 | ||
1290 | 64 | if(verifier->getModelType() == verifier->NOTTAWFN){ | 69 | if(verifier->getModelType() == verifier->NOTTAWFN){ |
1291 | 65 | std::cerr << "Model is not a TAWFN!" << std::endl; | 70 | std::cerr << "Model is not a TAWFN!" << std::endl; |
1292 | 66 | return -1; | 71 | return -1; |
1293 | 67 | }else if(verifier->getModelType() == verifier->ETAWFN){ | 72 | }else if(verifier->getModelType() == verifier->ETAWFN){ |
1294 | 68 | std::cout << "Model is a ETAWFN" << std::endl << std::endl; | 73 | std::cout << "Model is a ETAWFN" << std::endl << std::endl; |
1295 | 69 | }else if(verifier->getModelType() == verifier->MTAWFN){ | 74 | }else if(verifier->getModelType() == verifier->MTAWFN){ |
1296 | 70 | std::cout << "Model is a MTAWFN" << std::endl << std::endl; | 75 | std::cout << "Model is a MTAWFN" << std::endl << std::endl; |
1297 | 71 | } | 76 | } |
1298 | 72 | VerifyAndPrint( | 77 | VerifyAndPrint( |
1299 | 73 | tapn, | 78 | tapn, |
1300 | 74 | *verifier, | 79 | *verifier, |
1301 | 75 | options, | 80 | options, |
1302 | 76 | query); | 81 | query); |
1303 | 77 | verifier->printExecutionTime(cout); | 82 | verifier->printExecutionTime(cout); |
1304 | 78 | verifier->printMessages(cout); | 83 | verifier->printMessages(cout); |
1305 | 84 | #ifdef CLEANUP | ||
1306 | 85 | delete verifier; | ||
1307 | 86 | #endif | ||
1308 | 79 | } | 87 | } |
1309 | 80 | else{ | 88 | else{ |
1310 | 81 | // Assumes correct structure of net! | 89 | // Assumes correct structure of net! |
1312 | 82 | WorkflowStrongSoundnessReachability* verifier = new WorkflowStrongSoundnessReachability(tapn, *initialMarking, query, options, strategy); | 90 | WorkflowStrongSoundnessReachability* verifier; |
1313 | 91 | if(options.getMemoryOptimization() == VerificationOptions::NO_MEMORY_OPTIMIZATION) | ||
1314 | 92 | { | ||
1315 | 93 | verifier = new WorkflowStrongSoundnessReachability(tapn, *initialMarking, query, options, | ||
1316 | 94 | getWaitingList<NonStrictMarking* > (query, options)); | ||
1317 | 95 | } | ||
1318 | 96 | else | ||
1319 | 97 | { | ||
1320 | 98 | verifier = new WorkflowStrongSoundnessPTrie(tapn, *initialMarking, query, options, | ||
1321 | 99 | getWaitingList<ptriepointer_t<MetaData*> > (query, options)); | ||
1322 | 100 | } | ||
1323 | 83 | VerifyAndPrint( | 101 | VerifyAndPrint( |
1324 | 84 | tapn, | 102 | tapn, |
1325 | 85 | *verifier, | 103 | *verifier, |
1326 | 86 | options, | 104 | options, |
1327 | 87 | query); | 105 | query); |
1328 | 88 | verifier->printExecutionTime(cout); | 106 | verifier->printExecutionTime(cout); |
1329 | 107 | #ifdef CLEANUP | ||
1330 | 108 | delete verifier; | ||
1331 | 109 | #endif | ||
1332 | 89 | } | 110 | } |
1333 | 90 | 111 | ||
1335 | 91 | delete strategy; | 112 | |
1336 | 92 | return 0; | 113 | return 0; |
1337 | 93 | } | 114 | } |
1338 | 94 | 115 | ||
1339 | 95 | 116 | ||
1340 | === modified file 'src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp' | |||
1341 | --- src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp 2015-06-22 22:10:16 +0000 | |||
1342 | +++ src/DiscreteVerification/VerificationTypes/WorkflowSoundness.cpp 2015-08-20 13:27:24 +0000 | |||
1343 | @@ -6,6 +6,7 @@ | |||
1344 | 6 | */ | 6 | */ |
1345 | 7 | 7 | ||
1346 | 8 | #include "WorkflowSoundness.hpp" | 8 | #include "WorkflowSoundness.hpp" |
1347 | 9 | #include <limits> | ||
1348 | 9 | 10 | ||
1349 | 10 | namespace VerifyTAPN { | 11 | namespace VerifyTAPN { |
1350 | 11 | namespace DiscreteVerification { | 12 | namespace DiscreteVerification { |
1351 | @@ -13,6 +14,7 @@ | |||
1352 | 13 | WorkflowSoundness::WorkflowSoundness(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking*>* waiting_list) | 14 | WorkflowSoundness::WorkflowSoundness(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<NonStrictMarking*>* waiting_list) |
1353 | 14 | : Workflow(tapn, initialMarking, query, options), passedStack(), minExec(INT_MAX), linearSweepTreshold(3), coveredMarking(NULL), modelType(calculateModelType()){ | 15 | : Workflow(tapn, initialMarking, query, options), passedStack(), minExec(INT_MAX), linearSweepTreshold(3), coveredMarking(NULL), modelType(calculateModelType()){ |
1354 | 15 | pwList = new WorkflowPWList(waiting_list); | 16 | pwList = new WorkflowPWList(waiting_list); |
1355 | 17 | |||
1356 | 16 | } | 18 | } |
1357 | 17 | 19 | ||
1358 | 18 | 20 | ||
1359 | @@ -21,6 +23,17 @@ | |||
1360 | 21 | 23 | ||
1361 | 22 | }; | 24 | }; |
1362 | 23 | 25 | ||
1363 | 26 | WorkflowSoundnessPTrie::WorkflowSoundnessPTrie(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<ptriepointer_t<MetaData*> >* waiting_list) | ||
1364 | 27 | : WorkflowSoundness(tapn, initialMarking, query, options) { | ||
1365 | 28 | int kbound = modelType == MTAWFN ? (std::numeric_limits<int>::max() - 1) : options.getKBound(); | ||
1366 | 29 | pwList = new WorkflowPWListHybrid( tapn, | ||
1367 | 30 | waiting_list, | ||
1368 | 31 | kbound, | ||
1369 | 32 | tapn.getNumberOfPlaces(), | ||
1370 | 33 | tapn.getMaxConstant()); | ||
1371 | 34 | |||
1372 | 35 | } | ||
1373 | 36 | |||
1374 | 24 | 37 | ||
1375 | 25 | bool WorkflowSoundness::verify(){ | 38 | bool WorkflowSoundness::verify(){ |
1376 | 26 | if(addToPW(&initialMarking, NULL)){ | 39 | if(addToPW(&initialMarking, NULL)){ |
1377 | @@ -50,6 +63,7 @@ | |||
1378 | 50 | return false; | 63 | return false; |
1379 | 51 | } | 64 | } |
1380 | 52 | } | 65 | } |
1381 | 66 | deleteMarking(next_marking); | ||
1382 | 53 | } | 67 | } |
1383 | 54 | 68 | ||
1384 | 55 | // Phase 2 | 69 | // Phase 2 |
1385 | @@ -82,6 +96,25 @@ | |||
1386 | 82 | return passed; | 96 | return passed; |
1387 | 83 | } | 97 | } |
1388 | 84 | 98 | ||
1389 | 99 | int WorkflowSoundnessPTrie::numberOfPassed() | ||
1390 | 100 | { | ||
1391 | 101 | int passed = 0; | ||
1392 | 102 | while(passedStack.size()){ | ||
1393 | 103 | WorkflowSoundnessMetaDataWithEncoding* next = | ||
1394 | 104 | static_cast<WorkflowSoundnessMetaDataWithEncoding*>(passedStack.top()); | ||
1395 | 105 | |||
1396 | 106 | passedStack.pop(); | ||
1397 | 107 | if(next->passed) continue; | ||
1398 | 108 | next->passed = true; | ||
1399 | 109 | ++passed; | ||
1400 | 110 | for(vector<MetaData*>::iterator iter = next->parents.begin(); | ||
1401 | 111 | iter != next->parents.end(); iter++){ | ||
1402 | 112 | passedStack.push(*iter); | ||
1403 | 113 | } | ||
1404 | 114 | } | ||
1405 | 115 | return passed; | ||
1406 | 116 | } | ||
1407 | 117 | |||
1408 | 85 | 118 | ||
1409 | 86 | bool WorkflowSoundness::addToPW(NonStrictMarking* marking, NonStrictMarking* parent){ | 119 | bool WorkflowSoundness::addToPW(NonStrictMarking* marking, NonStrictMarking* parent){ |
1410 | 87 | marking->cut(placeStats); | 120 | marking->cut(placeStats); |
1411 | @@ -91,7 +124,9 @@ | |||
1412 | 91 | // Check K-bound | 124 | // Check K-bound |
1413 | 92 | pwList->setMaxNumTokensIfGreater(size); | 125 | pwList->setMaxNumTokensIfGreater(size); |
1414 | 93 | if(modelType == ETAWFN && size > options.getKBound()) { | 126 | if(modelType == ETAWFN && size > options.getKBound()) { |
1416 | 94 | lastMarking = marking; | 127 | if(lastMarking != NULL) deleteMarking(lastMarking); |
1417 | 128 | lastMarking = marking; | ||
1418 | 129 | setMetaParent(lastMarking); | ||
1419 | 95 | return true; // Terminate false | 130 | return true; // Terminate false |
1420 | 96 | } | 131 | } |
1421 | 97 | 132 | ||
1422 | @@ -101,8 +136,6 @@ | |||
1423 | 101 | NonStrictMarking* old = pwList->addToPassed(marking, false); | 136 | NonStrictMarking* old = pwList->addToPassed(marking, false); |
1424 | 102 | if(old == NULL){ | 137 | if(old == NULL){ |
1425 | 103 | isNew = true; | 138 | isNew = true; |
1426 | 104 | marking->meta = new WorkflowSoundnessMetaData(); | ||
1427 | 105 | marking->setParent(parent); | ||
1428 | 106 | } else { | 139 | } else { |
1429 | 107 | delete marking; | 140 | delete marking; |
1430 | 108 | marking = old; | 141 | marking = old; |
1431 | @@ -130,11 +163,14 @@ | |||
1432 | 130 | marking->meta->totalDelay = min(marking->meta->totalDelay, parent->meta->totalDelay); // Transition | 163 | marking->meta->totalDelay = min(marking->meta->totalDelay, parent->meta->totalDelay); // Transition |
1433 | 131 | // keep track of shortest trace | 164 | // keep track of shortest trace |
1434 | 132 | if (marking->meta->totalDelay < minExec) { | 165 | if (marking->meta->totalDelay < minExec) { |
1435 | 166 | if(lastMarking != NULL) deleteMarking(lastMarking); | ||
1436 | 167 | |||
1437 | 133 | minExec = marking->meta->totalDelay; | 168 | minExec = marking->meta->totalDelay; |
1438 | 134 | lastMarking = marking; | 169 | lastMarking = marking; |
1439 | 135 | return false; | 170 | return false; |
1440 | 136 | } | 171 | } |
1441 | 137 | }else{ | 172 | }else{ |
1442 | 173 | if(lastMarking != NULL) deleteMarking(lastMarking); | ||
1443 | 138 | lastMarking = marking; | 174 | lastMarking = marking; |
1444 | 139 | return true; // Terminate false | 175 | return true; // Terminate false |
1445 | 140 | } | 176 | } |
1446 | @@ -143,15 +179,18 @@ | |||
1447 | 143 | if(isNew){ | 179 | if(isNew){ |
1448 | 144 | pwList->addLastToWaiting(); | 180 | pwList->addLastToWaiting(); |
1449 | 145 | if(parent != NULL && marking->canDeadlock(tapn, 0)){ | 181 | if(parent != NULL && marking->canDeadlock(tapn, 0)){ |
1450 | 182 | if(lastMarking != NULL) deleteMarking(lastMarking); | ||
1451 | 146 | lastMarking = marking; | 183 | lastMarking = marking; |
1452 | 147 | return true; | 184 | return true; |
1453 | 148 | } | 185 | } |
1454 | 149 | if(modelType == MTAWFN && checkForCoveredMarking(marking)){ | 186 | if(modelType == MTAWFN && checkForCoveredMarking(marking)){ |
1456 | 150 | lastMarking = marking; | 187 | if(lastMarking != NULL) deleteMarking(lastMarking); |
1457 | 188 | lastMarking = marking; | ||
1458 | 151 | return true; // Terminate false | 189 | return true; // Terminate false |
1459 | 152 | } | 190 | } |
1460 | 153 | } | 191 | } |
1461 | 154 | } | 192 | } |
1462 | 193 | deleteMarking(marking); | ||
1463 | 155 | return false; | 194 | return false; |
1464 | 156 | } | 195 | } |
1465 | 157 | 196 | ||
1466 | @@ -162,6 +201,14 @@ | |||
1467 | 162 | 201 | ||
1468 | 163 | } | 202 | } |
1469 | 164 | 203 | ||
1470 | 204 | void WorkflowSoundnessPTrie::addParentMeta(MetaData* meta, MetaData* parent) | ||
1471 | 205 | { | ||
1472 | 206 | assert(meta != NULL); | ||
1473 | 207 | assert(parent != NULL); | ||
1474 | 208 | WorkflowSoundnessMetaDataWithEncoding* markingmeta = ((WorkflowSoundnessMetaDataWithEncoding*)meta); | ||
1475 | 209 | markingmeta->parents.push_back(parent); | ||
1476 | 210 | |||
1477 | 211 | } | ||
1478 | 165 | 212 | ||
1479 | 166 | bool WorkflowSoundness::checkForCoveredMarking(NonStrictMarking* marking){ | 213 | bool WorkflowSoundness::checkForCoveredMarking(NonStrictMarking* marking){ |
1480 | 167 | if(marking->size() <= options.getKBound()){ | 214 | if(marking->size() <= options.getKBound()){ |
1481 | @@ -193,6 +240,64 @@ | |||
1482 | 193 | } | 240 | } |
1483 | 194 | 241 | ||
1484 | 195 | 242 | ||
1485 | 243 | void WorkflowSoundnessPTrie::getTrace(NonStrictMarking* marking){ | ||
1486 | 244 | |||
1487 | 245 | PWListHybrid* pwhlist = dynamic_cast<PWListHybrid*>(this->pwList); | ||
1488 | 246 | |||
1489 | 247 | stack < NonStrictMarking*> printStack; | ||
1490 | 248 | |||
1491 | 249 | if(marking != NULL){ | ||
1492 | 250 | printStack.push(marking); | ||
1493 | 251 | |||
1494 | 252 | MetaDataWithTraceAndEncoding* meta = | ||
1495 | 253 | static_cast<MetaDataWithTraceAndEncoding*>(marking->meta); | ||
1496 | 254 | if(meta) | ||
1497 | 255 | { | ||
1498 | 256 | marking->setGeneratedBy(meta->generatedBy); | ||
1499 | 257 | |||
1500 | 258 | meta = meta->parent; | ||
1501 | 259 | while(meta != NULL) | ||
1502 | 260 | { | ||
1503 | 261 | NonStrictMarking* next = pwhlist->decode(meta->ep); | ||
1504 | 262 | printStack.push(next); | ||
1505 | 263 | next->setGeneratedBy(meta->generatedBy); | ||
1506 | 264 | printStack.top()->setParent(next); | ||
1507 | 265 | meta = meta->parent; | ||
1508 | 266 | } | ||
1509 | 267 | } | ||
1510 | 268 | printStack.top()->setGeneratedBy(NULL); | ||
1511 | 269 | } | ||
1512 | 270 | |||
1513 | 271 | #ifdef CLEANUP | ||
1514 | 272 | stack < NonStrictMarking*> clearStack = printStack; | ||
1515 | 273 | #endif | ||
1516 | 274 | printXMLTrace(marking, printStack, query, tapn); | ||
1517 | 275 | #ifdef CLEANUP | ||
1518 | 276 | while(!clearStack.empty()) | ||
1519 | 277 | { | ||
1520 | 278 | if(clearStack.top() == lastMarking) break; // deleted elsewhere | ||
1521 | 279 | delete clearStack.top(); | ||
1522 | 280 | clearStack.pop(); | ||
1523 | 281 | } | ||
1524 | 282 | #endif | ||
1525 | 283 | } | ||
1526 | 284 | |||
1527 | 285 | |||
1528 | 286 | void WorkflowSoundnessPTrie::setMetaParent(NonStrictMarking* marking){ | ||
1529 | 287 | PWListHybrid* pwhlist = dynamic_cast<PWListHybrid*>(this->pwList); | ||
1530 | 288 | |||
1531 | 289 | if(marking->meta == NULL) | ||
1532 | 290 | { | ||
1533 | 291 | marking->meta = new MetaDataWithTraceAndEncoding(); | ||
1534 | 292 | } | ||
1535 | 293 | |||
1536 | 294 | MetaDataWithTraceAndEncoding* mte = | ||
1537 | 295 | static_cast<MetaDataWithTraceAndEncoding*>(marking->meta); | ||
1538 | 296 | mte->parent = pwhlist->parent; | ||
1539 | 297 | mte->generatedBy = marking->getGeneratedBy(); | ||
1540 | 298 | } | ||
1541 | 299 | |||
1542 | 300 | |||
1543 | 196 | 301 | ||
1544 | 197 | WorkflowSoundness::ModelType WorkflowSoundness::calculateModelType() { | 302 | WorkflowSoundness::ModelType WorkflowSoundness::calculateModelType() { |
1545 | 198 | bool isin, isout; | 303 | bool isin, isout; |
1546 | 199 | 304 | ||
1547 | === modified file 'src/DiscreteVerification/VerificationTypes/WorkflowSoundness.hpp' | |||
1548 | --- src/DiscreteVerification/VerificationTypes/WorkflowSoundness.hpp 2015-06-22 22:10:16 +0000 | |||
1549 | +++ src/DiscreteVerification/VerificationTypes/WorkflowSoundness.hpp 2015-08-20 13:27:24 +0000 | |||
1550 | @@ -26,6 +26,7 @@ | |||
1551 | 26 | #include "../DataStructures/WaitingList.hpp" | 26 | #include "../DataStructures/WaitingList.hpp" |
1552 | 27 | #include "Workflow.hpp" | 27 | #include "Workflow.hpp" |
1553 | 28 | 28 | ||
1554 | 29 | using namespace ptrie; | ||
1555 | 29 | namespace VerifyTAPN { | 30 | namespace VerifyTAPN { |
1556 | 30 | namespace DiscreteVerification { | 31 | namespace DiscreteVerification { |
1557 | 31 | 32 | ||
1558 | @@ -71,6 +72,23 @@ | |||
1559 | 71 | 72 | ||
1560 | 72 | }; | 73 | }; |
1561 | 73 | 74 | ||
1562 | 75 | |||
1563 | 76 | class WorkflowSoundnessPTrie : public WorkflowSoundness | ||
1564 | 77 | { | ||
1565 | 78 | public: | ||
1566 | 79 | WorkflowSoundnessPTrie(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options, WaitingList<ptriepointer_t<MetaData*> >* waiting_list); | ||
1567 | 80 | |||
1568 | 81 | virtual void addParentMeta(MetaData* meta, MetaData* parent); | ||
1569 | 82 | virtual int numberOfPassed(); | ||
1570 | 83 | virtual void deleteMarking(NonStrictMarking* marking) | ||
1571 | 84 | { | ||
1572 | 85 | delete marking; | ||
1573 | 86 | } | ||
1574 | 87 | virtual void getTrace(NonStrictMarking* marking); | ||
1575 | 88 | protected: | ||
1576 | 89 | virtual void setMetaParent(NonStrictMarking*); | ||
1577 | 90 | }; | ||
1578 | 91 | |||
1579 | 74 | } /* namespace DiscreteVerification */ | 92 | } /* namespace DiscreteVerification */ |
1580 | 75 | } /* namespace VerifyTAPN */ | 93 | } /* namespace VerifyTAPN */ |
1581 | 76 | #endif /* NONSTRICTSEARCH_HPP_ */ | 94 | #endif /* NONSTRICTSEARCH_HPP_ */ |
1582 | 77 | 95 | ||
1583 | === modified file 'src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.cpp' | |||
1584 | --- src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.cpp 2015-06-22 22:10:16 +0000 | |||
1585 | +++ src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.cpp 2015-08-20 13:27:24 +0000 | |||
1586 | @@ -16,6 +16,10 @@ | |||
1587 | 16 | findInOut(); | 16 | findInOut(); |
1588 | 17 | }; | 17 | }; |
1589 | 18 | 18 | ||
1590 | 19 | WorkflowStrongSoundnessReachability::WorkflowStrongSoundnessReachability(TAPN::TimedArcPetriNet& tapn, NonStrictMarking& initialMarking, AST::Query* query, VerificationOptions options) | ||
1591 | 20 | : Workflow(tapn, initialMarking, query, options), maxValue(-1), outPlace(NULL){ | ||
1592 | 21 | findInOut(); | ||
1593 | 22 | }; | ||
1594 | 19 | 23 | ||
1595 | 20 | void WorkflowStrongSoundnessReachability::findInOut() | 24 | void WorkflowStrongSoundnessReachability::findInOut() |
1596 | 21 | { | 25 | { |
1597 | @@ -25,8 +29,27 @@ | |||
1598 | 25 | break; | 29 | break; |
1599 | 26 | } | 30 | } |
1600 | 27 | } | 31 | } |
1603 | 28 | }; | 32 | } |
1604 | 29 | 33 | ||
1605 | 34 | WorkflowStrongSoundnessPTrie::WorkflowStrongSoundnessPTrie( | ||
1606 | 35 | TAPN::TimedArcPetriNet& tapn, | ||
1607 | 36 | NonStrictMarking& initialMarking, | ||
1608 | 37 | AST::Query* query, | ||
1609 | 38 | VerificationOptions options, | ||
1610 | 39 | WaitingList<ptriepointer_t<MetaData*> >* waiting_list) : | ||
1611 | 40 | WorkflowStrongSoundnessReachability( | ||
1612 | 41 | tapn, | ||
1613 | 42 | initialMarking, | ||
1614 | 43 | query, | ||
1615 | 44 | options) | ||
1616 | 45 | { | ||
1617 | 46 | pwList = new WorkflowPWListHybrid( tapn, | ||
1618 | 47 | waiting_list, | ||
1619 | 48 | options.getKBound(), | ||
1620 | 49 | tapn.getNumberOfPlaces(), | ||
1621 | 50 | tapn.getMaxConstant()); | ||
1622 | 51 | } | ||
1623 | 52 | |||
1624 | 30 | bool WorkflowStrongSoundnessReachability::verify() { | 53 | bool WorkflowStrongSoundnessReachability::verify() { |
1625 | 31 | 54 | ||
1626 | 32 | if (outPlace == NULL) | 55 | if (outPlace == NULL) |
1627 | @@ -53,6 +76,7 @@ | |||
1628 | 53 | bool noDelay = false; | 76 | bool noDelay = false; |
1629 | 54 | Result res = successorGenerator.generateAndInsertSuccessors(*next_marking); | 77 | Result res = successorGenerator.generateAndInsertSuccessors(*next_marking); |
1630 | 55 | if (res == ADDTOPW_RETURNED_TRUE) { | 78 | if (res == ADDTOPW_RETURNED_TRUE) { |
1631 | 79 | clearTrace(); | ||
1632 | 56 | return true; | 80 | return true; |
1633 | 57 | } else if (res == ADDTOPW_RETURNED_FALSE_URGENTENABLED) { | 81 | } else if (res == ADDTOPW_RETURNED_FALSE_URGENTENABLED) { |
1634 | 58 | noDelay = true; | 82 | noDelay = true; |
1635 | @@ -65,7 +89,7 @@ | |||
1636 | 65 | marking->setGeneratedBy(NULL); | 89 | marking->setGeneratedBy(NULL); |
1637 | 66 | 90 | ||
1638 | 67 | if (addToPW(marking, next_marking)) { | 91 | if (addToPW(marking, next_marking)) { |
1640 | 68 | 92 | clearTrace(); | |
1641 | 69 | lastMarking = marking; | 93 | lastMarking = marking; |
1642 | 70 | return true; | 94 | return true; |
1643 | 71 | } | 95 | } |
1644 | @@ -77,6 +101,7 @@ | |||
1645 | 77 | // remove childless markings from stack | 101 | // remove childless markings from stack |
1646 | 78 | while(!trace.empty() && trace.top()->getNumberOfChildren() <= 1){ | 102 | while(!trace.empty() && trace.top()->getNumberOfChildren() <= 1){ |
1647 | 79 | trace.top()->meta->inTrace = false; | 103 | trace.top()->meta->inTrace = false; |
1648 | 104 | deleteMarking(trace.top()); | ||
1649 | 80 | trace.pop(); | 105 | trace.pop(); |
1650 | 81 | } | 106 | } |
1651 | 82 | if(trace.empty()){ | 107 | if(trace.empty()){ |
1652 | @@ -108,6 +133,64 @@ | |||
1653 | 108 | printXMLTrace(lastMarking, printStack, query, tapn); | 133 | printXMLTrace(lastMarking, printStack, query, tapn); |
1654 | 109 | } | 134 | } |
1655 | 110 | 135 | ||
1656 | 136 | void WorkflowStrongSoundnessPTrie::getTrace() { | ||
1657 | 137 | |||
1658 | 138 | PWListHybrid* pwhlist = dynamic_cast<PWListHybrid*>(this->pwList); | ||
1659 | 139 | |||
1660 | 140 | std::stack < NonStrictMarking*> printStack; | ||
1661 | 141 | |||
1662 | 142 | NonStrictMarking* next = lastMarking; | ||
1663 | 143 | if(next != NULL) | ||
1664 | 144 | { | ||
1665 | 145 | |||
1666 | 146 | printStack.push(next); | ||
1667 | 147 | MetaDataWithTraceAndEncoding* meta = | ||
1668 | 148 | static_cast<MetaDataWithTraceAndEncoding*>(next->meta); | ||
1669 | 149 | |||
1670 | 150 | if(meta == NULL) | ||
1671 | 151 | { | ||
1672 | 152 | // We assume the parent was not deleted on return | ||
1673 | 153 | NonStrictMarking* parent = (NonStrictMarking*)lastMarking->getParent(); | ||
1674 | 154 | if(parent != NULL) meta = | ||
1675 | 155 | static_cast<MetaDataWithTraceAndEncoding*>(parent->meta); | ||
1676 | 156 | delete parent; | ||
1677 | 157 | } | ||
1678 | 158 | else | ||
1679 | 159 | { | ||
1680 | 160 | meta = meta->parent; | ||
1681 | 161 | } | ||
1682 | 162 | |||
1683 | 163 | while(meta != NULL) | ||
1684 | 164 | { | ||
1685 | 165 | next = pwhlist->decode(meta->ep); | ||
1686 | 166 | next->setGeneratedBy(meta->generatedBy); | ||
1687 | 167 | printStack.top()->setParent(next); | ||
1688 | 168 | printStack.push(next); | ||
1689 | 169 | meta = meta->parent; | ||
1690 | 170 | } | ||
1691 | 171 | } | ||
1692 | 172 | #ifdef CLEANUP | ||
1693 | 173 | std::stack < NonStrictMarking*> cleanup = printStack; | ||
1694 | 174 | #endif | ||
1695 | 175 | printXMLTrace(lastMarking, printStack, query, tapn); | ||
1696 | 176 | |||
1697 | 177 | #ifdef CLEANUP | ||
1698 | 178 | while(!cleanup.empty()) | ||
1699 | 179 | { | ||
1700 | 180 | if(cleanup.top() != lastMarking) // deleted elsewhere | ||
1701 | 181 | { | ||
1702 | 182 | delete cleanup.top(); | ||
1703 | 183 | cleanup.pop(); | ||
1704 | 184 | } | ||
1705 | 185 | else | ||
1706 | 186 | { | ||
1707 | 187 | break; | ||
1708 | 188 | } | ||
1709 | 189 | } | ||
1710 | 190 | #endif | ||
1711 | 191 | } | ||
1712 | 192 | |||
1713 | 193 | |||
1714 | 111 | bool WorkflowStrongSoundnessReachability::addToPW(NonStrictMarking* marking, NonStrictMarking* parent) { | 194 | bool WorkflowStrongSoundnessReachability::addToPW(NonStrictMarking* marking, NonStrictMarking* parent) { |
1715 | 112 | marking->cut(placeStats); | 195 | marking->cut(placeStats); |
1716 | 113 | marking->setParent(parent); | 196 | marking->setParent(parent); |
1717 | @@ -135,6 +218,7 @@ | |||
1718 | 135 | // make sure we can print trace | 218 | // make sure we can print trace |
1719 | 136 | marking->setNumberOfChildren(1); | 219 | marking->setNumberOfChildren(1); |
1720 | 137 | maxValue = totalDelay; | 220 | maxValue = totalDelay; |
1721 | 221 | deleteMarking(old); | ||
1722 | 138 | return true; | 222 | return true; |
1723 | 139 | } else { | 223 | } else { |
1724 | 140 | // search again to find maxdelay | 224 | // search again to find maxdelay |
1725 | @@ -145,12 +229,12 @@ | |||
1726 | 145 | // fall through on purpose | 229 | // fall through on purpose |
1727 | 146 | } | 230 | } |
1728 | 147 | } else { | 231 | } else { |
1729 | 232 | deleteMarking(old); | ||
1730 | 148 | delete marking; | 233 | delete marking; |
1731 | 149 | // already seen this maxage/marking combination | 234 | // already seen this maxage/marking combination |
1732 | 150 | return false; | 235 | return false; |
1733 | 151 | } | 236 | } |
1734 | 152 | } else { | 237 | } else { |
1735 | 153 | marking->meta = new MetaData(); | ||
1736 | 154 | marking->meta->totalDelay = totalDelay; | 238 | marking->meta->totalDelay = totalDelay; |
1737 | 155 | } | 239 | } |
1738 | 156 | 240 | ||
1739 | @@ -166,10 +250,14 @@ | |||
1740 | 166 | // if terminal, update max_value and last marking of trace | 250 | // if terminal, update max_value and last marking of trace |
1741 | 167 | if(maxValue < marking->meta->totalDelay) { | 251 | if(maxValue < marking->meta->totalDelay) { |
1742 | 168 | maxValue = marking->meta->totalDelay; | 252 | maxValue = marking->meta->totalDelay; |
1743 | 253 | if(lastMarking != NULL) deleteMarking(lastMarking); | ||
1744 | 169 | lastMarking = marking; | 254 | lastMarking = marking; |
1745 | 170 | return false; | 255 | return false; |
1746 | 171 | } | 256 | } |
1747 | 172 | } | 257 | } |
1748 | 258 | |||
1749 | 259 | deleteMarking(marking); | ||
1750 | 260 | |||
1751 | 173 | return false; | 261 | return false; |
1752 | 174 | } | 262 | } |
1753 | 175 | 263 | ||
1754 | @@ -179,5 +267,25 @@ | |||
1755 | 179 | old->setParent(marking->getParent()); | 267 | old->setParent(marking->getParent()); |
1756 | 180 | } | 268 | } |
1757 | 181 | 269 | ||
1758 | 270 | void WorkflowStrongSoundnessPTrie::swapData(NonStrictMarking* marking, NonStrictMarking* parent) | ||
1759 | 271 | { | ||
1760 | 272 | PWListHybrid* pwhlist = dynamic_cast<PWListHybrid*>(this->pwList); | ||
1761 | 273 | MetaDataWithTraceAndEncoding* meta = | ||
1762 | 274 | static_cast<MetaDataWithTraceAndEncoding*>(parent->meta); | ||
1763 | 275 | |||
1764 | 276 | meta->generatedBy = marking->getGeneratedBy(); | ||
1765 | 277 | meta->parent = pwhlist->parent; | ||
1766 | 278 | } | ||
1767 | 279 | |||
1768 | 280 | void WorkflowStrongSoundnessPTrie::clearTrace() | ||
1769 | 281 | { | ||
1770 | 282 | if(!trace.empty()) trace.pop(); // pop parent, used in getTrace | ||
1771 | 283 | while(!trace.empty()) | ||
1772 | 284 | { | ||
1773 | 285 | delete trace.top(); | ||
1774 | 286 | trace.pop(); | ||
1775 | 287 | } | ||
1776 | 288 | } | ||
1777 | 289 | |||
1778 | 182 | } /* namespace DiscreteVerification */ | 290 | } /* namespace DiscreteVerification */ |
1779 | 183 | } /* namespace VerifyTAPN */ | 291 | } /* namespace VerifyTAPN */ |
1780 | 184 | 292 | ||
1781 | === modified file 'src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.hpp' | |||
1782 | --- src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.hpp 2015-06-22 22:10:16 +0000 | |||
1783 | +++ src/DiscreteVerification/VerificationTypes/WorkflowStrongSoundness.hpp 2015-08-20 13:27:24 +0000 | |||
1784 | @@ -53,6 +53,26 @@ | |||
1785 | 53 | int validChildren; | 53 | int validChildren; |
1786 | 54 | }; | 54 | }; |
1787 | 55 | 55 | ||
1788 | 56 | class WorkflowStrongSoundnessPTrie : public WorkflowStrongSoundnessReachability | ||
1789 | 57 | { | ||
1790 | 58 | public: | ||
1791 | 59 | WorkflowStrongSoundnessPTrie( | ||
1792 | 60 | TAPN::TimedArcPetriNet& tapn, | ||
1793 | 61 | NonStrictMarking& initialMarking, | ||
1794 | 62 | AST::Query* query, | ||
1795 | 63 | VerificationOptions options, | ||
1796 | 64 | WaitingList<ptriepointer_t<MetaData*> >* waiting_list); | ||
1797 | 65 | virtual void getTrace(); | ||
1798 | 66 | virtual void deleteMarking(NonStrictMarking* marking) | ||
1799 | 67 | { | ||
1800 | 68 | delete marking; | ||
1801 | 69 | } | ||
1802 | 70 | |||
1803 | 71 | protected: | ||
1804 | 72 | virtual void swapData(NonStrictMarking* marking, NonStrictMarking* old); | ||
1805 | 73 | virtual void clearTrace(); | ||
1806 | 74 | }; | ||
1807 | 75 | |||
1808 | 56 | } /* namespace DiscreteVerification */ | 76 | } /* namespace DiscreteVerification */ |
1809 | 57 | } /* namespace VerifyTAPN */ | 77 | } /* namespace VerifyTAPN */ |
1810 | 58 | #endif /* NONSTRICTSEARCH_HPP_ */ | 78 | #endif /* NONSTRICTSEARCH_HPP_ */ |
Please, merge trunk to this branch and resolve the numerous conflicts.