Get iSpin Full Featured

One needs to install some other software to use iSpin. Under Ubuntu, this can be easily done by Synaptics, but the package names are not so intuitive.

• Spin (follow this link), the main background program
• iSpin (interface), run iSpin/install.sh found in the Spin package
• Tcl/Tk (Synaptics > tcl), iSpin interface
• Dot (Synaptics > graphviz), for generating automata view
• Yacc (Synaptic > bison), for compilation

To generate the channel messages flowchart from .trail file (shown as msc.ps), one can use command

spin -M -t foo.pml

It is saved into foo.pml.ps.
For the flowchart directly built from model, it may be wise to specify it's depth when the model has an infinite behavior.

spin -u100 foo.pml

To generate the automata view in ps file:

./pan -D | dot > foo.dot
dot -Tps foo.dot -o foo.ps

See more here: The Dot Guide.