0b55f123 |
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 |