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