1 -- Updated for SPIN Version 5.0 --- October 2007 ---
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
10 The last test checks the use of execution priorities
11 during random simulations.
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)
18 You can always check valid options of spin
19 by typing (at command prompt $):
22 Similarly, you can check valid options of
23 the compiled verifiers by typing:
26 test 0 check that spin exists, is executable, and is
27 the version that you expect
30 Spin Version 5.0 -- 26 October 2007
32 test 1 check that you can run a simulation
38 or without the default indenting of output:
44 test 2 a basic reachability check (safety)
46 $ spin -a loops # generate c-verifier
47 $ cc -DNOREDUCE -o pan pan.c # no reduction (test)
49 hint: this search is more efficient if pan.c is compiled -DSAFETY
51 (Spin Version 5.0 -- 26 October 2007)
53 Full statespace search for:
54 never-claim - (none specified)
55 assertion violations +
56 acceptance cycles - (not selected)
59 State-vector 12 byte, depth reached 11, errors: 0
62 19 transitions (= stored+matched)
64 hash conflicts: 0 (resolved)
66 2.501 memory usage (Mbyte)
68 unreached in proctype loop
69 line 12, state 12, "-end-"
72 pan: elapsed time 0 seconds
74 test 3 cycle detection check (liveness):
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
82 Full statespace search for:
83 never-claim - (none specified)
84 assertion violations +
85 > acceptance cycles + (fairness disabled)
88 State-vector 12 byte, depth reached 11, errors: 1
89 13 states, stored (15 visited)
91 17 transitions (= visited+matched)
93 hash conflicts: 0 (resolved)
95 2.501 memory usage (Mbyte)
97 pan: elapsed time 0.015 seconds
98 pan: rate 1000 states/second
100 test 4 guided simulation check (playback the error trail found in test 3)
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
120 12: proc 0 (loop) line 4 "loops" (state 9)
123 test 5 try to find a cycle that avoids the progress labels (there are none)
125 $ cc -DNP -DNOREDUCE -o pan pan.c # add support for non-progress
126 $ ./pan -l # search for non-progress cycles
128 (Spin Version 5.0 -- 26 October 2007)
130 Full statespace search for:
132 assertion violations + (if within scope of claim)
133 non-progress cycles + (fairness disabled)
134 invalid end states - (disabled by never claim)
136 State-vector 16 byte, depth reached 23, errors: 0
137 27 states, stored (39 visited)
139 67 transitions (= visited+matched)
141 hash conflicts: 0 (resolved)
143 2.501 memory usage (Mbyte)
145 unreached in proctype loop
146 line 12, state 12, "-end-"
149 pan: elapsed time 0 seconds
151 test 6: check partial order reduction algorithm -- first disable it
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)
158 Full statespace search for:
159 never claim - (not selected)
160 assertion violations +
161 cycle checks - (disabled by -DSAFETY)
164 State-vector 196 byte, depth reached 108, errors: 0
166 42402 states, matched
167 58181 transitions (= stored+matched)
169 hash conflicts: 440 (resolved)
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
180 pan: elapsed time 0.125 seconds
181 pan: rate 126232 states/second
183 test 6b: now leave p.o. reduction enabled (i.e., do not disable it)
185 $ cc -DSAFETY -DNOCLAIM -o pan pan.c # safety only, reduced search
186 $ ./pan -c0 -n # -n = no dead code listing
188 (Spin Version 5.0 -- 26 October 2007)
189 + Partial Order Reduction
191 Full statespace search for:
192 never claim - (not selected)
193 assertion violations +
194 cycle checks - (disabled by -DSAFETY)
197 State-vector 196 byte, depth reached 108, errors: 0
200 97 transitions (= stored+matched)
202 hash conflicts: 0 (resolved)
204 2.501 memory usage (Mbyte)
206 pan: elapsed time 0 seconds
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.
217 States Stored Transitions Memory Used Time (s)
219 S= 15779 T= 58181 M= 4.904 Mb t= 0.125
220 S= 97 T= 97 M= 2.501 Mb t= <0.1
223 S= 61619 T= 211398 M= 8.03 Mb t= 0.328
224 S= 9343 T= 12706 M= 3.38 Mb t= 0.03
227 S= 144813 T= 397948 M= 18.97 Mb t= 0.79
228 S= 47356 T= 64970 M= 8.07 Mb t= 0.14
231 S= 107713 T= 512419 M= 18.87 Mb t= 1.08
232 S= 135 T= 135 M= 2.50 Mb t= <0.1
235 test 7 check random number generator
237 $ spin -p -g -u10000 priorities # runs 10000 steps
239 depth-limit (-u10000 steps) reached
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>
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
258 test 8 test the generation of never claims from LTL formulae:
260 $ spin -f "[] ( p U ( <> q ))"
262 never { /* [] ( p U ( <> q )) */
265 :: ((q)) -> goto accept_S9
266 :: (1) -> goto T0_init
270 :: (1) -> goto T0_init
274 test 9 read a never claim from a file
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)
282 (Spin Version 5.0 -- 26 October 2007)
283 + Partial Order Reduction
285 Full statespace search for:
287 assertion violations + (if within scope of claim)
288 acceptance cycles + (fairness disabled)
289 invalid end states - (disabled by never claim)
291 State-vector 204 byte, depth reached 205, errors: 0
292 181 states, stored (360 visited)
294 611 transitions (= visited+matched)
296 hash conflicts: 0 (resolved)
298 2.501 memory usage (Mbyte)
300 unreached in proctype node
301 line 53, state 28, "out!two,nr"
303 unreached in proctype :init:
306 pan: elapsed time 0 seconds