$ spin -c spec # simulation run, columnated output
$ spin -p spec # simulation run, process moves(Use "spin --" to see what other options are available at this point.)
$ spin -a spec # generate verifier
$ cc -o pan pan.c # default compilationor to decline partial order reduction (useful for tests only!) The reduction preserves correctness properties.
$ cc -DNOREDUCE -o pan pan.c # rarely usedIf you know an exact memory bound that you want to restrict verification runs to (e.g., to avoid paging), find the nearest power of 2 (e.g., 23 for the bound 223) and compile as follows.
$ cc -DMEMCNT=23 -o pan pan.c # memory bound 223 bytesIf the verification runs out of memory increase the memory bound or, if this is impossible, use compression:
$ cc -DMEMCNT=23 -DCOLLAPSE -o pan pan.c # memory bound 223If also this is insufficient, and exceeds the memory bounds, switch to supertrace.
$ cc -DBITSTATE -o pan pan.c # supertrace algorithmThis is typically used as the method of last resort when a full verication turns out to be infeasible because of memory limitations. It can also be used as a fast prescan of the problem, to get an early and quick indication of the presence or absence of errors.
$ pan -w23The argument defines the number of states you expect as a power of 2. Don't worry if you set the argument too low or too high: setting it too high merely wastes some memory, too low wastes some cpu-time, but both will complete correctly.
For a supertrace run (i.e., you compiled with -DBITSTATE), the hashtable is the memory arena, so set it to the maximum size of memory you can grab without making the system page (i.e., set it to the amount of real physical memory you can use). The -w argument should again equal at least the nearest power of 2 of the total number of reachable system states you expect. For instance, use 26 if you expect 8 million reachable states and can use 8 million bits of memory (i.e., 226 bits is 8 million bits, which requires 2 23 or 1 Megabyte of RAM).
It's also no problem her if you set the number too high or too low. Too low will not fully utilize available memory, and give you lower coverage than possible. Too high means asking for more memory than your system has available -- the system will complain.
For acceptance cycles use option -a:
$ pan -aFor non-progress cycles you must add the directive -DNP when compiling Spin. After that, you can use run-time option -l (Spin will warn you if you forget -DNP):
$ cc -DNP -o pan pan.c or: $ cc -DNP -DBITSTATE -o pan pan.c followed by: $ pan -lIf you don't use options -l or -a, only basic safety properties are checked (assertion violations, unreachable code, etc). In that case, you can obtain a faster verifier by compiling:
$ cc -DSAFETY -o pan pan.c or $ cc -DSAFETY -DBITSTATE -o pan pan.c
$ pan -m100000If you find a particularly nasty error that takes a large number of steps to hit, you may also set lower search depths to find the shortest variant of an error sequence.
$ pan -m40Or you can ask Spin to iterative home in on shorter versions of the error. In that case, add the compile time directive -DREACH when you compile pan.c, and use either the -i or the -I runtime flag:
$ cc -DREACH -o pan pan.c $ pan -m100000 -I # iterative search for short errors
If you find an error, any error, Spin dumps an error-trail into the file `spec.trail', where `spec' is the name of your PROMELA input. To inspect the trail, and examine the cause of the error, use a guided simulation with option -t:
$ spin -t -p specAdd as many extra or different options as you need to pin down the error. (You can check Spin's available options by typing: "spin --" .) One option is to convert the trail into a Postscript represetation of a message sequence chart of send and receive actions:
$ spin -t -M specOr a rough approximation of this in plain ASCII:
$ spin -t -c specFor more detailed tracebacks use, for instance:
$ spin -t -r -s -l -g specMake sure the file `spec' didn't change since you generated the verifier. (Spin will warn if you did.)
If you find non-progress cycles: add or delete progress labels and repeat the verifications until you're content that you found what you're looking for.
If you're not interested in the first error you see, use option -c to print others into the trail
$ pan -c3prints the third error into the trail. If you just want to count all errors and not see them, use
$ pan -c0By default, the argument is 1.
If you want to obtain a trail for each and every error, use:
$ pan -e -c0This creates a series of error trails in files numbers spec.trail, spec2.trail, spec3.trail, ...etc., where "spec" is the name of the file from which you created the verifier. To trace back a specific one of these trails, you must specify the appropriate number with the -t option:
$ pan -e -c0 ... $ spin -t6 -c spec
$ pan -d # print state machinesto print the optimized state machine assignments, as it is used during verification. The unoptimized machine (used during random or guided simulations with spin -t for instance) can also be printed, using:
$ pan -d -d # print full, unoptimized state machinesThese two options should also make it easier to understand and verify the working of Spin/pan in terms of automata theory.
When needed, you can also compile the verifier with -DCHECK, to get verbose printouts from the progress of the search itself.
Spin HomePage | (Page Updated: 17 August 1997) |