Spin

Run-Time Options

Overview

NAME
spin - verification tool for models of distributed systems

SYNTAX
spin [options] file
spin -V

DESCRIPTION
Spin is a tool for analyzing the logical consistency of asynchronous systems, specifically distributed software and communication protocols. A verification model of the system is first specified in a guarded command language called Promela. This specification language, described in the reference, allows for the modeling of dynamic creation of asynchronous processes, nondeterministic case selection, loops, gotos, local and global variables. It also allows for a concise specification of logical correctness requirements, including, but not restricted to requirements expressed in linear temporal logic.

Given a Promela model stored in file , Spin can perform interactive, guided, or random simulations of the system's execution. It can also generate a C program that performs an exhaustive or approximate verification of the correctness requirements for the system.

Simulation Options

With only a filename as an argument and no option flags, Spin performs a random simulation of the model specified in the file (standard input is the default if the filename is omitted). This normally does not generate output, except what is generated explicitly by the user within the model with printf statements, and some details about the final state that is reached after the simulation completes. A first group of option flags can be used to set the desired level of information that the user wants to see in a random, guided, or interactive simulation run. Every line of output normally contains a reference to the source line in the specification that generated it. If option -i is added, the simulation is interactive, or if option -t is added, the simulation is guided.

• -B Suppresses the verbose printout at the end of a simulation run (giving process states etc.).
• -b Suppresses the execution of printf statements within the model (see also -T).
• -c Produce an ASCII approximation of a message sequence chart for a random or guided (when combined with -t) simulation run. See also option -M.
• -g Shows at each time step the current value of global variables (see also -w).
• -i Perform an interactive simulation, prompting the user at every execution step that requires a nondeterministic choice to be made. The simulation proceeds without user intervention when execution is deterministic.
• -jN Skip the first N steps of a random or guided simulation. (See also option -uN.)
• -l In combination with option -p, shows the current value of local variables of the process (see also -w).
• -M Produce a message sequence chart in Postscript form for a random simulation or a guided simulation (when combined with -t), for the model in file , and write the result into file.ps . See also option -c.
• -nN Set the seed for a random simulation to the integer value N. There is no space between the -n and the integer N. -p, shows the current value of local variables of the process.
• -p Shows at each simulation step which process changed state, and what source statement was executed.
• -qN In columnated output (option -c) and elsewhere, suppress the printing of output for send or receive operations on the channel numbered N.
• -r Shows all message-receive events, giving the name and number of the receiving process and the corresponding the source line number. For each message parameter, show the message type and the message channel number and name.
• -s Shows all message-send events.
• -T Suppress the default indentation of output from print statements. By default the output from process i is indented by i spaces. See also option -b.
• -t[N] Perform a guided simulation, following the error trail that was produces by an earlier verification run, see the online manuals for the details on verification. If an optional number is attached (no space between the number and the -t) the error trail with that sequence number is opened, instead of the default trail, without sequence number.
• -uN Stop a random or guided simulation after the first N steps. (See also option -jN.)
• -v Verbose mode, adds some more detail, and generates more hints and warnings about the model.
• -w Even more verbose output with options -l and -g (e.g., prints all variable values, not just those that change).

Generate, Compile, and Run

• -search Generate the verifier source code in pan.c (like -a does) and immediately compile and execute the verifier. Options that follow the -search argument are passed through to the compiler (options starting with -[ODUE] or to the verifier as runtime flags (all other options).
  Options to Spin itself, for parsing the Promela specification (e.g., macro definitions), should precede the -search argument.
  Options that can follow the -search argument include:

  	-bfs, -bfspar, -bcs, -ltl name, -safety, -noclaim, -bitstate, -hc, -collapse, -i, -l, -a

Verifier Generation Related

• -a Generate a verifier (model checker) for the specification. The output is written into a set of C files, named pan.[ cbhmt ] that can be compiled, (e.g., cc pan.c ) to produce an executable verifier. The online Spin manuals (see below) contain the details on compilation and use of the verifiers.
• -A Perform property-based slicing, warning the user of all statements and data objects that are likely to be redundant for the stated properties (i.e., in assertions and never claims).
• -d Produce symbol table information for the model specified in file . For each Promela object this information includes the type, name and number of elements (if declared as an array), the initial value (if a data object) or size (if a message channel), the scope (global or local), and whether the object is declared as a variable or as a parameter. For message channels, the data types of the message fields are listed. For structure variables, the 3rd field defines the name of the structure declaration that contains the variable.
• -F file This behaves identical to option -f but will read the formula from the file instead of from the command line. The file should contain the formula as the first line. Any text that follows this first line is ignored, so it can be used to store comments or annotation on the formula. (On some systems the quoting conventions of the shell complicate the use of option -f. Option -F is meant to solve those problems.)
• -f LTL Translate the LTL formula LTL into a never claim.
  This option reads a formula in LTL syntax from the second argument and translates it into Promela syntax (a never claim, qhich is Promela's equivalent of a Buchi Automaton). The LTL operators are written: [] (always), <> (eventually), and U (strong until). There is no X (next) operator, to secure compatibility with the partial order reduction rules that are applied during the verification process. If the formula contains spaces, it should be quoted to form a single argument to the Spin command. As the name suggests, a Spin never claim is used to specify behavior than is required to be impossible, i.e., behavior that would violate a user-specified property. This means that to check for compliance with an LTL formula, the formula must be negated explicitly before it is converted into a never claim. Negating an LTL formula is easy: just place the formula "f" in parentheses and negate it: "!(f)".
• -J Reverse the evaluation order of nested 'unless' statements (so that it conforms to the evaluation order of nested 'catch' statements in Java).
• -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.
• -N filename add the never claim stored in filename.
• -S1 and -S2 separate pan source for claim and model (see book for details).
• -V Prints the Spin version number and exits.

Optimization

• -o1 disable dataflow-optimizations in verifier. this marks variables as temporarily dead when they cannot be read before written. their value is then reset to zero, in an attempt to avoid redundant values in the state-vector. in rare cases, this option can increase complexity (by adding the zero value where it did not appear before).
• -o2 disable dead variables elimination in verifier (should never be necessary, other than to confirm its effect on the length of the state vector and reduction of memory requirements).
• -o3 disable statement merging in verifier. this option can make it harder to read the pan -d output (of the internal state machines used in the verifier). disabling it restores the old, more explicit, format, but loses the advantage of statement merging during model checking.
• -o4 enable rendez-vous optimizations (experimental). this attempts to precompute the feasibility of a rendez-vous operation, rather than letting the model checker determine this at run-time. we have been unable to see a positive effect on runtime when this option is enabled, so it is likely to disappear again.
• -o5 disable case caching (having this option enabled makes smarter use of the case-statements in the pan.m and pan.b files, and allows for faster compilation times; disable only when bugs are encountered).
• -o6 revert to the old rules for interpreting priority tags (pre version 6.2)
• -o7 revert to the old rules for semi-colon usage (pre version 6.3)

SEE ALSO

• Pan.html, Quick.html, GettingStarted.html, Roadmap.html, Manual.html, WhatsNew.html, Exercises.html

More background information on the system and the verification process, can be found in:

• G.J. Holzmann, The Spin Model Checker: Primer and Reference Manual, Addison-Wesley, 2003.
• --, Design and Validation of Computer Protocols, Prentice Hall, 1991.
• --, `The model checker Spin,' IEEE Trans. on SE, Vol, 23, No. 5, May 1997.