Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages


home | help
SPIN(1)			    General Commands Manual		       SPIN(1)

	Spin - verification of multithreaded systems

       spin -V
       spin [ options ]	file

       SPIN  is	 a  tool for analyzing the logical consistency of asynchronous
       systems,	specifically distributed software, multi-threaded systems, and
       communication  protocols.   A  model  of	 the  system is	specified in a
       guarded command language	called Promela (process	meta language).	  This
       modeling	 language supports dynamic creation of processes, nondetermin-
       istic case selection, loops, gotos, local  and  global  variables.   It
       also allows for a concise specification of logical correctness require-
       ments, including, but not restricted to requirements expressed in  lin-
       ear 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 verification	of the
       correctness requirements	for the	system.	 The  main  options  supported
       are as follows. (You can	always get a full list of current options with
       the command "spin --".

       -a     Generate a verifier (a model  checker)  for  the	specification.
	      The  output  is written into a set of C files named pan.[cbhmt],
	      that can be compiled (cc -o pan pan.c) to	produce	an  executable
	      verifier.	 The online SPIN manuals contain the details on	compi-
	      lation and use of	the verifiers.

       -b     Do not execute printf statements in a simulation run.

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

       -Dxxx  Pass -Dxxx to the	preprocessor (see also -E and -I).

       -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	 vari-
	      ables,  the 3rd field defines the	name of	the structure declara-
	      tion that	contains the variable.

       -Exxx  Pass xxx to the preprocessor (see	also -D	and -I).

       -e     If the specification contains  multiple  never  claims,  or  ltl
	      properties,  compute  the	 synchronous product of	all claims and
	      write the	result to the standard output.

       -f LTL Translate	the LTL	formula	LTL into a never claim.
	      This option reads	a formula in LTL syntax	from the second	 argu-
	      ment and translates it into Promela syntax (a never claim, qhich
	      is Promela's equivalent of a Bchi	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 veri-
	      fication process.	 If the	formula	contains spaces, it should  be
	      quoted to	form a single argument to the SPIN command.
	      This  option  has	largely	been replaced with the support for in-
	      line specification of ltl	formula, in Spin version 6.0.

       -F file
	      Translate	the LTL	formula	stored in file into a never claim.
	      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 con-
	      ventions	of the shell complicate	the use	of option -f .	Option
	      -F is meant to solve those problems.)

       -g     In combination with option -p, print all global variable updates
	      in a simulation run.

       -h     At the end of a simulation run, print the	value of the seed that
	      was used for the random number  generator.   By  specifying  the
	      same  seed  with	the  -n	 option, the exact run can be repeated

       -I     Show the result of inlining and preprocessing.

       -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 printing for	the first N steps in a simulation run.

       -J     Reverse the evaluation order for nested unless statements, e.g.,
	      to match the way in which	Java handles exceptions.

       -k file
	      Use the file name	file as	the trail-file,	see also -t.

       -l     In combination with option -p, include all  local	 variable  up-
	      dates in the output of a simulation run.

       -M     Produce  a  message  sequence  chart in tcl/tk form for a	random
	      simulation or a guided simulation	(when combined with  -t),  for
	      the  model in file , and display the result with wish.  See also
	      option -c.

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

       -nN    Set the seed for a random	simulation to the integer  value  N  .
	      There is no space	between	the -n and the integer N.  ,TP -N file
	      Use the never claim stored in file to generate the verified (see

       -O     Use the original scope rules from	pre-Spin version 6.

	      Turn  off	 data-flow optimization	(-o1).	Do not hide write-only
	      variables	(-o2) during verification.  Turn off statement merging
	      (-o3)  during  verification.   Turn  on  rendezvous optimization
	      (-o4) during verification.  Turn on case caching (-o5) to	reduce
	      the size of pan.m, but losing accuracy in	reachability reports.

       -O     Use the scope rules pre-version 6.0. In this case	there are only
	      two possible levels of scope for all data	declarations:  global,
	      or  proctype  local.   In	version	6.0 and	later there is a third
	      level of scope: inlines or blocks.

       -Pxxx  Use the command xxx for preprocessing instead of the standard  C

       -p     Include  all  statement  executions  in the output of simulation

       -qN    Suppress the output generated for	channel	 N  during  simulation

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

	      Replay an	error trace found  in  an  earlier  verification  (see
	      -search).	  As  with  -search,  arguments	 meant for Spin	itself
	      (e.g., -p) can be	given before the -replay argument. If the  re-
	      play  can	only be	done with the ./pan executable,	then arguments
	      for the replay with the ./pan executable can be given after  the
	      -replay argument.

	      Compile  and run directly. Verificaiton compile-time and runtime
	      flags can	be added after this parameter. Any Spin	parse-time pa-
	      rameters	must  come  before  the	-search	parameter.  The	actual
	      command line executed is printed if -v is	specified (before  the
	      -search argument).

       -s     Include all send operations in the output	of simulation runs.

       -T     Do  not automatically indent the printf output of	process	i with
	      i	tabs.

       -t[N]  Perform a	guided simulation, following  the  [Nth]  error	 trail
	      that was produces	by an earlier verification run,	see the	online
	      manuals for the details on verification. By  default  the	 error
	      trail  is	 looked	 for  in  a file with the same basename	as the
	      model, and with extension	.trail.	 See also -k.

       -v     Verbose mode, add	some more detail, and generate more hints  and
	      warnings about the model.

       -V     Print the	SPIN version number and	exit.

       -x     Generate	transition tables from model and exit (generates, com-
	      piles, and runs pan.c).

       With only a filename as an argument and no option flags,	SPIN  performs
       a  random simulation of the model specified in the file.	 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.   The
       group of	options	-bgilmprstv is used to set the desired level of	infor-
       mation that the user wants about	a random, guided, or interactive simu-
       lation  run.  Every line	of output normally contains a reference	to the
       source line in the specification	that generated it.  If	option	-i  is
       included,  the simulation is interactive, or if option -t or -k file is
       added, the simulation is	guided.

       -b     Suppress the execution of	printf statements within the model.

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

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

       -p     Show  at	each  simulation step which process changed state, and
	      what source statement was	executed.

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

       -s     Show all message-send events.

       -v     Verbose  mode,  add some more detail, and	generat	more hints and
	      warnings about the model.

       Online manuals at
       More background information on the system and the verification process,
       can be found in,	for instance:
	   G.J.	Holzmann, The Spin Model Checker  Primer and Reference Manual,
	   Addison-Wesley, Reading, Mass., 2004.
	   --, `The model checker SPIN,' IEEE Trans. on	SE, Vol,  23,  No.  5,
	   May 1997.
	   --, `Design and validation of protocols: a tutorial,' Computer Net-
	   works and ISDN Systems, Vol.	25, No.	9, 1993, pp. 981-1017.
	   --, Design and Validation of	Computer Protocols, Prentice Hall, En-
	   glewood Cliffs, NJ, 1991.



Want to link to this manual page? Use this URL:

home | help