| 1 | -- Updated for SPIN Version 5.0 --- October 2007 --- |
| 2 | |
| 3 | Perform tests test0 to test5 in the order listed, and |
| 4 | make sure you get the same results. |
| 5 | The next four tests are to assess the effect of |
| 6 | partial order reductions. In exhaustive mode, they |
| 7 | may not all be executable within the bounds of your |
| 8 | system - with reduction turned on, though, they should |
| 9 | all run as specified. |
| 10 | The last test checks the use of execution priorities |
| 11 | during random simulations. |
| 12 | |
| 13 | The file called 'pathfinder' illustrates the use of |
| 14 | 'provided' clauses (using as inspiration the bug in |
| 15 | the control software of the Mars pathfinder that |
| 16 | spotted an otherwise perfect mission in July 1997) |
| 17 | |
| 18 | You can always check valid options of spin |
| 19 | by typing (at command prompt $): |
| 20 | $ spin -- |
| 21 | |
| 22 | Similarly, you can check valid options of |
| 23 | the compiled verifiers by typing: |
| 24 | $ pan -- |
| 25 | |
| 26 | test 0 check that spin exists, is executable, and is |
| 27 | the version that you expect |
| 28 | |
| 29 | $ spin -V |
| 30 | Spin Version 5.0 -- 26 October 2007 |
| 31 | |
| 32 | test 1 check that you can run a simulation |
| 33 | |
| 34 | $ spin hello |
| 35 | passed first test! |
| 36 | 1 process created |
| 37 | |
| 38 | or without the default indenting of output: |
| 39 | |
| 40 | $ spin -T hello |
| 41 | passed first test! |
| 42 | 1 process created |
| 43 | |
| 44 | test 2 a basic reachability check (safety) |
| 45 | |
| 46 | $ spin -a loops # generate c-verifier |
| 47 | $ cc -DNOREDUCE -o pan pan.c # no reduction (test) |
| 48 | $ ./pan # default run |
| 49 | hint: this search is more efficient if pan.c is compiled -DSAFETY |
| 50 | |
| 51 | (Spin Version 5.0 -- 26 October 2007) |
| 52 | |
| 53 | Full statespace search for: |
| 54 | never-claim - (none specified) |
| 55 | assertion violations + |
| 56 | acceptance cycles - (not selected) |
| 57 | invalid endstates + |
| 58 | |
| 59 | State-vector 12 byte, depth reached 11, errors: 0 |
| 60 | 15 states, stored |
| 61 | 4 states, matched |
| 62 | 19 transitions (= stored+matched) |
| 63 | 0 atomic steps |
| 64 | hash conflicts: 0 (resolved) |
| 65 | |
| 66 | 2.501 memory usage (Mbyte) |
| 67 | |
| 68 | unreached in proctype loop |
| 69 | line 12, state 12, "-end-" |
| 70 | (1 of 12 states) |
| 71 | |
| 72 | pan: elapsed time 0 seconds |
| 73 | |
| 74 | test 3 cycle detection check (liveness): |
| 75 | |
| 76 | $ ./pan -a # search for acceptance cycles |
| 77 | pan: acceptance cycle (at depth 0) |
| 78 | pan: wrote loops.trail |
| 79 | (Spin Version 5.0 -- 26 October 2007) |
| 80 | Warning: Search not completed |
| 81 | |
| 82 | Full statespace search for: |
| 83 | never-claim - (none specified) |
| 84 | assertion violations + |
| 85 | > acceptance cycles + (fairness disabled) |
| 86 | invalid endstates + |
| 87 | |
| 88 | State-vector 12 byte, depth reached 11, errors: 1 |
| 89 | 13 states, stored (15 visited) |
| 90 | 2 states, matched |
| 91 | 17 transitions (= visited+matched) |
| 92 | 0 atomic steps |
| 93 | hash conflicts: 0 (resolved) |
| 94 | |
| 95 | 2.501 memory usage (Mbyte) |
| 96 | |
| 97 | pan: elapsed time 0.015 seconds |
| 98 | pan: rate 1000 states/second |
| 99 | |
| 100 | test 4 guided simulation check (playback the error trail found in test 3) |
| 101 | |
| 102 | $ spin -t -p loops # guided simulation for the error-cycle |
| 103 | Starting loop with pid 0 |
| 104 | <<<<<START OF CYCLE>>>>> |
| 105 | 1: proc 0 (loop) line 5 "loops" (state 1) [a = ((a+1)%3)] |
| 106 | 2: proc 0 (loop) line 7 "loops" (state 2) [b = (2*a)] |
| 107 | 3: proc 0 (loop) line 7 "loops" (state 3) [(1)] |
| 108 | 4: proc 0 (loop) line 10 "loops" (state 8) [b = (b-1)] |
| 109 | 5: proc 0 (loop) line 5 "loops" (state 1) [a = ((a+1)%3)] |
| 110 | 6: proc 0 (loop) line 7 "loops" (state 2) [b = (2*a)] |
| 111 | 7: proc 0 (loop) line 7 "loops" (state 3) [(1)] |
| 112 | 8: proc 0 (loop) line 10 "loops" (state 8) [b = (b-1)] |
| 113 | 9: proc 0 (loop) line 5 "loops" (state 1) [a = ((a+1)%3)] |
| 114 | 10: proc 0 (loop) line 8 "loops" (state 4) [b = (2*a)] |
| 115 | 11: proc 0 (loop) line 8 "loops" (state 5) [(1)] |
| 116 | spin: line 10 "loops", Error: value (-1->255 (8)) truncated in assignment |
| 117 | 12: proc 0 (loop) line 10 "loops" (state 8) [b = (b-1)] |
| 118 | spin: trail ends after 12 steps |
| 119 | #processes: 1 |
| 120 | 12: proc 0 (loop) line 4 "loops" (state 9) |
| 121 | 1 process created |
| 122 | |
| 123 | test 5 try to find a cycle that avoids the progress labels (there are none) |
| 124 | |
| 125 | $ cc -DNP -DNOREDUCE -o pan pan.c # add support for non-progress |
| 126 | $ ./pan -l # search for non-progress cycles |
| 127 | |
| 128 | (Spin Version 5.0 -- 26 October 2007) |
| 129 | |
| 130 | Full statespace search for: |
| 131 | never claim + |
| 132 | assertion violations + (if within scope of claim) |
| 133 | non-progress cycles + (fairness disabled) |
| 134 | invalid end states - (disabled by never claim) |
| 135 | |
| 136 | State-vector 16 byte, depth reached 23, errors: 0 |
| 137 | 27 states, stored (39 visited) |
| 138 | 28 states, matched |
| 139 | 67 transitions (= visited+matched) |
| 140 | 0 atomic steps |
| 141 | hash conflicts: 0 (resolved) |
| 142 | |
| 143 | 2.501 memory usage (Mbyte) |
| 144 | |
| 145 | unreached in proctype loop |
| 146 | line 12, state 12, "-end-" |
| 147 | (1 of 12 states) |
| 148 | |
| 149 | pan: elapsed time 0 seconds |
| 150 | |
| 151 | test 6: check partial order reduction algorithm -- first disable it |
| 152 | |
| 153 | $ spin -a leader (or snoopy, pftp, sort) |
| 154 | $ cc -DSAFETY -DNOREDUCE -DNOCLAIM -o pan pan.c # safety only |
| 155 | $ ./pan -c0 -n # exhaustive, -c0 = ignore errors |
| 156 | (Spin Version 5.0 -- 26 October 2007) |
| 157 | |
| 158 | Full statespace search for: |
| 159 | never claim - (not selected) |
| 160 | assertion violations + |
| 161 | cycle checks - (disabled by -DSAFETY) |
| 162 | invalid end states + |
| 163 | |
| 164 | State-vector 196 byte, depth reached 108, errors: 0 |
| 165 | 15779 states, stored |
| 166 | 42402 states, matched |
| 167 | 58181 transitions (= stored+matched) |
| 168 | 12 atomic steps |
| 169 | hash conflicts: 440 (resolved) |
| 170 | |
| 171 | Stats on memory usage (in Megabytes): |
| 172 | 3.010 equivalent memory usage for states (stored*(State-vector + overhead)) |
| 173 | 2.731 actual memory usage for states (compression: 90.73%) |
| 174 | state-vector as stored = 177 byte + 4 byte overhead |
| 175 | 2.000 memory used for hash table (-w19) |
| 176 | 0.267 memory used for DFS stack (-m10000) |
| 177 | 0.094 memory lost to fragmentation |
| 178 | 4.904 total actual memory usage |
| 179 | |
| 180 | pan: elapsed time 0.125 seconds |
| 181 | pan: rate 126232 states/second |
| 182 | |
| 183 | test 6b: now leave p.o. reduction enabled (i.e., do not disable it) |
| 184 | |
| 185 | $ cc -DSAFETY -DNOCLAIM -o pan pan.c # safety only, reduced search |
| 186 | $ ./pan -c0 -n # -n = no dead code listing |
| 187 | |
| 188 | (Spin Version 5.0 -- 26 October 2007) |
| 189 | + Partial Order Reduction |
| 190 | |
| 191 | Full statespace search for: |
| 192 | never claim - (not selected) |
| 193 | assertion violations + |
| 194 | cycle checks - (disabled by -DSAFETY) |
| 195 | invalid end states + |
| 196 | |
| 197 | State-vector 196 byte, depth reached 108, errors: 0 |
| 198 | 97 states, stored |
| 199 | 0 states, matched |
| 200 | 97 transitions (= stored+matched) |
| 201 | 12 atomic steps |
| 202 | hash conflicts: 0 (resolved) |
| 203 | |
| 204 | 2.501 memory usage (Mbyte) |
| 205 | |
| 206 | pan: elapsed time 0 seconds |
| 207 | |
| 208 | If compiled as above, the results should match the results from the table below. |
| 209 | The numbers in the first two columns of the table should match precisely. |
| 210 | The numbers in the third column should match approximately (how well it matches |
| 211 | depends only on the properties of the C-compiler and the speed of the hardware |
| 212 | you use to run the tests.) |
| 213 | The first line for each test is for the exhaustive run, the second line is for |
| 214 | the default run using partial order reduction. |
| 215 | The times given are for a 2.4GHz dual-core Intel PC, with 2 GB of memory. |
| 216 | |
| 217 | States Stored Transitions Memory Used Time (s) |
| 218 | leader |
| 219 | S= 15779 T= 58181 M= 4.904 Mb t= 0.125 |
| 220 | S= 97 T= 97 M= 2.501 Mb t= <0.1 |
| 221 | |
| 222 | snoopy |
| 223 | S= 61619 T= 211398 M= 8.03 Mb t= 0.328 |
| 224 | S= 9343 T= 12706 M= 3.38 Mb t= 0.03 |
| 225 | |
| 226 | pftp |
| 227 | S= 144813 T= 397948 M= 18.97 Mb t= 0.79 |
| 228 | S= 47356 T= 64970 M= 8.07 Mb t= 0.14 |
| 229 | |
| 230 | sort |
| 231 | S= 107713 T= 512419 M= 18.87 Mb t= 1.08 |
| 232 | S= 135 T= 135 M= 2.50 Mb t= <0.1 |
| 233 | |
| 234 | |
| 235 | test 7 check random number generator |
| 236 | |
| 237 | $ spin -p -g -u10000 priorities # runs 10000 steps |
| 238 | .... |
| 239 | depth-limit (-u10000 steps) reached |
| 240 | #processes: 5 |
| 241 | a[0] = 0 |
| 242 | a[1] = 334 |
| 243 | a[2] = 677 |
| 244 | a[3] = 994 |
| 245 | a[4] = 1327 |
| 246 | 10000: proc 4 (A) line 11 "priorities" (state 3) |
| 247 | 10000: proc 3 (A) line 12 "priorities" (state 2) |
| 248 | 10000: proc 2 (A) line 14 "priorities" (state 4) |
| 249 | 10000: proc 1 (A) line 11 "priorities" (state 3) |
| 250 | 10000: proc 0 (:init:) line 22 "priorities" (state 6) <valid end state> |
| 251 | 5 processes created |
| 252 | |
| 253 | The numbers in the array should tend to the ratio |
| 254 | 1:2:3:4 if the random number generator works properly. |
| 255 | array index 0 remains unused (it's the pid of the init |
| 256 | process) |
| 257 | |
| 258 | test 8 test the generation of never claims from LTL formulae: |
| 259 | |
| 260 | $ spin -f "[] ( p U ( <> q ))" |
| 261 | |
| 262 | never { /* [] ( p U ( <> q )) */ |
| 263 | T0_init: |
| 264 | if |
| 265 | :: ((q)) -> goto accept_S9 |
| 266 | :: (1) -> goto T0_init |
| 267 | fi; |
| 268 | accept_S9: |
| 269 | if |
| 270 | :: (1) -> goto T0_init |
| 271 | fi; |
| 272 | } |
| 273 | |
| 274 | test 9 read a never claim from a file |
| 275 | |
| 276 | $ spin -a -N leader.ltl leader # the claim is in file leader.ltl |
| 277 | $ cc -o pan pan.c # the default compilation |
| 278 | $ ./pan -a # search for acceptance cycles |
| 279 | warning: for p.o. reduction to be valid the never claim must be stutter-invariant |
| 280 | (never claims generated from LTL formulae are stutter-invariant) |
| 281 | |
| 282 | (Spin Version 5.0 -- 26 October 2007) |
| 283 | + Partial Order Reduction |
| 284 | |
| 285 | Full statespace search for: |
| 286 | never claim + |
| 287 | assertion violations + (if within scope of claim) |
| 288 | acceptance cycles + (fairness disabled) |
| 289 | invalid end states - (disabled by never claim) |
| 290 | |
| 291 | State-vector 204 byte, depth reached 205, errors: 0 |
| 292 | 181 states, stored (360 visited) |
| 293 | 251 states, matched |
| 294 | 611 transitions (= visited+matched) |
| 295 | 24 atomic steps |
| 296 | hash conflicts: 0 (resolved) |
| 297 | |
| 298 | 2.501 memory usage (Mbyte) |
| 299 | |
| 300 | unreached in proctype node |
| 301 | line 53, state 28, "out!two,nr" |
| 302 | (1 of 49 states) |
| 303 | unreached in proctype :init: |
| 304 | (0 of 11 states) |
| 305 | |
| 306 | pan: elapsed time 0 seconds |
| 307 | |
| 308 | end of tests |