| 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 |
projects / lttv.git / blame