Provided by: spin_6.5.2+dfsg-1_amd64 bug

NAME

        Spin − verification of multithreaded systems

SYNOPSIS

       spin -V
       spin [ options ] file

DESCRIPTION

       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,  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  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
              compilation 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 variables, the 3rd field defines the name of  the  structure
              declaration 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 argument  and  translates
              it  into  Promela  syntax  (a never claim, which is Promela's equivalent of a Büchi
              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.
              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 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.)

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

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

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

       -o[123]
              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 preprocessor.

       -p     Include all statement executions in the output of simulation runs.

       -qN    Suppress the output generated for channel N during simulation runs.

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

       -replay
              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 replay can only be done with the ./pan executable, then  arguments
              for the replay with the ./pan executable can be given after the -replay argument.

       -search
              Compile  and run directly. Verificaiton compile-time and runtime flags can be added
              after this parameter. Any Spin parse-time parameters 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,  compiles,  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 information that the user wants
       about 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 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 number.  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.

SEE ALSO

       Online manuals at spinroot.com:
           http://spinroot.com/spin/Man/3_SpinGUI.html
           http://spinroot.com/spin/Man/4_SpinVerification.html
           http://spinroot.com/spin/Man/1_Exercises.html
       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  Networks  and  ISDN
           Systems, Vol. 25, No. 9, 1993, pp. 981-1017.
           --,  Design and Validation of Computer Protocols, Prentice Hall, Englewood Cliffs, NJ,
           1991.

                                                                                          SPIN(1)