SPIN VERIFIER's ROADMAP:
BUILDING AND VERIFYING Spin MODELS

	$ spin -a spec		# generate verifier

Three

• Full verification. Compile as follows.

  
  	$ cc -o pan pan.c               # default compilation
  
  

  or to decline partial order reduction (useful for tests only!) The reduction preserves correctness properties.

  
  	$ cc -DNOREDUCE -o pan pan.c    # rarely used
  
  

  If 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 2²³) and compile as follows.

  
  	$ cc -DMEMCNT=23 -o pan pan.c   # memory bound 223 bytes
  
  

  If 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 223
  
  

  If also this is insufficient, and exceeds the memory bounds, switch to supertrace.
• Supertrace verification. Compile as follows.

  
  	$ cc -DBITSTATE -o pan pan.c    # supertrace algorithm
  
  

  This 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.

Four

• selecting a good size of the hashtable, which is in effect an estimate of the number of reachable states,
• selecting the type of property to be verified (safety or liveness properties),
• selecting the maximum search depth,
• selecting the parameters for an inspection of the error that is found, if so.

• For a full verification (i.e., if you compiled without the -DBITSTATE option), set the size of the hashtable with runtime option -w.

  
  	$ pan -w23
  
  

  The 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., 2²⁶ bits is 8 million bits, which requires 2 ²³ 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.

• The second runtime decision is to decide if you want to check the model for non-progress cycles (and only non-progress cycles), acceptance cycles (and only acceptance cycles), or safety properties.

  For acceptance cycles use option -a:

  
  	$ pan -a
  
  

  For 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 -l
  
  

  If 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
  
  

• The next decision has to do with the search depth. By default the verifiers have a search depth restriction of 10,000 steps. If this isn't enough, the search will truncate at 9,999 steps (watch for it in the printout). You can define a different searchdepth with the -m flag.

  
  	$ pan -m100000
  
  

  If 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 -m40
  
  

  Or 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
  
  

• You can now do a first verification run. If you see that any of the verification parameters you chose earlier was wrong (e.g., amount of memory available, or number of reachable states) adjust and repeat.

  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 spec
  
  

  Add 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 spec
  
  

  Or a rough approximation of this in plain ASCII:

  
  	$ spin -t -c spec
  
  

  For more detailed tracebacks use, for instance:

  
  	$ spin -t -r -s -l -g spec
  
  

  Make 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 -c3
  
  

  prints the third error into the trail. If you just want to count all errors and not see them, use

  
  	$ pan -c0
  
  

  By default, the argument is 1.

  If you want to obtain a trail for each and every error, use:

  
  	$ pan -e -c0
  
  

  This 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
  
  

And Finally

	$ pan -d	# print state machines

	$ pan -d -d	# print full, unoptimized state machines

When needed, you can also compile the verifier with -DCHECK, to get verbose printouts from the progress of the search itself.