2 warning: for p.o. reduction to be valid the never claim must be stutter-invariant
3 (never claims generated from LTL formulae are stutter-invariant)
4 depth 0: Claim reached state 5 (line 301)
5 Depth= 198 States= 1e+06 Transitions= 2.9e+06 Memory= 79.649 t= 7.71 R= 1e+05
7 (Spin Version 5.1.6 -- 9 May 2008)
8 + Partial Order Reduction
10 Full statespace search for:
12 assertion violations + (if within scope of claim)
13 acceptance cycles + (fairness disabled)
14 invalid end states - (disabled by never claim)
16 State-vector 100 byte, depth reached 200, errors: 0
17 1295413 states, stored
18 2540827 states, matched
19 3836240 transitions (= stored+matched)
21 hash conflicts: 1991528 (resolved)
23 Stats on memory usage (in Megabytes):
24 143.307 equivalent memory usage for states (stored*(State-vector + overhead))
25 100.700 actual memory usage for states (compression: 70.27%)
26 state-vector as stored = 66 byte + 16 byte overhead
27 2.000 memory used for hash table (-w19)
28 0.305 memory used for DFS stack (-m10000)
29 102.891 total actual memory usage
31 unreached in proctype switcher
33 unreached in proctype tracer
35 unreached in proctype reader
37 unreached in proctype cleaner
39 unreached in proctype :init:
41 unreached in proctype :never:
42 line 306, "pan.___", state 8, "-end-"
45 pan: elapsed time 10.3 seconds
46 pan: rate 125768.25 states/second
47 pan: avg transition delay 2.6849e-06 usec
49 warning: for p.o. reduction to be valid the never claim must be stutter-invariant
50 (never claims generated from LTL formulae are stutter-invariant)
51 depth 0: Claim reached state 5 (line 301)
52 Depth= 198 States= 1e+06 Transitions= 2.9e+06 Memory= 79.649 t= 7.7 R= 1e+05
54 (Spin Version 5.1.6 -- 9 May 2008)
55 + Partial Order Reduction
57 Full statespace search for:
59 assertion violations + (if within scope of claim)
60 acceptance cycles + (fairness disabled)
61 invalid end states - (disabled by never claim)
63 State-vector 100 byte, depth reached 200, errors: 0
64 1295413 states, stored
65 2540827 states, matched
66 3836240 transitions (= stored+matched)
68 hash conflicts: 1991528 (resolved)
70 Stats on memory usage (in Megabytes):
71 143.307 equivalent memory usage for states (stored*(State-vector + overhead))
72 100.700 actual memory usage for states (compression: 70.27%)
73 state-vector as stored = 66 byte + 16 byte overhead
74 2.000 memory used for hash table (-w19)
75 0.305 memory used for DFS stack (-m10000)
76 102.891 total actual memory usage
78 unreached in proctype switcher
80 unreached in proctype tracer
82 unreached in proctype reader
84 unreached in proctype cleaner
86 unreached in proctype :init:
88 unreached in proctype :never:
89 line 306, "pan.___", state 8, "-end-"
92 pan: elapsed time 10.3 seconds
93 pan: rate 125890.48 states/second
94 pan: avg transition delay 2.6823e-06 usec
96 warning: for p.o. reduction to be valid the never claim must be stutter-invariant
97 (never claims generated from LTL formulae are stutter-invariant)
98 depth 0: Claim reached state 3 (line 302)
99 depth 25: Claim reached state 7 (line 307)
100 pan: acceptance cycle (at depth 167)
101 pan: wrote model.spin.trail
103 (Spin Version 5.1.6 -- 9 May 2008)
104 Warning: Search not completed
105 + Partial Order Reduction
107 Full statespace search for:
109 assertion violations + (if within scope of claim)
110 acceptance cycles + (fairness disabled)
111 invalid end states - (disabled by never claim)
113 State-vector 100 byte, depth reached 168, errors: 1
116 43 transitions (= stored+matched)
118 hash conflicts: 0 (resolved)
120 Stats on memory usage (in Megabytes):
121 0.005 equivalent memory usage for states (stored*(State-vector + overhead))
122 0.277 actual memory usage for states (unsuccessful compression: 5822.98%)
123 state-vector as stored = 6739 byte + 16 byte overhead
124 2.000 memory used for hash table (-w19)
125 0.305 memory used for DFS stack (-m10000)
126 2.501 total actual memory usage
128 unreached in proctype switcher
129 line 80, "pan.___", state 8, "(1)"
130 line 75, "pan.___", state 9, "(((((new_off-read_off)>4)&&((new_off-read_off)<(255/2)))||(size==(4/2))))"
131 line 75, "pan.___", state 9, "else"
132 line 86, "pan.___", state 15, "write_off = new_off"
133 line 83, "pan.___", state 18, "((prev_off!=write_off))"
134 line 83, "pan.___", state 18, "else"
135 line 96, "pan.___", state 21, "commit_count[((prev_off%4)/(4/2))] = tmp_commit"
136 line 102, "pan.___", state 25, "(1)"
137 line 97, "pan.___", state 26, "((((((prev_off/4)*4)/2)+(4/2))-tmp_commit))"
138 line 97, "pan.___", state 26, "else"
139 line 90, "pan.___", state 29, "tmp_commit = (commit_count[((prev_off%4)/(4/2))]+size)"
141 unreached in proctype tracer
142 line 153, "pan.___", state 34, "((i<size))"
143 line 153, "pan.___", state 34, "((i>=size))"
144 line 151, "pan.___", state 46, "i = 0"
145 line 176, "pan.___", state 48, "events_lost = (events_lost+1)"
147 unreached in proctype reader
148 line 201, "pan.___", state 12, "i = 0"
149 line 215, "pan.___", state 23, "i = 0"
151 unreached in proctype cleaner
153 unreached in proctype :init:
154 line 253, "pan.___", state 7, "((i<2))"
155 line 253, "pan.___", state 7, "((i>=2))"
156 line 272, "pan.___", state 29, "((i<4))"
157 line 272, "pan.___", state 29, "((i>=4))"
159 unreached in proctype :never:
160 line 306, "pan.___", state 7, "(!((events_lost!=0)))"
161 line 309, "pan.___", state 9, "-end-"
164 pan: elapsed time 0 seconds
166 warning: for p.o. reduction to be valid the never claim must be stutter-invariant
167 (never claims generated from LTL formulae are stutter-invariant)
168 depth 0: Claim reached state 5 (line 301)
169 depth 0: Claim reached state 5 (line 302)
171 (Spin Version 5.1.6 -- 9 May 2008)
172 + Partial Order Reduction
174 Full statespace search for:
176 assertion violations + (if within scope of claim)
177 acceptance cycles + (fairness disabled)
178 invalid end states - (disabled by never claim)
180 State-vector 32 byte, depth reached 0, errors: 0
183 1 transitions (= stored+matched)
185 hash conflicts: 0 (resolved)
187 Stats on memory usage (in Megabytes):
188 0.000 equivalent memory usage for states (stored*(State-vector + overhead))
189 0.277 actual memory usage for states (unsuccessful compression: 604850.00%)
190 state-vector as stored = 290312 byte + 16 byte overhead
191 2.000 memory used for hash table (-w19)
192 0.305 memory used for DFS stack (-m10000)
193 2.501 total actual memory usage
195 unreached in proctype switcher
196 line 74, "pan.___", state 3, "new_off = (prev_off+size)"
197 line 80, "pan.___", state 8, "(1)"
198 line 75, "pan.___", state 9, "(((((new_off-read_off)>4)&&((new_off-read_off)<(255/2)))||(size==(4/2))))"
199 line 75, "pan.___", state 9, "else"
200 line 71, "pan.___", state 11, "prev_off = write_off"
201 line 86, "pan.___", state 15, "write_off = new_off"
202 line 83, "pan.___", state 18, "((prev_off!=write_off))"
203 line 83, "pan.___", state 18, "else"
204 line 96, "pan.___", state 21, "commit_count[((prev_off%4)/(4/2))] = tmp_commit"
205 line 102, "pan.___", state 25, "(1)"
206 line 97, "pan.___", state 26, "((((((prev_off/4)*4)/2)+(4/2))-tmp_commit))"
207 line 97, "pan.___", state 26, "else"
208 line 90, "pan.___", state 29, "tmp_commit = (commit_count[((prev_off%4)/(4/2))]+size)"
209 line 108, "pan.___", state 31, "-end-"
211 unreached in proctype tracer
212 line 122, "pan.___", state 3, "prev_off = write_off"
213 line 130, "pan.___", state 7, "(1)"
214 line 126, "pan.___", state 10, "((((new_off-read_off)>4)&&((new_off-read_off)<(255/2))))"
215 line 126, "pan.___", state 10, "else"
216 line 136, "pan.___", state 14, "write_off = new_off"
217 line 142, "pan.___", state 20, "buffer_use[((prev_off+i)%4)] = 1"
218 line 143, "pan.___", state 21, "i = (i+1)"
219 line 133, "pan.___", state 27, "((prev_off!=write_off))"
220 line 133, "pan.___", state 27, "else"
221 line 156, "pan.___", state 31, "i = (i+1)"
222 line 153, "pan.___", state 34, "((i<size))"
223 line 153, "pan.___", state 34, "((i>=size))"
224 line 164, "pan.___", state 39, "commit_count[((prev_off%4)/(4/2))] = tmp_commit"
225 line 170, "pan.___", state 43, "(1)"
226 line 165, "pan.___", state 44, "((((((prev_off/4)*4)/2)+(4/2))-tmp_commit))"
227 line 165, "pan.___", state 44, "else"
228 line 151, "pan.___", state 46, "i = 0"
229 line 176, "pan.___", state 48, "events_lost = (events_lost+1)"
230 line 178, "pan.___", state 49, "refcount = (refcount-1)"
231 line 173, "pan.___", state 50, "goto end"
232 line 180, "pan.___", state 51, "-end-"
234 unreached in proctype reader
235 line 206, "pan.___", state 5, "buffer_use[((read_off+i)%4)] = 1"
236 line 207, "pan.___", state 6, "i = (i+1)"
237 line 201, "pan.___", state 12, "i = 0"
238 line 220, "pan.___", state 16, "i = (i+1)"
239 line 223, "pan.___", state 22, "read_off = (read_off+(4/2))"
240 line 215, "pan.___", state 23, "i = 0"
241 line 195, "pan.___", state 26, "((((((write_off/(4/2))-(read_off/(4/2)))>0)&&(((write_off/(4/2))-(read_off/(4/2)))<(255/2)))&&(((commit_count[((read_off%4)/(4/2))]-(4/2))-(((read_off/4)*4)/2))==0)))"
242 line 195, "pan.___", state 26, "((read_off>=(4-events_lost)))"
243 line 227, "pan.___", state 29, "-end-"
245 unreached in proctype cleaner
246 line 239, "pan.___", state 3, "(run switcher())"
247 line 236, "pan.___", state 5, "((refcount==0))"
248 line 235, "pan.___", state 8, "((refcount==0))"
249 line 243, "pan.___", state 9, "-end-"
251 unreached in proctype :init:
252 line 256, "pan.___", state 4, "i = (i+1)"
253 line 253, "pan.___", state 7, "((i<2))"
254 line 253, "pan.___", state 7, "((i>=2))"
255 line 266, "pan.___", state 14, "i = (i+1)"
256 line 263, "pan.___", state 17, "((i<4))"
257 line 263, "pan.___", state 17, "((i>=4))"
258 line 269, "pan.___", state 20, "(run reader())"
259 line 270, "pan.___", state 21, "(run cleaner())"
260 line 275, "pan.___", state 25, "(run tracer())"
261 line 272, "pan.___", state 29, "((i<4))"
262 line 272, "pan.___", state 29, "((i>=4))"
263 line 283, "pan.___", state 35, "(run switcher())"
264 line 288, "pan.___", state 43, "-end-"
266 unreached in proctype :never:
267 line 305, "pan.___", state 11, "((events_lost!=0))"
268 line 305, "pan.___", state 11, "(1)"
269 line 311, "pan.___", state 14, "-end-"
272 pan: elapsed time 0 seconds