How to Use SPIN Model Checker

spin.md

How to Use SPIN

Run Verifier

It's possible to use spin -a src.pml to create pan.[cbhmt] files. Then, it's possible to compile the generated verifier using gcc -o pan pan.c. The compiler verifier could be run by ./pan. spin -run src.pml automates the whole process.

Rerun After Failure

If the execution is stopped because of assertion failure or any other reason, a scr.pml.trail file is generated. By spin -t src.pml, the aforementioned trail is rerun.

Verbose Run

Running spin with some options generates more verbose details:

• -p Shows the state changes of the Promela processes at every time step.
• -g Shows the current value of global variables at every time step.
• -l Shows the current value of local variables, after the process that owns them has changed state. It is best used in combination with option -p.
• -r Shows all message receive events. It shows the process performing the receive, its name and number, the source line number, the message parameter number (there is one line for each parameter), the message type and the message channel number and name.
• -s Shows all message send events.
• -c columnated -s -r simulation output

You may consider using -m option, too:

• -m Changes the semantics of send events. Ordinarily, a send action will be (blocked) if the target message buffer is full. With this option a message sent to a full buffer is lost.

Visualize

By using -M flag, spin generates msc-flow in tcl/tk format.

You may want to add the following lines to the end of src.pml.tcl file, and rerun wish src.pml.tcl:

update;
.c postscript -height 60000 -file ./src.ps

Use large enough values (see last lines of tcl file) for -height option (and maybe -width option, too), or use appropriate values for -height, -width, -x, and -y options to control which part of canvas should be printed. Use ps2pdf -dEPSCrop src.ps to convert postscript to pdf.

Interactive Run

Running spin with -i option make it possible to select the execution path interactively.

Generate Program Graph

Using ./pan -d it's possible to print state tables.

Using ./pan -D it's possible to generate a graphviz dot compatible version of state tables. By saving one state table in a file like state-table.dot, and running dot -Tpng -Gdpi=300 state-table.dot -o state-table.png, it's possible to visualize state table.

Apply Redundancy and Syntax Check

Running spin -A src.pml invokes a redundancy and syntax check process.