Return to spin.1 CVS log

Up to [Research Unix] / researchv10dc / man / adm / man1

Annotation of researchv10dc/man/adm/man1/spin.1, revision 1.1.1.1

1.1       root        1: .TH SPIN 1
                      2: .CT 1 comm_mach protocol
                      3: .SH NAME
                      4: spin \(mi protocol analysis software
                      5: .SH SYNOPSIS
                      6: .B spin
                      7: [
                      8: .BI -n N
                      9: ]
                     10: [
                     11: .BI -pglprs
                     12: ]
                     13: [
                     14: .BI -at
                     15: ]
                     16: [
                     17: .I file
                     18: ]
                     19: .SH DESCRIPTION
                     20: .I Spin
                     21: is a tool for analyzing the logical consistency of
                     22: concurrent systems, specifically communication protocols.
                     23: The system is specified in a guarded command language called Promela.
                     24: The language, described in the reference,
                     25: allows for the dynamic creation and deletion of both processes
                     26: and message channels, nondeterministic case selection, loops, gotos,
                     27: variables and assertions.
                     28: .PP
                     29: Given a model system specified in Promela,
                     30: .I spin
                     31: can either perform random simulations of the system's execution
                     32: or it can generate a C program that performs a fast exhaustive
                     33: validation of the system state space.
                     34: The validator can check, for instance, if user specified system
                     35: invariants may be violated during a protocol's execution.
                     36: .PP
                     37: Without any options the program performs a random simulation.
                     38: With option
                     39: .TP
                     40: .BI -n N
                     41: the seed for the simulation is set explicitly to the integer value
                     42: .BR N .
                     43: .PP
                     44: The second group of options
                     45: .B -pglrs
                     46: is used to set the desired level of information that the user wants
                     47: about the simulation run.
                     48: Every line of output normally contains a reference to the source
                     49: line in the specification that caused it.
                     50: .TP
                     51: .B p
                     52: Show at each time step which process changed state.
                     53: .TP
                     54: .B l
                     55: In combination with option
                     56: .BR p ,
                     57: show the current value of local variables of the process.
                     58: .TP
                     59: .B g
                     60: Show at each time step the current value of global variables.
                     61: .TP
                     62: .B r
                     63: Show all message-receive events, giving
                     64: the name and number of the receiving process
                     65: and the corresponding the source line number.
                     66: For each message parameter, show
                     67: the message type and the message channel number and name.
                     68: .TP
                     69: .B s
                     70: Show all message-send events.
                     71: .TP
                     72: .B a
                     73: Generate a protocol-specific analyzer.
                     74: The output is written into a set of C files, named
                     75: .BR pan. [ cbhmt ],
                     76: that can be compiled
                     77: .RB ( "cc pan.c" )
                     78: to produce an executable analyzer.
                     79: For larger systems the state space can quickly exhaust
                     80: the available memory on the machine used.
                     81: Large to very large systems can still be analyzed by compiling
                     82: with a bit state space:
                     83: .IP
                     84: .B cc -DBITSTATE pan.c
                     85: .IP
                     86: A compiled analyzer has its own set of options,
                     87: which can be seen by typing
                     88: .BR "a.out -?" .
                     89: .TP
                     90: .B t
                     91: If the analyzer finds a violation of an assertion, a deadlock, or
                     92: an unspecified reception, it writes an error trail into a file
                     93: named
                     94: .BR pan.trail .
                     95: The trail can be inspected in detail by invoking
                     96: .I spin
                     97: with the
                     98: .B t
                     99: option.
                    100: In combination with the options
                    101: .B pglrs
                    102: different views of the error sequence are then easily obtained.
                    103: .SH SEE ALSO
                    104: .I cospan
                    105: in
                    106: .IR langs (1)
                    107: .br
                    108: G.J. Holzmann,
                    109: `Spin \(em A Protocol Analyzer',
                    110: this manual, Volume 2.

This archive runs on limited infrastructure. Preserving old code on modern bandwidth. Automated agents are requested to crawl responsibly.