Return to spin.1 CVS log

Up to [Research Unix] / researchv10dc / vol2 / spin

Annotation of researchv10dc/vol2/spin/spin.1, revision 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 -pfglpqrsm
        !            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 of processes,
        !            26: nondeterministic case selection, loops, gotos,
        !            27: variables and assertions.
        !            28: The tool has fast and frugal algorithms for analyzing
        !            29: liveness and safeness conditions.
        !            30: .PP
        !            31: Given a model system specified in Promela,
        !            32: .I spin
        !            33: can either perform random simulations of the system's execution
        !            34: or it can generate a C program that performs a fast exhaustive
        !            35: validation of the system state space.
        !            36: The validator can check, for instance, if user specified system
        !            37: invariants may be violated during a protocol's execution, or
        !            38: if any non-progress execution cycles exist.
        !            39: .PP
        !            40: Without any options the program performs a random simulation.
        !            41: With option
        !            42: .TP
        !            43: .BI -n N
        !            44: the seed for the simulation is set explicitly to the integer value
        !            45: .BR N .
        !            46: .PP
        !            47: A second group of options
        !            48: .B -pglrs
        !            49: is used to set the desired level of information that the user wants
        !            50: about the simulation run.
        !            51: Every line of output normally contains a reference to the source
        !            52: line in the specification that caused it.
        !            53: .TP
        !            54: .B p
        !            55: Show at each time step which process changed state.
        !            56: .TP
        !            57: .B l
        !            58: In combination with option
        !            59: .BR p ,
        !            60: show the current value of local variables of the process.
        !            61: .TP
        !            62: .B g
        !            63: Show at each time step the current value of global variables.
        !            64: .TP
        !            65: .B r
        !            66: Show all message-receive events, giving
        !            67: the name and number of the receiving process
        !            68: and the corresponding the source line number.
        !            69: For each message parameter, show
        !            70: the message type and the message channel number and name.
        !            71: .TP
        !            72: .B s
        !            73: Show all message-send events.
        !            74: .PP
        !            75: Two options can be used to alter the model definition itself.
        !            76: .TP
        !            77: .B m
        !            78: Changes the semantics of send events.
        !            79: Ordinarily, a send action will be delayed if the
        !            80: target message buffer if full.
        !            81: With this option a message sent to a full buffer is lost.
        !            82: The option can be combined with
        !            83: .TP
        !            84: .B q
        !            85: Causes spin to inspect the Promela code for sequences that
        !            86: can safely be cast into atomic sequences, to allow a
        !            87: reduction of the complexity of larger validation runs.
        !            88: Manual placement of atomic sequences can usually achieve
        !            89: still larger reductions.
        !            90: .B -a
        !            91: (see below).
        !            92: .TP
        !            93: .B a
        !            94: Generate a protocol-specific analyzer.
        !            95: The output is written into a set of C files, named
        !            96: .BR pan. [ cbhmt ],
        !            97: that can be compiled
        !            98: .RB ( "cc pan.c" )
        !            99: to produce an executable analyzer.
        !           100: Large systems, that require more memory than available
        !           101: on the target machine, can still be analyzed by compiling
        !           102: the analyzer with a bit state space:
        !           103: .IP
        !           104: .B cc -DBITSTATE pan.c
        !           105: .IP
        !           106: This collapses the state space to 1 bit per system state,
        !           107: with minimal side-effects.
        !           108: .IP
        !           109: A compiled analyzer has its own set of options,
        !           110: which can be seen by typing
        !           111: .BR "a.out -?" .
        !           112: .TP
        !           113: .B t
        !           114: If the analyzer finds a violation of an assertion, a deadlock,
        !           115: a non-progress loop, or
        !           116: an unspecified reception, it writes an error trail into a file
        !           117: named
        !           118: .BR pan.trail .
        !           119: The trail can be inspected in detail by invoking
        !           120: .I spin
        !           121: with the
        !           122: .B t
        !           123: option.
        !           124: In combination with the options
        !           125: .B pglrs
        !           126: different views of the error sequence are then easily obtained.
        !           127: .SH SEE ALSO
        !           128: .I cospan
        !           129: in
        !           130: .IR langs (1)
        !           131: .br
        !           132: G.J. Holzmann,
        !           133: `Spin \(em A Protocol Analyzer',
        !           134: this manual, Volume 2.

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