verif/Spin/Test/README.tests

   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