Unix/Linux Go Back    

Plan 9 - man page for spin (plan9 section 1)

Linux & Unix Commands - Search Man Pages
Man Page or Keyword Search:   man
Select Man Page Set:       apropos Keyword Search (sections above)

SPIN(1) 										  SPIN(1)

       spin - verification tool for concurrent systems

       spin [ -nN ] [ -plgrsmv ] [ -iat ] [ -DV ] [ file ]

       Spin  is  a tool for analyzing the logical consistency of concurrent systems, specifically
       communication protocols.  The system is specified in a  guarded	command  language  called
       PROMELA2.   The	language, described in the references, allows for the dynamic creation of
       processes, nondeterministic case selection, loops, gotos, variables, and the specification
       of  correctness	requirements.  The tool has fast algorithms for analyzing arbitrary live-
       ness and safety conditions.

       Given a model system specified in PROMELA2, spin can perform interactive, guided, or  ran-
       dom  simulations of the system's execution or it can generate a C program that performs an
       exhaustive or approximate verification  of  the	system.   The  verifier  can  check,  for
       instance,  if user specified system invariants are violated during a protocol's execution,
       or if non-progress execution cycles exist.

       Without any options the program performs a random simulation of the system defined in  the
       input  file,  default  standard input.  The option -nN sets the random seed to the integer
       value N.

       The group of options -pglmrsv is used to set the level of information reported  about  the
       simulation  run.  Every line of output normally contains a reference to the source line in
       the specification that caused it.

       p      Show at each time step which process changed state and what  source  statement  was

       l      In  combination  with  option  p,  show the current value of local variables of the

       g      Show the value of global variables at each time step.

       r      Show all message-receive events, giving  the  name  and  number  of  the	receiving
	      process and the corresponding source line number.  For each message parameter, show
	      the message type and the message channel number and name.

       s      Show all message-send events.

       m      Ordinarily, a send action will be delayed if the target  message	buffer	if  full.
	      With  this  option a message sent to a full buffer is lost.  The option can be com-
	      bined with -a (see below).

       v      Verbose mode: add extra detail and include more warnings.

       i      Perform an interactive simulation.

       a      Generate a protocol-specific verifier.  The output is  written  into  a  set  of	C
	      files,  named pan.[cbhmt], that can be compiled (cc pan.c) to produce an executable
	      verifier.  Systems that require more memory than available on  the  target  machine
	      can still be analyzed by compiling the verifier with a bit state space:

		 cc -DBITSTATE pan.c

	      This  collapses  the  state  space  to  1  bit per system state, with minimal side-
	      effects.	Partial order reduction rules take effect during the verification if  the
	      compiler directive -DREDUCE is used.

	      The compiled verifiers have their own sets of options, which can be seen by running
	      them with option -?.

       t      If the verifier finds a violation of a correctness property,  it	writes	an  error
	      trail.   The  trail can be inspected in detail by invoking spin with the -t option.
	      In combination with the options pglrsv, different views of the error  sequence  are
	      then be obtained.

       D      Perform a static dataflow analysis.

       V      Print the version number and exit.

       G.J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1991.
       --, ``Using SPIN''.

Unix & Linux Commands & Man Pages : ©2000 - 2018 Unix and Linux Forums

All times are GMT -4. The time now is 07:16 PM.