SPIN man page on Plan9

Printed from http://www.polarhome.com/service/man/?qf=SPIN&af=0&tf=2&of=Plan9

SPIN(1)								       SPIN(1)

       spin - verification tool for models of concurrent systems

       spin [ options ] file
       spin -V

       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 (pcc pan.c) to produce an executable	 veri‐
	      fier.   The  online spin manuals contain the details on compila‐
	      tion 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 third field defines the name of the structure decla‐
	      ration 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, which
	      is Promela's equivalent of a Büchi Automaton).  The  LTL	opera‐
	      tors  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.
	      This  option  has	 largely  been	replaced  with the support for
	      inline specification of ltl formula, in Spin version 6.0.

       -F file
	      Translate the LTL formula stored in file into a never claim.
	      This behaves identically 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
	      updates in the output of a simulation run.

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

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

       -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 merg‐
	      ing ( -o3 ) during verification.	Turn on	 rendezvous  optimiza‐
	      tion  ( -o4 ) during verification.  Turn on case caching ( -o5 )
	      to reduce the size of pan.m, but losing accuracy in reachability

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

       -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     Prints the spin version number and exit.

       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  i interactive, or if option -t or -kfile is
       added, the simulation is guided.


       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
       —, `Design and validation of protocols: a tutorial,' Computer  Networks
       and ISDN Systems, Vol. 25, No. 9, 1993, pp. 981-1017.
       —,  Design  and Validation of Computer Protocols, Prentice Hall, Engle‐
       wood Cliffs, NJ, 1991.

                             _         _         _ 
                            | |       | |       | |     
                            | |       | |       | |     
                         __ | | __ __ | | __ __ | | __  
                         \ \| |/ / \ \| |/ / \ \| |/ /  
                          \ \ / /   \ \ / /   \ \ / /   
                           \   /     \   /     \   /    
                            \_/       \_/       \_/ 
More information is available in HTML format for server Plan9

List of man pages available for Plan9

Copyright (c) for man pages and the logo by the respective OS vendor.

For those who want to learn more, the polarhome community provides shell access and support.

[legal] [privacy] [GNU] [policy] [cookies] [netiquette] [sponsors] [FAQ]
Polarhome, production since 1999.
Member of Polarhome portal.
Based on Fawad Halim's script.
Vote for polarhome
Free Shell Accounts :: the biggest list on the net