dc45444e |
1 | Exit-Status 0 |
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 |
6 | |
7 | (Spin Version 5.1.6 -- 9 May 2008) |
8 | + Partial Order Reduction |
9 | |
10 | Full statespace search for: |
11 | never claim + |
12 | assertion violations + (if within scope of claim) |
13 | acceptance cycles + (fairness disabled) |
14 | invalid end states - (disabled by never claim) |
15 | |
16 | State-vector 100 byte, depth reached 200, errors: 0 |
17 | 1295413 states, stored |
18 | 2540827 states, matched |
19 | 3836240 transitions (= stored+matched) |
20 | 4818193 atomic steps |
21 | hash conflicts: 1991528 (resolved) |
22 | |
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 |
30 | |
31 | unreached in proctype switcher |
32 | (0 of 31 states) |
33 | unreached in proctype tracer |
34 | (0 of 51 states) |
35 | unreached in proctype reader |
36 | (0 of 29 states) |
37 | unreached in proctype cleaner |
38 | (0 of 9 states) |
39 | unreached in proctype :init: |
40 | (0 of 43 states) |
41 | unreached in proctype :never: |
42 | line 306, "pan.___", state 8, "-end-" |
43 | (1 of 8 states) |
44 | |
45 | pan: elapsed time 10.3 seconds |
46 | pan: rate 125768.25 states/second |
47 | pan: avg transition delay 2.6849e-06 usec |
48 | Exit-Status 0 |
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 |
53 | |
54 | (Spin Version 5.1.6 -- 9 May 2008) |
55 | + Partial Order Reduction |
56 | |
57 | Full statespace search for: |
58 | never claim + |
59 | assertion violations + (if within scope of claim) |
60 | acceptance cycles + (fairness disabled) |
61 | invalid end states - (disabled by never claim) |
62 | |
63 | State-vector 100 byte, depth reached 200, errors: 0 |
64 | 1295413 states, stored |
65 | 2540827 states, matched |
66 | 3836240 transitions (= stored+matched) |
67 | 4818193 atomic steps |
68 | hash conflicts: 1991528 (resolved) |
69 | |
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 |
77 | |
78 | unreached in proctype switcher |
79 | (0 of 31 states) |
80 | unreached in proctype tracer |
81 | (0 of 51 states) |
82 | unreached in proctype reader |
83 | (0 of 29 states) |
84 | unreached in proctype cleaner |
85 | (0 of 9 states) |
86 | unreached in proctype :init: |
87 | (0 of 43 states) |
88 | unreached in proctype :never: |
89 | line 306, "pan.___", state 8, "-end-" |
90 | (1 of 8 states) |
91 | |
92 | pan: elapsed time 10.3 seconds |
93 | pan: rate 125890.48 states/second |
94 | pan: avg transition delay 2.6823e-06 usec |
95 | Exit-Status 0 |
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 |
102 | |
103 | (Spin Version 5.1.6 -- 9 May 2008) |
104 | Warning: Search not completed |
105 | + Partial Order Reduction |
106 | |
107 | Full statespace search for: |
108 | never claim + |
109 | assertion violations + (if within scope of claim) |
110 | acceptance cycles + (fairness disabled) |
111 | invalid end states - (disabled by never claim) |
112 | |
113 | State-vector 100 byte, depth reached 168, errors: 1 |
114 | 43 states, stored |
115 | 0 states, matched |
116 | 43 transitions (= stored+matched) |
117 | 83 atomic steps |
118 | hash conflicts: 0 (resolved) |
119 | |
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 |
127 | |
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)" |
140 | (8 of 31 states) |
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)" |
146 | (3 of 51 states) |
147 | unreached in proctype reader |
148 | line 201, "pan.___", state 12, "i = 0" |
149 | line 215, "pan.___", state 23, "i = 0" |
150 | (2 of 29 states) |
151 | unreached in proctype cleaner |
152 | (0 of 9 states) |
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))" |
158 | (2 of 43 states) |
159 | unreached in proctype :never: |
160 | line 306, "pan.___", state 7, "(!((events_lost!=0)))" |
161 | line 309, "pan.___", state 9, "-end-" |
162 | (2 of 9 states) |
163 | |
164 | pan: elapsed time 0 seconds |
165 | Exit-Status 0 |
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) |
170 | |
171 | (Spin Version 5.1.6 -- 9 May 2008) |
172 | + Partial Order Reduction |
173 | |
174 | Full statespace search for: |
175 | never claim + |
176 | assertion violations + (if within scope of claim) |
177 | acceptance cycles + (fairness disabled) |
178 | invalid end states - (disabled by never claim) |
179 | |
180 | State-vector 32 byte, depth reached 0, errors: 0 |
181 | 1 states, stored |
182 | 0 states, matched |
183 | 1 transitions (= stored+matched) |
184 | 0 atomic steps |
185 | hash conflicts: 0 (resolved) |
186 | |
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 |
194 | |
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-" |
210 | (11 of 31 states) |
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-" |
233 | (17 of 51 states) |
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-" |
244 | (8 of 29 states) |
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-" |
250 | (4 of 9 states) |
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-" |
265 | (10 of 43 states) |
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-" |
270 | (2 of 14 states) |
271 | |
272 | pan: elapsed time 0 seconds |