Return to spin CVS log

Up to [Plan 9 NeXT] / lucent / sys / man / 1

Annotation of lucent/sys/man/1/spin, revision 1.1

1.1     ! root        1: .TH SPIN 1
        !             2: .SH NAME
        !             3: spin \- verification tool for concurrent systems
        !             4: .SH SYNOPSIS
        !             5: .B spin
        !             6: [
        !             7: .BI -n N
        !             8: ]
        !             9: [
        !            10: .B -plgrsmv
        !            11: ]
        !            12: [
        !            13: .B -iat
        !            14: ]
        !            15: [
        !            16: .B -DV
        !            17: ]
        !            18: [
        !            19: .I file
        !            20: ]
        !            21: .SH DESCRIPTION
        !            22: .I Spin
        !            23: is a tool for analyzing the logical consistency of
        !            24: concurrent systems, specifically communication protocols.
        !            25: The system is specified in a guarded command language called
        !            26: .SM PROMELA2\c
        !            27: \&.
        !            28: The language, described in the references,
        !            29: allows for the dynamic creation of processes,
        !            30: nondeterministic case selection, loops, gotos,
        !            31: variables, and the specification of correctness requirements.
        !            32: The tool has fast algorithms for analyzing arbitrary
        !            33: liveness and safety conditions.
        !            34: .PP
        !            35: Given a model system specified in
        !            36: .SM PROMELA2\c
        !            37: ,
        !            38: .I spin
        !            39: can perform interactive, guided, or random simulations
        !            40: of the system's execution
        !            41: or it can generate a C program that performs an exhaustive
        !            42: or approximate verification of the system.
        !            43: The verifier can check, for instance, if user specified system
        !            44: invariants are violated during a protocol's execution, or
        !            45: if non-progress execution cycles exist.
        !            46: .PP
        !            47: Without any options the program performs a random simulation of the system
        !            48: defined in the input
        !            49: .IR file ,
        !            50: default standard input.
        !            51: The option
        !            52: .BI -n N
        !            53: sets the random seed to the integer value
        !            54: .IR N .
        !            55: .PP
        !            56: The group of options
        !            57: .B -pglmrsv
        !            58: is used to set the level of information reported
        !            59: about the simulation run.
        !            60: Every line of output normally contains a reference to the source
        !            61: line in the specification that caused it.
        !            62: .TP
        !            63: .B p
        !            64: Show at each time step which process changed state and what source
        !            65: statement was executed.
        !            66: .TP
        !            67: .B l
        !            68: In combination with option
        !            69: .BR p ,
        !            70: show the current value of local variables of the process.
        !            71: .TP
        !            72: .B g
        !            73: Show the value of global variables at each time step.
        !            74: .TP
        !            75: .B r
        !            76: Show all message-receive events, giving
        !            77: the name and number of the receiving process
        !            78: and the corresponding source line number.
        !            79: For each message parameter, show
        !            80: the message type and the message channel number and name.
        !            81: .TP
        !            82: .B s
        !            83: Show all message-send events.
        !            84: .TP
        !            85: .B m
        !            86: Ordinarily, a send action will be delayed if the
        !            87: target message buffer if full.
        !            88: With this option a message sent to a full buffer is lost.
        !            89: The option can be combined with
        !            90: .B -a
        !            91: (see below).
        !            92: .TP
        !            93: .B v
        !            94: Verbose mode: add extra detail and include more warnings.
        !            95: .TP
        !            96: .BI i
        !            97: Perform an interactive simulation.
        !            98: .TP
        !            99: .B a
        !           100: Generate a protocol-specific verifier.
        !           101: The output is written into a set of C files, named
        !           102: .BR pan. [ cbhmt ],
        !           103: that can be compiled
        !           104: .RB ( "cc pan.c" )
        !           105: to produce an executable verifier.
        !           106: Systems that require more memory than available
        !           107: on the target machine can still be analyzed by compiling
        !           108: the verifier with a bit state space:
        !           109: .IP
        !           110: .B "   cc -DBITSTATE pan.c
        !           111: .IP
        !           112: This collapses the state space to 1 bit per system state,
        !           113: with minimal side-effects.
        !           114: Partial order reduction rules take effect during the
        !           115: verification if the compiler directive
        !           116: .B -DREDUCE
        !           117: is used.
        !           118: .IP
        !           119: The compiled verifiers have their own sets of options,
        !           120: which can be seen by running them with option
        !           121: .BR -? .
        !           122: .TP
        !           123: .B t
        !           124: If the verifier finds a violation of a correctness property,
        !           125: it writes an error trail.
        !           126: The trail can be inspected in detail by invoking
        !           127: .I spin
        !           128: with the
        !           129: .B -t
        !           130: option.
        !           131: In combination with the options
        !           132: .BR pglrsv ,
        !           133: different views of the error sequence are then be obtained.
        !           134: .TP
        !           135: .B D
        !           136: Perform a static dataflow analysis.
        !           137: .TP
        !           138: .B V
        !           139: Print the version number and exit.
        !           140: .SH SEE ALSO
        !           141: G.J. Holzmann,
        !           142: .I
        !           143: Design and Validation of Computer Protocols,
        !           144: Prentice Hall, 1991.
        !           145: .br
        !           146: \(em, ``Using
        !           147: .SM SPIN\c
        !           148: \&''.

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