Return to spin.ms CVS log

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

Annotation of researchv10dc/vol2/spin/spin.ms, revision 1.1

1.1     ! root        1: .so ../ADM/mac
        !             2: .XX spin 429 "Spin \(em A Protocol Analyzer"
        !             3: .nr dP 2
        !             4: .nr dV 3p
        !             5: .EQ
        !             6: delim @@
        !             7: .EN
        !             8: .de IH \" makes a bold italic sub heading
        !             9: .NH 2
        !            10: \\$1
        !            11: ..
        !            12: .ds P \\s-2PROMELA\\s0
        !            13: .ds S \fISpin\fP
        !            14: .ds s \fIspin\fP
        !            15: .TL
        !            16: Spin \(em A Protocol Analyzer
        !            17: .AU "MH 2C-521" 6335
        !            18: Gerard J. Holzmann
        !            19: .AI
        !            20: .MH
        !            21: .AB
        !            22: \*S is a tool for analyzing the logical consistency of
        !            23: concurrent systems, specifically of data communication protocols.
        !            24: The system is described in a modeling language called \*P.
        !            25: The language allows for the dynamic creation of concurrent processes.
        !            26: Communication via message channels can be defined to be synchronous
        !            27: (i.e., rendez-vous), or asynchronous (i.e., buffered).
        !            28: .PP
        !            29: Given a model system specified in \*P, \*s
        !            30: can either perform random simulations of the system's execution
        !            31: or it can generate a C program that performs a fast exhaustive
        !            32: validation of the system state space.
        !            33: During simulations and validations \*s checks for the absence of deadlocks,
        !            34: unspecified receptions, and unexecutable code.
        !            35: The validator can also be used to verify the correctness of
        !            36: system invariants, and it can find non-progress execution cycles.
        !            37: .PP
        !            38: The validator is setup to be extremely fast and to use
        !            39: only a minimal amount of memory.
        !            40: The exhaustive validations performed by \*s are conclusive,
        !            41: They establish with certainty whether or not a given behavior
        !            42: is error-free.
        !            43: Very large validation runs, that can ordinarily not be
        !            44: performed with automated techniques, can be
        !            45: done in \*s with a novel ``bit state space'' technique.
        !            46: With this method the state space is collapsed to a single
        !            47: bit per system state stored, with minimal side-effects.
        !            48: .PP
        !            49: The first part of this memo gives an introduction to \*P,
        !            50: the second part discusses the usage of \*s, and
        !            51: the third part contains a brief reference manual for \*P.
        !            52: In the appendix an example is used to illustrate the construction
        !            53: of a basic \*P model for \*s validations.
        !            54: .AE
        !            55: .2C
        !            56: .NH
        !            57: Introduction to \*P
        !            58: .PP
        !            59: \*P is a validation modeling language.
        !            60: It provides a vehicle for making abstractions of protocols
        !            61: (or distributed systems in general) that suppress details
        !            62: that are unrelated to process interaction.
        !            63: The intended use of \*s is to validate fractions of process
        !            64: behavior, that for one reason or another is considered suspect.
        !            65: The relevant behavior is modeled in \*P and validated.
        !            66: A complete validation is therefore typically performed in a series of steps,
        !            67: with the construction of increasingly detailed \*P models.
        !            68: Each model can be validated with \*s under different types of
        !            69: assumptions about the environment (e.g., message loss, message
        !            70: duplications etc).
        !            71: Once the correctness of a model has been established with \*s, that
        !            72: fact can be used in the construction and validation of all
        !            73: subsequent models.
        !            74: .PP
        !            75: \*P programs consist of \f2processes\f1,
        !            76: message \f2channels\f1, and \f2variables\f1.
        !            77: Processes are global objects.
        !            78: Message channels and variables can be declared either globally
        !            79: or locally within a process.
        !            80: Processes specify behavior; channels and global variables
        !            81: define the environment in which the processes run.
        !            82: .IH Executability
        !            83: .PP
        !            84: In \*P there is no difference between conditions and
        !            85: statements, even isolated boolean conditions can be used as statements.
        !            86: The execution of every statement is conditional on its
        !            87: .I executability .
        !            88: Statements are either executable or blocked.
        !            89: The executability is the basic means of synchronization.
        !            90: A process can wait for an event to happen by waiting
        !            91: for a statement to become executable.
        !            92: For instance, instead of writing a busy wait loop:
        !            93: .P1 0
        !            94: while (a != b)
        !            95:        skip    /* wait for a==b */
        !            96: .P2
        !            97: one can achieve the same effect in \*P with the statement
        !            98: .P1 0
        !            99: (a == b)
        !           100: .P2
        !           101: A condition can only be executed (passed) when it holds.
        !           102: If the condition does not hold, execution blocks until it does.
        !           103: .PP
        !           104: Variables are used to store either global information about the
        !           105: system as a whole, or information local to one specific process,
        !           106: depending on where the declaration for the variable is placed.
        !           107: The declarations
        !           108: .P1 0
        !           109: bool flag;
        !           110: int state;
        !           111: byte msg;
        !           112: .P2
        !           113: define variables that can store integer values in
        !           114: three different ranges.
        !           115: The scope of a variable is global if it is declared outside all
        !           116: process declarations, and local if it is declared within a process
        !           117: declaration.
        !           118: .IH "Data Types"
        !           119: .PP
        !           120: Table 1 summarizes the basic data types, sizes,
        !           121: and the corresponding value ranges (on a DEC VAX computer).
        !           122: .KS
        !           123: .SP .5
        !           124: .ps -1
        !           125: .vs -2
        !           126: .TS
        !           127: center;
        !           128: l l l l
        !           129: lFCW n r c.
        !           130: =
        !           131: Name   Size (bits)     Usage   Range
        !           132: _
        !           133: bit    1       unsigned        0..1
        !           134: bool   1       unsigned        0..1
        !           135: byte   8       unsigned        0..255
        !           136: short  16      signed  @-2 sup 15@..@{2 sup 15} - 1@
        !           137: int    32      signed  @-2 sup 31@..@{2 sup 31} - 1@
        !           138: _
        !           139: .TE
        !           140: .ps +1
        !           141: .vs +2
        !           142: .SP .5
        !           143: .ce
        !           144: \fBTable 1.\fP Data Types
        !           145: .SP
        !           146: .KE
        !           147: The names
        !           148: .CW bit
        !           149: and
        !           150: .CW bool
        !           151: are synonyms for a single bit of information.
        !           152: A
        !           153: .CW byte
        !           154: is an unsigned quantity that can store a value between
        !           155: .CW 0
        !           156: and
        !           157: .CW 255 .
        !           158: .CW short s
        !           159: and
        !           160: .CW int s
        !           161: are signed quantities that
        !           162: differ only in the range of values they can hold.
        !           163: .IH "Array Variables"
        !           164: .PP
        !           165: Variables can be declared as arrays.
        !           166: For instance,
        !           167: .P1 0
        !           168: byte state[N]
        !           169: .P2
        !           170: declares an array of
        !           171: .CW N
        !           172: bytes that can be accessed in statements such as
        !           173: .P1 0
        !           174: state[0] = state[3] + 5 * state[3*2/n]
        !           175: .P2
        !           176: where
        !           177: .CW n
        !           178: is a constant or a variable declared elsewhere.
        !           179: The index to an array can be any expression that
        !           180: determines a unique integer value.
        !           181: The effect of an index value outside the range
        !           182: .CW "0 .. N-1"
        !           183: is undefined; most likely it will cause a runtime error.
        !           184: .PP
        !           185: So far we have seen examples of variable declarations
        !           186: and of two types of statements: boolean conditions and
        !           187: assignments.
        !           188: Declarations and assignments are always \f2executable\f1.
        !           189: Conditions are only executable when they hold.
        !           190: .IH "Process Types"
        !           191: .PP
        !           192: The state of a variable or of a message channel
        !           193: can only be changed or inspected by processes.
        !           194: The behavior of a process is defined in a
        !           195: .CW proctype
        !           196: declaration.
        !           197: The following, for instance, declares a process with one local variable
        !           198: .CW state .
        !           199: .P1 0
        !           200: proctype A()
        !           201: {      byte state;
        !           202: 
        !           203:        state = 3
        !           204: }
        !           205: .P2
        !           206: The process type is named
        !           207: .CW A .
        !           208: The body of the declaration is enclosed in curly braces.
        !           209: The declaration body consists of a list of zero or more
        !           210: declarations of local variables and/or statements.
        !           211: The declaration above contains one local variable declaration
        !           212: and a single statement: an assignment of the
        !           213: value 3 to variable
        !           214: .CW state .
        !           215: .PP
        !           216: The semicolon is a statement \f2separator\f1 (not a statement terminator,
        !           217: hence there is no semicolon after the last statement).
        !           218: \*P accepts two different statement separators:
        !           219: .CW `->'
        !           220: (arrow) and
        !           221: .CW `;' .
        !           222: The two statement separators are equivalent.
        !           223: The arrow is sometimes used as an informal way to indicate a causal
        !           224: relation between two statements.
        !           225: Consider the following example.
        !           226: .P1 0
        !           227: byte state = 2;
        !           228: 
        !           229: proctype A()
        !           230: {      (state == 1) -> state = 3
        !           231: }
        !           232: .P3
        !           233: proctype B()
        !           234: {      state = state \- 1
        !           235: }
        !           236: .P2
        !           237: In this example we declared two types of processes,
        !           238: .CW A
        !           239: and
        !           240: .CW B .
        !           241: Variable
        !           242: .CW state
        !           243: is now a global, initialized to the value two.
        !           244: Process type
        !           245: .CW A
        !           246: contains two statements, separated by an arrow.
        !           247: In the example, process declaration
        !           248: .CW B
        !           249: contains a single statement that decrements
        !           250: the value of the state variable by one.
        !           251: Since the assignment is always executable,
        !           252: processes of type
        !           253: .CW B
        !           254: can always complete without delay.
        !           255: Processes of type
        !           256: .CW A ,
        !           257: however, are delayed at the condition until
        !           258: the variable
        !           259: .CW state
        !           260: contains the proper value.
        !           261: ......
        !           262: .IH "Process Instantiation"
        !           263: .PP
        !           264: A
        !           265: .CW proctype
        !           266: definition only declares process behavior, it
        !           267: does not execute it.
        !           268: Initially, in the \*P model, just one process will be executed:
        !           269: a process of type
        !           270: .CW init ,
        !           271: that must be declared explicitly in every \*P specification.
        !           272: The smallest possible \*P specification, therefore, is:
        !           273: .P1 0
        !           274: init { skip }
        !           275: .P2
        !           276: where
        !           277: .CW skip
        !           278: is a dummy, null statement.
        !           279: More interestingly, however,
        !           280: the initial process can initialize global variables,
        !           281: and instantiate processes.
        !           282: An
        !           283: .CW init
        !           284: declaration for the above system, for instance, could look as follows.
        !           285: .P1 0
        !           286: init
        !           287: {      run A(); run B()
        !           288: }
        !           289: .P2
        !           290: .PP
        !           291: .CW run
        !           292: is used as a unary operator that takes the name of a process type (e.g.
        !           293: .CW A ).
        !           294: It is executable only if a process of
        !           295: the type specified can be instantiated.
        !           296: It is unexecutable if this cannot be done,
        !           297: for instance if too many processes are already running.
        !           298: .PP
        !           299: The
        !           300: .CW run
        !           301: statement can pass parameter values of all basic
        !           302: data types to the new process.
        !           303: The declarations are then written, for instance, as follows:
        !           304: .P1 0
        !           305: proctype A(byte state; short foo)
        !           306: {
        !           307:        (state == 1) -> state = foo
        !           308: }
        !           309: .P3
        !           310: init
        !           311: {
        !           312:        run A(1, 3)
        !           313: }
        !           314: .P2
        !           315: Data arrays or process types can not be passed as parameters.
        !           316: As we will see below, there is just one other data type that
        !           317: can be used as a parameter: a message channel.
        !           318: .PP
        !           319: .CW Run
        !           320: statements can be used in any process to spawn new processes,
        !           321: not just in the initial process.
        !           322: Processes are created with the
        !           323: .CW run
        !           324: statements.
        !           325: An executing process disappears again when it terminates
        !           326: (i.e., reaches the end of the body of its
        !           327: process type declaration), but not before all processes
        !           328: that it started have terminated.
        !           329: .PP
        !           330: With the
        !           331: .CW run
        !           332: statement we can create any number of copies of the process types
        !           333: .CW A
        !           334: and
        !           335: .CW B .
        !           336: If, however, more than one concurrent process is allowed to both read and
        !           337: write the value of a global variable a well-known set of problems
        !           338: can result; for example see |reference(dijkstra concurrent).
        !           339: Consider, for instance, the following system of
        !           340: two processes, sharing access to the global variable
        !           341: .CW state .
        !           342: .P1 0
        !           343: byte state = 1;
        !           344: 
        !           345: proctype A()
        !           346: {      (state==1) -> state = state+1
        !           347: }
        !           348: .P3
        !           349: proctype B()
        !           350: {      (state==1) -> state = state\-1
        !           351: }
        !           352: .P3
        !           353: init
        !           354: {      run A(); run B()
        !           355: }
        !           356: .P2
        !           357: If one of the two processes completes before its competitor has
        !           358: started, the other process will block forever on the initial condition.
        !           359: If both pass the condition simultaneously, both will complete, but
        !           360: the resulting value of
        !           361: .CW state
        !           362: is unpredictable.
        !           363: It can be any of the values
        !           364: .CW 0 ,
        !           365: .CW 1 ,
        !           366: or
        !           367: .CW 2 .
        !           368: .PP
        !           369: Many solutions to this problem have been considered, ranging from
        !           370: an abolishment of global variables to the provision of special
        !           371: machine instructions that can guarantee an indivisible test and
        !           372: set sequence on a shared variable.
        !           373: The example below was one of the first solutions published.
        !           374: It is due to the Dutch mathematician Dekker.
        !           375: It grants two processes mutually exclusion access to an arbitrary
        !           376: .I
        !           377: critical section
        !           378: .R
        !           379: in their code, by manipulation three additional global variables.
        !           380: The first four lines in the \*P specification
        !           381: below are C-style macro definitions.
        !           382: The first two macros define
        !           383: .CW true
        !           384: to be a constant value equal to
        !           385: .CW 1
        !           386: and
        !           387: .CW false
        !           388: to be a constant
        !           389: .CW 0 .
        !           390: Similarly,
        !           391: .CW Aturn
        !           392: and
        !           393: .CW Bturn
        !           394: are defined as constants.
        !           395: .P1 0
        !           396: #define true   1
        !           397: #define false  0
        !           398: #define Aturn  false
        !           399: #define Bturn  true
        !           400: 
        !           401: bool x, y, t;
        !           402: .P3
        !           403: 
        !           404: proctype A()
        !           405: {      x = true;
        !           406:        t = Bturn;
        !           407:        (y == false || t == Aturn);
        !           408:        /* critical section */
        !           409:        x = false
        !           410: }
        !           411: .P3
        !           412: proctype B()
        !           413: {      y = true;
        !           414:        t = Aturn;
        !           415:        (x == false || t == Bturn);
        !           416:        /* critical section */
        !           417:        y = false
        !           418: }
        !           419: .P3
        !           420: init
        !           421: {      run A(); run B()
        !           422: }
        !           423: .P2
        !           424: The algorithm can be executed repeatedly and is independent of
        !           425: the relative speeds of the two processes.
        !           426: .IH "Atomic Sequences"
        !           427: .PP
        !           428: In \*P there is also another way to avoid the \f2test and set\f1
        !           429: problem:
        !           430: .CW atomic
        !           431: sequences.
        !           432: By prefixing a sequence of statements enclosed in curly
        !           433: braces with the keyword
        !           434: .CW atomic
        !           435: the user can indicate that the sequence is to be executed
        !           436: as one indivisible unit, non-interleaved with any other
        !           437: processes.
        !           438: It causes a run-time error if any statement, other than
        !           439: the first statement, blocks in an atomic sequence.
        !           440: This is how we can use atomic sequences to protect the
        !           441: concurrent access to the global variable
        !           442: .CW state
        !           443: in the earlier example.
        !           444: .P1 0
        !           445: byte state = 1;
        !           446: 
        !           447: proctype A()
        !           448: {      atomic {
        !           449:          (state==1) -> state = state+1
        !           450:        }
        !           451: }
        !           452: .P3
        !           453: proctype B()
        !           454: {      atomic {
        !           455:          (state==1) -> state = state\-1
        !           456:        }
        !           457: }
        !           458: .P3
        !           459: init
        !           460: {      run A(); run B()
        !           461: }
        !           462: .P2
        !           463: In this case the final value of
        !           464: .CW state
        !           465: is guaranteed to be zero, though during the execution of
        !           466: .CW A
        !           467: and
        !           468: .CW B
        !           469: the intermediate value can be either
        !           470: .CW 0
        !           471: or
        !           472: .CW 2 .
        !           473: .PP
        !           474: Atomic sequences can be an important tool in reducing
        !           475: the complexity of validation models.
        !           476: Note that atomic sequence restricts the amount of
        !           477: interleaving that is allowed in a distributed system.
        !           478: Otherwise untractable models can be made tractable
        !           479: by, for instance, labeling all manipulations of local variables
        !           480: with atomic sequences.
        !           481: The reduction in complexity can be dramatic.
        !           482: .IH "Message Passing"
        !           483: .PP
        !           484: Message channels are used to model the transfer of data
        !           485: from one process to another.
        !           486: They are declared either locally or globally,
        !           487: for instance as follows:
        !           488: .P1 0
        !           489: chan qname[16] of { short }
        !           490: .P2
        !           491: This declares a channel that can store up
        !           492: to 16 messages of type
        !           493: .CW short .
        !           494: Channel names can be passed from one process to another via
        !           495: channels or as parameters in process instantiations.
        !           496: If the messages to be passed by the channel have more than
        !           497: one field, the declaration may look as follows:
        !           498: .P1 0
        !           499: chan qname[16] of { byte, int, chan, byte }
        !           500: .P2
        !           501: This time each message in the channel stores up to
        !           502: sixteen messages, each consisting of two 8-bit values,
        !           503: one 32-bit value, and a channel name.
        !           504: .PP
        !           505: .Tm !  S
        !           506: .Tm ?  S
        !           507: The statement
        !           508: .P1 0
        !           509: qname!expr
        !           510: .P2
        !           511: sends the value of expression
        !           512: .CW expr
        !           513: to the channel that we just created, that is:
        !           514: it appends the value to the tail of the channel.
        !           515: .P1 0
        !           516: qname?msg
        !           517: .P2
        !           518: receives the message, it retrieves it from the head of the channel,
        !           519: and stores it in a variable
        !           520: .CW msg .
        !           521: The channels pass messages in first-in-first-out order.
        !           522: In the above cases only a single value
        !           523: is passed through the channel.
        !           524: If more than one value is to be transferred per message,
        !           525: they are specified in a comma separated list
        !           526: .P1 0
        !           527: qname!expr1,expr2,expr3
        !           528: qname?var1,var2,var3
        !           529: .P2
        !           530: If more parameters are sent per message then the message channel
        !           531: can store, the redundant parameters are lost without warning.
        !           532: If fewer parameters are sent then the message channel can store,
        !           533: the value of the remaining parameters is undefined.
        !           534: Similarly, if the receive operation tries to retrieve more
        !           535: parameters than available, the value of the extra parameters is
        !           536: undefined; if it receives fewer than the number of parameters
        !           537: that was sent, the extra information is lost.
        !           538: .PP
        !           539: By convention, the first message field is often
        !           540: used to specify the message type (i.e. a constant).
        !           541: An alternative, and equivalent, notation for the
        !           542: send and receive operations is therefore to specify the
        !           543: message type, followed by a list of message fields
        !           544: enclosed in braces.
        !           545: In general:
        !           546: .P1 0
        !           547: qname!expr1(expr2,expr3)
        !           548: qname?var1(var2,var3)
        !           549: .P2
        !           550: .PP
        !           551: The send operation is executable only when the channel addressed is not full.
        !           552: The receive operation, similarly, is only executable
        !           553: when the channel is non empty.
        !           554: Optionally, some of the arguments of the receive operation
        !           555: can be constants:
        !           556: .P1 0
        !           557: qname?cons1,var2,cons2
        !           558: .P2
        !           559: in this case, a further condition on the executability of the
        !           560: receive operation is that the value of all message fields that are
        !           561: specified as constants match the value of the corresponding fields
        !           562: in the message that is at the head of the channel.
        !           563: Again, nothing bad will happen if a statement happens to be non-executable.
        !           564: The process trying to execute it will be delayed until the
        !           565: statement, or, more likely, an alternative statement, becomes executable.
        !           566: .PP
        !           567: Here is an example that uses some of the mechanisms introduced
        !           568: so far.
        !           569: .P1 0
        !           570: proctype A(chan q1)
        !           571: {      chan q2;
        !           572:        q1?q2;
        !           573:        q2!123
        !           574: }
        !           575: .P3
        !           576: proctype B(chan qforb)
        !           577: {      int x;
        !           578:        qforb?x;
        !           579:        printf("x = %d\n", x)
        !           580: }
        !           581: .P3
        !           582: init {
        !           583:        chan qname[1] of { chan };
        !           584:        chan qforb[1] of { int };
        !           585:        run A(qname);
        !           586:        run B(qforb);
        !           587:        qname!qforb
        !           588: }
        !           589: .P2
        !           590: The value printed will be
        !           591: .CW 123 .
        !           592: .PP
        !           593: A predefined function
        !           594: .CW len(qname)
        !           595: returns the number of messages currently
        !           596: stored in channel
        !           597: .CW qname .
        !           598: Note that if
        !           599: .CW len
        !           600: is used as a statement, rather than on
        !           601: the right hand side of an assignment, it will be unexecutable if
        !           602: the channel is empty: it returns a zero result, which by definition
        !           603: means that the statement is temporarily unexecutable.
        !           604: Composite conditions such as
        !           605: .P1 0
        !           606: (qname?var == 0)
        !           607: .P2
        !           608: or
        !           609: .P1 0
        !           610: (a > b && qname!123)
        !           611: .P2
        !           612: are invalid in \*P (note that these conditions can not be evaluated
        !           613: without side-effects).
        !           614: For a receive statement there is an alternative, using square
        !           615: brackets around the clause behind the question mark.
        !           616: .P1 0
        !           617: qname?[ack,var]
        !           618: .P2
        !           619: is evaluated as a condition.
        !           620: It returns
        !           621: .CW 1
        !           622: if the corresponding receive statement
        !           623: .P1 0
        !           624: qname?ack,var
        !           625: .P2
        !           626: is executable, i.e., if there is indeed a message
        !           627: .CW ack
        !           628: at the head of the channel.
        !           629: It returns
        !           630: .CW 0
        !           631: otherwise.
        !           632: In neither case has the evaluation of a statement such as
        !           633: .P1 0
        !           634: qname?[ack,var]
        !           635: .P2
        !           636: any side-effects: the receive is evaluated, not executed.
        !           637: .PP
        !           638: Note carefully that in non-atomic sequences of two statements such as
        !           639: .P1 0
        !           640: (len(qname) < MAX) -> qname!msgtype
        !           641: .P2
        !           642: or
        !           643: .P1 0
        !           644: qname?[msgtype] -> qname?msgtype
        !           645: .P2
        !           646: the second statement is not \f2necessarily\f1 executable
        !           647: after the first one has been executed.
        !           648: There may be race conditions if access to the channels
        !           649: is shared between several processes.
        !           650: In the first case
        !           651: another process can send a message to channel
        !           652: .CW qname
        !           653: just after this process determined that the channel was not full.
        !           654: In the second case, the other process can steal away the
        !           655: message just after our process determined its presence.
        !           656: .IH "Rendez-Vous Communication"
        !           657: .PP
        !           658: So far we have talked about asynchronous communication between processes
        !           659: via message channels, declared in statements such as
        !           660: .P1 0
        !           661: chan qname [N] of { byte }
        !           662: .P2
        !           663: where
        !           664: .CW N
        !           665: is a positive constant that defines the buffer size.
        !           666: A logical extension is to allow for the declaration
        !           667: .P1 0
        !           668: chan port [0] of { byte }
        !           669: .P2
        !           670: to define a rendez-vous port that can pass single byte messages.
        !           671: The channel size is zero, that is, the channel
        !           672: .CW port
        !           673: can pass, but can not store messages.
        !           674: Message interactions via such rendez-vous ports are
        !           675: by definition synchronous.
        !           676: Consider the following example.
        !           677: .P1 0
        !           678: #define msgtype 33
        !           679: 
        !           680: chan name [0] of { byte, byte };
        !           681: 
        !           682: proctype A()
        !           683: {      name!msgtype(124);
        !           684:        name!msgtype(121)
        !           685: }
        !           686: .P3
        !           687: proctype B()
        !           688: {      byte state;
        !           689:        name?msgtype(state)
        !           690: }
        !           691: .P3
        !           692: init
        !           693: {      atomic { run A(); run B() }
        !           694: }
        !           695: .P2
        !           696: Channel
        !           697: .CW name
        !           698: is a global rendez-vous port.
        !           699: The two processes will synchronously execute their first statement:
        !           700: a handshake on message
        !           701: .CW msgtype
        !           702: and a transfer of the value 124 to local variable
        !           703: .CW state .
        !           704: The second statement in process
        !           705: .CW A
        !           706: will be unexecutable,
        !           707: because there is no matching receive operation in process
        !           708: .CW B .
        !           709: .PP
        !           710: If the channel
        !           711: .CW name
        !           712: is defined  with a non-zero buffer capacity,
        !           713: the behavior is different.
        !           714: If the buffer size is at least 2, the process of type
        !           715: .CW A
        !           716: can complete its execution, before its peer even starts.
        !           717: If the buffer size is 1, the sequence of events is as follows.
        !           718: The process of type
        !           719: .CW A
        !           720: can complete its first send action, but it blocks on the
        !           721: second, because the channel is now filled to capacity.
        !           722: The process of type
        !           723: .CW B
        !           724: can then retrieve the first message and complete.
        !           725: At this point
        !           726: .CW A
        !           727: becomes executable again and completes,
        !           728: leaving its last message as a residual in the channel.
        !           729: .PP
        !           730: Rendez-vous communication is binary: only two processes,
        !           731: a sender and a receiver, can be synchronized in a
        !           732: rendez-vous handshake.
        !           733: We will see an example of a way to exploit this to
        !           734: build a semaphore below.
        !           735: But first, let us introduce a few more control flow structures
        !           736: that may be useful.
        !           737: .NH 2
        !           738: Control Flow
        !           739: .PP
        !           740: Between the lines, we have already introduced three ways of
        !           741: defining control flow: concatenation of statements
        !           742: within a process, parallel execution of processes, and
        !           743: atomic sequences.
        !           744: There are three other control flow constructs in \*P to be discussed.
        !           745: They are case selection,
        !           746: repetition, and
        !           747: unconditional jumps.
        !           748: .NH 3
        !           749: Case Selection
        !           750: .PP
        !           751: The simplest construct is the selection structure.
        !           752: Using the relative values of two variables
        !           753: .CW a
        !           754: and
        !           755: .CW b
        !           756: to choose between two options, for instance, we can write:
        !           757: .P1 0
        !           758: if
        !           759: :: (a != b) -> option1
        !           760: :: (a == b) -> option2
        !           761: fi
        !           762: .P2
        !           763: The selection structure contains two execution sequences,
        !           764: each preceded by a double colon.
        !           765: Only one sequence from the list will be executed.
        !           766: A sequence can be selected only if its first statement is executable.
        !           767: The first statement is therefore called a \f2guard\f1.
        !           768: .PP
        !           769: In the above example the guards are mutually exclusive, but they
        !           770: need not be.
        !           771: If more than one guard is executable, one of the corresponding sequences
        !           772: is selected nondeterministically.
        !           773: If all guards are unexecutable the process will block until at least
        !           774: one of them can be selected.
        !           775: There is no restriction on the type of statements that can be used
        !           776: as a guard.
        !           777: The following example, for instance, uses input statements.
        !           778: .P1 0
        !           779: #define a 1
        !           780: #define b 2
        !           781: 
        !           782: chan ch[1] of { byte };
        !           783: 
        !           784: proctype A()
        !           785: {      ch!a
        !           786: }
        !           787: .P3
        !           788: proctype B()
        !           789: {      ch!b
        !           790: }
        !           791: .P3
        !           792: proctype C()
        !           793: {      if
        !           794:        :: ch?a
        !           795:        :: ch?b
        !           796:        fi
        !           797: }
        !           798: .P3
        !           799: init
        !           800: {      atomic { run A(); run B(); run C() }
        !           801: }
        !           802: .P2
        !           803: The example defines three processes and one channel.
        !           804: The first option in the selection structure of the process
        !           805: of type
        !           806: .CW C
        !           807: is executable if the channel contains
        !           808: a message
        !           809: .CW a ,
        !           810: where
        !           811: .CW a
        !           812: is a constant with value
        !           813: .CW 1 ,
        !           814: defined in a macro definition at the start of the program.
        !           815: The second option is executable if it contains a message
        !           816: .CW b ,
        !           817: where, similarly,
        !           818: .CW b
        !           819: is a constant.
        !           820: Which message will be available depends on the unknown
        !           821: relative speeds of the processes.
        !           822: .PP
        !           823: A process of the following type will either increment
        !           824: or decrement the value of variable
        !           825: .CW count
        !           826: once.
        !           827: .P1 0
        !           828: byte count;
        !           829: 
        !           830: proctype counter()
        !           831: {
        !           832:        if
        !           833:        :: count = count + 1
        !           834:        :: count = count \- 1
        !           835:        fi
        !           836: }
        !           837: .P2
        !           838: .NH 3
        !           839: Repetition
        !           840: .PP
        !           841: A logical extension of the selection structure is
        !           842: the repetition structure.
        !           843: We can modify the above program as follows, to obtain
        !           844: a cyclic program that randomly changes the value of
        !           845: the variable up or down.
        !           846: .P1 0
        !           847: byte count;
        !           848: 
        !           849: proctype counter()
        !           850: {
        !           851:        do
        !           852:        :: count = count + 1
        !           853:        :: count = count \- 1
        !           854:        :: (count == 0) -> break
        !           855:        od
        !           856: }
        !           857: .P2
        !           858: .PP
        !           859: Only one option can be selected for execution at a time.
        !           860: After the option completes, the execution of the structure
        !           861: is repeated.
        !           862: The normal way to terminate the repetition structure is
        !           863: with a
        !           864: .CW break
        !           865: statement.
        !           866: In the example, the loop can be
        !           867: broken when the count reaches zero.
        !           868: Note, however, that it need
        !           869: not terminate since the other two options always remain executable.
        !           870: To force termination we could modify the program as follows.
        !           871: .P1 0
        !           872: proctype counter()
        !           873: {
        !           874:        do
        !           875:        :: (count != 0) ->
        !           876:                if
        !           877:                :: count = count + 1
        !           878:                :: count = count \- 1
        !           879:                fi
        !           880:        :: (count == 0) -> break
        !           881:        od
        !           882: }
        !           883: .P2
        !           884: .NH 3
        !           885: Unconditional Jumps
        !           886: .PP
        !           887: Another way to break the loop is with an unconditional jump:
        !           888: the infamous
        !           889: .CW goto
        !           890: statement.
        !           891: This is illustrated in the following implementation of Euclid's algorithm for
        !           892: finding the greatest common divisor of two non-zero, positive numbers:
        !           893: .P1 0
        !           894: proctype Euclid(int x, y)
        !           895: {
        !           896:        do
        !           897:        :: (x >  y) -> x = x \- y
        !           898:        :: (x <  y) -> y = y \- x
        !           899:        :: (x == y) -> goto done
        !           900:        od;
        !           901: done:
        !           902:        skip
        !           903: }
        !           904: .P2
        !           905: The
        !           906: .CW goto
        !           907: in this example jumps to a label named
        !           908: .CW done .
        !           909: A label can only appear before a statement.
        !           910: Above we want to jump to the end of the program.
        !           911: In this case a dummy statement
        !           912: .CW skip
        !           913: is useful: it is a place holder that
        !           914: is always executable and has no effect.
        !           915: The
        !           916: .CW goto
        !           917: is also always executable.
        !           918: .PP
        !           919: The following example specifies a filter that receives
        !           920: messages from a channel
        !           921: .CW in
        !           922: and divides them over two channels
        !           923: .CW large
        !           924: and
        !           925: .CW small
        !           926: depending on the values attached.
        !           927: The constant
        !           928: .CW N
        !           929: is defined to be
        !           930: .CW 128
        !           931: and
        !           932: .CW size
        !           933: is defined to be
        !           934: .CW 16
        !           935: in the two macro definitions.
        !           936: .P1 0
        !           937: #define N    128
        !           938: #define size  16
        !           939: .P3
        !           940: 
        !           941: chan in    [size] of { short };
        !           942: chan large [size] of { short };
        !           943: chan small [size] of { short };
        !           944: .P3
        !           945: 
        !           946: proctype split()
        !           947: {      short cargo;
        !           948: 
        !           949:        do
        !           950:        :: in?cargo ->
        !           951:                if
        !           952:                :: (cargo >= N) ->
        !           953:                        large!cargo
        !           954:                :: (cargo <  N) ->
        !           955:                        small!cargo
        !           956:                fi
        !           957:        od
        !           958: }
        !           959: .P3
        !           960: init
        !           961: {      run split()
        !           962: }
        !           963: .P2
        !           964: A process type that merges the two streams back into one, most
        !           965: likely in a different order, and writes it back
        !           966: into the channel
        !           967: .CW in
        !           968: could be specified as follows.
        !           969: .P1 0
        !           970: proctype merge()
        !           971: {      short cargo;
        !           972: 
        !           973:        do
        !           974:        ::      if
        !           975:                :: large?cargo
        !           976:                :: small?cargo
        !           977:                fi;
        !           978:                in!cargo
        !           979:        od
        !           980: }
        !           981: .P2
        !           982: If we now modify the
        !           983: .CW init
        !           984: process as follows, the
        !           985: split and merge processes could busily perform their
        !           986: duties forever on.
        !           987: .P1 0
        !           988: init
        !           989: {      in!345; in!12; in!6777;
        !           990:        in!32;  in!0;
        !           991:        run split();
        !           992:        run merge()
        !           993: }
        !           994: .P2
        !           995: .PP
        !           996: As a final example, consider the following implementation of
        !           997: a Dijkstra semaphore, using binary rendez-vous communication.
        !           998: .P1 0
        !           999: #define p      0
        !          1000: #define v      1
        !          1001: 
        !          1002: chan sema[0] of { bit };
        !          1003: .P3
        !          1004: proctype dijkstra()
        !          1005: {      byte count = 1;
        !          1006: 
        !          1007:        do
        !          1008:        :: (count == 1) \->
        !          1009:                sema!p; count = 0
        !          1010:        :: (count == 0) \->
        !          1011:                sema?v; count = 1
        !          1012:        od      
        !          1013: }
        !          1014: .P3
        !          1015: proctype user()
        !          1016: {      do
        !          1017:        :: sema?p;
        !          1018:           /*     critical section */
        !          1019:           sema!v;
        !          1020:           /* non-critical section */
        !          1021:        od
        !          1022: }
        !          1023: .P3
        !          1024: init
        !          1025: {      run dijkstra();
        !          1026:        run user();
        !          1027:        run user();
        !          1028:        run user()
        !          1029: }
        !          1030: .P2
        !          1031: The semaphore guarantees that only one of the user processes
        !          1032: can enter its critical section at a time.
        !          1033: It does not necessarily prevent the monopolization of
        !          1034: the access to the critical section by one of the processes.
        !          1035: .IH "Modeling Procedures and Recursion"
        !          1036: .PP
        !          1037: Procedures can be modeled as processes, even recursive ones.
        !          1038: The return value can be passed back to the calling process
        !          1039: via a global variable, or via a message.
        !          1040: The following program illustrates this.
        !          1041: .P1 0
        !          1042: proctype fact(int n; chan p)
        !          1043: {      chan child[1] of { int };
        !          1044:        int result;
        !          1045: 
        !          1046:        if
        !          1047:        :: (n <= 1) -> p!1
        !          1048:        :: (n >= 2) ->
        !          1049:                run fact(n-1, child);
        !          1050:                child?result;
        !          1051:                p!n*result
        !          1052:        fi
        !          1053: }
        !          1054: init
        !          1055: {      chan child [1] of { int };
        !          1056:        int result;
        !          1057: 
        !          1058:        run fact(7, child);
        !          1059:        child?result;
        !          1060:        printf("result: %d\n", result)
        !          1061: }
        !          1062: .P2
        !          1063: The process
        !          1064: .I "fact(n, p)"
        !          1065: recursively calculates the factorial of
        !          1066: .I n ,
        !          1067: communicating the result via a message to its parent process
        !          1068: .I p .
        !          1069: .IH "Timeouts"
        !          1070: .PP
        !          1071: We have already discussed two types of statement
        !          1072: with a predefined meaning in \*P:
        !          1073: .CW skip ,
        !          1074: and
        !          1075: .CW break .
        !          1076: Another predefined statement is
        !          1077: .CW timeout .
        !          1078: The
        !          1079: .CW timeout
        !          1080: models a special condition that allows a process to
        !          1081: abort the waiting for a condition that may never become true, e.g.
        !          1082: an input from an empty channel.
        !          1083: The timeout keyword is a modeling feature in \*P that provides an
        !          1084: escape from a hang state.
        !          1085: The timeout condition becomes true only when no other
        !          1086: statements within the distributed system is executable.
        !          1087: Note that we deliberately abstract from absolute timing
        !          1088: considerations, which is crucial in validation work,
        !          1089: and we do not specify how the timeout should be implemented.
        !          1090: A simple example is the following process that will send
        !          1091: a reset message to a channel named \f2guard\f1 whenever the
        !          1092: system comes to a standstill.
        !          1093: .P1 0
        !          1094: proctype watchdog()
        !          1095: {
        !          1096:        do
        !          1097:        :: timeout -> guard!reset
        !          1098:        od
        !          1099: }
        !          1100: .P2
        !          1101: .IH "Assertions"
        !          1102: .PP
        !          1103: Another important language construct in \*P that
        !          1104: needs little explanation is the
        !          1105: .CW assert
        !          1106: statement.
        !          1107: Statements of the form
        !          1108: .P1 0
        !          1109: assert(any_boolean_condition)
        !          1110: .P2
        !          1111: are always executable.
        !          1112: If the boolean condition specified holds, the statement has no effect.
        !          1113: If, however, the condition does not necessarily hold,
        !          1114: the statement will produce an error report during validations with \*s.
        !          1115: .NH 2
        !          1116: More Advanced Usage
        !          1117: .PP
        !          1118: The modeling language has a few features that specifically address
        !          1119: the validation aspects.
        !          1120: It shows up in the way labels are used, in the
        !          1121: semantics of the \*P
        !          1122: .CW timeout
        !          1123: statement, and in the usage of statements such as
        !          1124: \f(CWassert\f1 that we discuss next.
        !          1125: .NH 3
        !          1126: End-State Labels
        !          1127: .PP
        !          1128: When \*P is used as a validation language the user must
        !          1129: be able to make very specific assertions about the behavior
        !          1130: that is being modeled.
        !          1131: In particular, if a \*P is checked for the presence of
        !          1132: deadlocks, the validator must be able to distinguish a normal \f2end state\f1
        !          1133: from an abnormal one.
        !          1134: .PP
        !          1135: A normal end state could be a state in which every \*P process
        !          1136: that was instantiated has properly reached the end of the
        !          1137: defining program body, and all message channels are empty.
        !          1138: But, not all \*P process are, of course, meant to reach the
        !          1139: end of their program body.
        !          1140: Some may very well linger in an \f(CWIDLE\f1
        !          1141: state, or they may sit patiently in a loop
        !          1142: ready to spring into action when new input arrives.
        !          1143: .PP
        !          1144: To make it clear to the validator that these alternate end states
        !          1145: are legal, and do not constitute a deadlock, a \*P model can use
        !          1146: end state labels.
        !          1147: For instance, if by adding a label to the process type
        !          1148: \f(CWdijkstra()\f1, from section 1.9:
        !          1149: .P1
        !          1150: proctype dijkstra()
        !          1151: {      byte count = 1;
        !          1152: 
        !          1153: end:   do
        !          1154:        :: (count == 1) \->
        !          1155:                sema!p; count = 0
        !          1156:        :: (count == 0) \->
        !          1157:                sema?v; count = 1
        !          1158:        od      
        !          1159: }
        !          1160: .P2
        !          1161: we indicate that it is not an error if, at the end of an
        !          1162: execution sequence, a process of type \f(CWdijkstra()\f1
        !          1163: has not reached its closing curly brace, but waits in the loop.
        !          1164: Of course, such a state could still be part of a deadlock state, but
        !          1165: if so, it is not caused by this particular process.
        !          1166: (It will still be reported if any one of the other processes
        !          1167: in not in a valid end-state).
        !          1168: .PP
        !          1169: There may be more than one end state label per validation model.
        !          1170: If so, all labels that occur within the same process body must
        !          1171: be unique.
        !          1172: The rule is that every label name that \f2starts\f1 with the three
        !          1173: character sequence \f(CW"end"\f1
        !          1174: is an endstate label.
        !          1175: So it is perfectly valid to use variations such as
        !          1176: \f(CWenddne\f1, \f(CWend0\f1, \f(CWend_appel\f1, etc.
        !          1177: .NH 3
        !          1178: Progress-State Labels
        !          1179: .PP
        !          1180: In the same spirit as the end state labels, the user can also
        !          1181: define \f2progress state\f1 labels.
        !          1182: In this case, a progress state labels will mark a state that
        !          1183: \f2must\f1 be executed for the protocol to make progress.
        !          1184: Any infinite cycle in the protocol execution that does not
        !          1185: pass through at least one of these progress states, is a
        !          1186: potential starvation loop.
        !          1187: In the
        !          1188: .CW dijkstra
        !          1189: example, for instance, we can label the
        !          1190: successful passing of a semaphore test as ``progress'' and
        !          1191: ask a validator to make sure that there is no cycle in the
        !          1192: protocol execution where at least one process succeeds in
        !          1193: passing the semaphore guard.
        !          1194: If more than one state carries a progress label,
        !          1195: variations with a common prefix are again valid:
        !          1196: \f(CWprogress0\f1, \f(CWprogress_foo\f1, etc.
        !          1197: .KF
        !          1198: .P1
        !          1199: proctype dijkstra()
        !          1200: {      byte count = 1;
        !          1201: 
        !          1202: end:   do
        !          1203:        :: (count == 1) ->
        !          1204: progress:      sema!p; count = 0
        !          1205:        :: (count == 0) ->
        !          1206:                sema?v; count = 1
        !          1207:        od      
        !          1208: }
        !          1209: .P2
        !          1210: .KE
        !          1211: .PP
        !          1212: .CW "spin -a"
        !          1213: generates analyzers that support (after compilation) a
        !          1214: .CW -l
        !          1215: option, which makes the analyzer use a fast search for non-progress loops,
        !          1216: instead of the default search for deadlocks.
        !          1217: The
        !          1218: .CW -l
        !          1219: search completely avoids the expense of a
        !          1220: full construction of all strongly
        !          1221: connected components in the reachability graph
        !          1222: (the conventional method for doing loop analysis).
        !          1223: The expense is therefore never more than about
        !          1224: twice the time and memory requirements of
        !          1225: a default search for deadlocks.
        !          1226: .IH "Message Type Definitions"
        !          1227: .PP
        !          1228: We have seen how variables are declared and how constants
        !          1229: can be defined using C-style macros.
        !          1230: As a mild form of syntactic sugar, \*P also allows for
        !          1231: message type definitions that look as follows:
        !          1232: .P1 0
        !          1233: mtype = {
        !          1234:        ack, nak, err,
        !          1235:        next, accept
        !          1236: }
        !          1237: .P2
        !          1238: This is a preferred way of specifying the message types since
        !          1239: it abstracts from the specific values to be used, and it makes
        !          1240: the names of the constants available to an implementation,
        !          1241: which can improve error reporting.
        !          1242: .IH "Pseudo Statements"
        !          1243: .PP
        !          1244: We have now discussed all the basic types of statements defined in \*P:
        !          1245: assignments, conditions, send and receive,
        !          1246: .CW assert ,
        !          1247: .CW timeout ,
        !          1248: .CW goto ,
        !          1249: .CW break
        !          1250: and
        !          1251: .CW skip .
        !          1252: Note that
        !          1253: .CW chan ,
        !          1254: .CW len 
        !          1255: and
        !          1256: .CW run
        !          1257: are not really statements but unary operators that can be used in
        !          1258: conditions and assignments.
        !          1259: .PP
        !          1260: The
        !          1261: .CW skip
        !          1262: statement was mentioned in passing as a statement that can be
        !          1263: a useful filler to satisfy syntax requirements, but that really
        !          1264: has no effect.
        !          1265: It is formally not part of the language but a \f2pseudo-statement\f1,
        !          1266: merely a synonym of another statement with the same effect: a
        !          1267: simple condition of a constant value
        !          1268: .CW (1) .
        !          1269: In the same spirit other pseudo-statements could be
        !          1270: defined, such as
        !          1271: \f(CWblock\f1 or \f(CWhang\f1, equivalents of \f(CW(0)\f1,
        !          1272: and
        !          1273: \f(CWhalt\f1, as an equivalent of \f(CWassert(0)\f1..
        !          1274: .IH Example
        !          1275: .PP
        !          1276: Here is a simple example of a (flawed) protocol, modeled in \*P.
        !          1277: .P1 0
        !          1278: mtype = {
        !          1279:        ack, nak, err, next, accept
        !          1280: }
        !          1281: 
        !          1282: .P3
        !          1283: proctype transfer(chan in,out,chin,chout)
        !          1284: {      byte o, i;
        !          1285: 
        !          1286:        in?next(o);
        !          1287: .P3
        !          1288:        do
        !          1289:        :: chin?nak(i) ->
        !          1290:                        out!accept(i);
        !          1291:                        chout!ack(o)
        !          1292: .P3
        !          1293:        :: chin?ack(i) ->
        !          1294:                        out!accept(i);
        !          1295:                        in?next(o);
        !          1296:                        chout!ack(o)
        !          1297: .P3
        !          1298:        :: chin?err(i) ->
        !          1299:                        chout!nak(o)
        !          1300:        od
        !          1301: }
        !          1302: 
        !          1303: .P3
        !          1304: init
        !          1305: {      chan AtoB[1] of { byte, byte };
        !          1306:        chan BtoA[1] of { byte, byte };
        !          1307: .P3
        !          1308:        chan Ain [2] of { byte };
        !          1309:        chan Bin [2] of { byte };
        !          1310: .P3
        !          1311:        chan Aout[2] of { byte };
        !          1312:        chan Bout[2] of { byte };
        !          1313: .P3
        !          1314:        atomic {
        !          1315:          run transfer(Ain,Aout, AtoB,BtoA);
        !          1316:          run transfer(Bin,Bout, BtoA,AtoB)
        !          1317:        };
        !          1318: .P3
        !          1319:        AtoB!err(0)
        !          1320: }
        !          1321: .P2
        !          1322: The channels
        !          1323: .CW Ain
        !          1324: and
        !          1325: .CW Bin
        !          1326: are to be filled with
        !          1327: token messages of type
        !          1328: .CW next
        !          1329: and arbitrary values (e.g.
        !          1330: ASCII character values) by unspecified background processes:
        !          1331: the users of the transfer service.
        !          1332: Similarly, these user processes
        !          1333: can read received data from the channels
        !          1334: .CW Aout
        !          1335: and
        !          1336: .CW Bout .
        !          1337: The channels and processes are initialized in a single
        !          1338: atomic statement, and started with the dummy
        !          1339: .CW err
        !          1340: message.
        !          1341: .NH
        !          1342: Introduction to Spin
        !          1343: .PP
        !          1344: Given a model system specified in \*P, \*s
        !          1345: can either perform random simulations of the system's execution
        !          1346: or it can generate a C program that performs a fast exhaustive
        !          1347: validation of the system state space.
        !          1348: The validator can check, for instance, if user specified system
        !          1349: invariants may be violated during a protocol's execution.
        !          1350: .PP
        !          1351: If \*s is invoked without any options it performs a random simulation.
        !          1352: With option
        !          1353: .CW -n\fIN
        !          1354: the seed for the simulation is set explicitly to the integer value
        !          1355: .I N .
        !          1356: .PP
        !          1357: The options
        !          1358: .CW pglrs
        !          1359: controls the amount of information output from the simulation run.
        !          1360: Every line of output normally contains a reference to the source
        !          1361: line in the specification that caused it.
        !          1362: .IP \f(CW-p\f1
        !          1363: Shows the state changes of the \*P
        !          1364: processes at every time step.
        !          1365: .IP \f(CW-g\f1
        !          1366: Shows the current value of global variables at every time step.
        !          1367: .IP \f(CW-l\f1
        !          1368: Shows the current value of local variables, after the
        !          1369: process that owns them has changed state.
        !          1370: It is best used in combination with option
        !          1371: .CW -p .
        !          1372: .IP \f(CW-r\f1
        !          1373: Shows all message receive events.
        !          1374: It shows the process performing the receive, its name and number,
        !          1375: the source line number, the message parameter number (there is
        !          1376: one line for each parameter), the message type and the message
        !          1377: channel number and name.
        !          1378: .IP \f(CW-s\f1
        !          1379: Shows all message send events.
        !          1380: .LP
        !          1381: \*S understands four other options:
        !          1382: .IP \f(CW-a\f1
        !          1383: Generates a protocol specific analyzer.
        !          1384: The output is written into a set of C files, named
        !          1385: .CW pan.[cbhmt] ,
        !          1386: that can be compiled to produce the analyzer
        !          1387: (which is then executed to perform the analysis).
        !          1388: To guarantee an exhaustive exploration of the state space, the
        !          1389: program can be compiled simply as
        !          1390: .RS
        !          1391: .IP
        !          1392: .P1
        !          1393: $ cc -o run pan.c
        !          1394: .P2
        !          1395: .RE
        !          1396: .IP
        !          1397: For larger systems this may, however, exhaust the available memory
        !          1398: on the machine used.
        !          1399: Large to very large systems can still be analyzed by using a
        !          1400: memory efficient bit state space method by
        !          1401: .RS
        !          1402: .IP
        !          1403: .P1
        !          1404: $ cc -DBITSTATE -o run pan.c
        !          1405: .P2
        !          1406: .RE
        !          1407: .IP
        !          1408: An indication of the coverage of such a search can be derived from the
        !          1409: .I "hash factor"
        !          1410: (see below).
        !          1411: The generated executable analyzer, named
        !          1412: .CW run
        !          1413: above, has its own set of options that can be seen by typing
        !          1414: .CW "run -?"
        !          1415: (see also below in ``The Analyzer'').
        !          1416: .IP \f(CW-m\f1
        !          1417: can be used to change the default semantics of send actions.
        !          1418: Normally, a send operation is only executable if the target channel
        !          1419: is non-full.
        !          1420: This imposes an implicit synchronization that can not always
        !          1421: be justified.
        !          1422: Option \f(CW-m\f1 causes send actions to be always executable.
        !          1423: Messages sent to a channel that is full are then dropped.
        !          1424: If this option is combined with \f(CW-a\f1 the semantics of send
        !          1425: in the analyzers generated is similarly altered, and the validations
        !          1426: will take the effects of this type of message loss into consideration.
        !          1427: .IP \f(CW-q\f1
        !          1428: causes \*s to peruse the model for obviously atomicable
        !          1429: sequences, and to label them appropriately, in an effort to
        !          1430: reduce the complexity of large validation runs.
        !          1431: Typically, the user can do better by hand (by being more
        !          1432: daring than \*s can be in this case).
        !          1433: .IP \f(CW-t\f1
        !          1434: is a trail-hunting option.
        !          1435: If the analyzer finds a violation of an assertion, a deadlock or
        !          1436: an unspecified reception, it writes an error trail into a file
        !          1437: named
        !          1438: .CW pan.trail .
        !          1439: The trail can be inspected in detail by invoking \*s with the
        !          1440: .CW -t
        !          1441: option.
        !          1442: In combination with the options
        !          1443: .CW pglrs
        !          1444: different views of the error sequence are then easily obtained.
        !          1445: .PP
        !          1446: For brevity, other features of \*s are not discussed here.
        !          1447: For details see|reference(holzmann spinbook), for a hint of
        !          1448: what else is available, see ``Digging Deeper'' at the end of this manual.
        !          1449: .IH "The Simulator"
        !          1450: .PP
        !          1451: Consider the following example protocol, that we will store in a
        !          1452: file named
        !          1453: .CW lynch .
        !          1454: .P1 0
        !          1455:    1  #define MIN      9
        !          1456:    2  #define MAX      12
        !          1457:    3  #define FILL     99
        !          1458:    4  
        !          1459:    5  mtype = { ack, nak, err }
        !          1460:    6  
        !          1461: .P3
        !          1462:    7  proctype transfer(chan chin, chout)
        !          1463:    8  {        byte o, i, last_i=MIN;
        !          1464:    9  
        !          1465:   10   o = MIN+1;
        !          1466: .P3
        !          1467:   11   do
        !          1468:   12   :: chin?nak(i) ->
        !          1469:   13           assert(i == last_i+1);
        !          1470:   14           chout!ack(o)
        !          1471: .P3
        !          1472:   15   :: chin?ack(i) ->
        !          1473:   16           if
        !          1474:   17           :: (o <  MAX) -> o = o+1
        !          1475:   18           :: (o >= MAX) -> o = FILL
        !          1476:   19           fi;
        !          1477:   20           chout!ack(o)
        !          1478: .P3
        !          1479:   21   :: chin?err(i) ->
        !          1480:   22           chout!nak(o)
        !          1481:   23   od
        !          1482:   24  }
        !          1483:   25  
        !          1484: .P3
        !          1485:   26  proctype channel(chan in, out)
        !          1486:   27  {        byte md, mt;
        !          1487:   28   do
        !          1488:   29   :: in?mt,md ->
        !          1489:   30           if
        !          1490:   31           :: out!mt,md
        !          1491:   32           :: out!err,0
        !          1492:   33           fi
        !          1493:   34   od
        !          1494:   35  }
        !          1495:   36  
        !          1496: .P3
        !          1497:   37  init
        !          1498:   38  {        chan AtoB[1] of { byte, byte };
        !          1499:   39   chan BtoC[1] of { byte, byte };
        !          1500:   40   chan CtoA[1] of { byte, byte };
        !          1501:   41   atomic {
        !          1502:   42           run transfer(AtoB, BtoC);
        !          1503:   43           run channel(BtoC, CtoA);
        !          1504:   44           run transfer(CtoA, AtoB)
        !          1505:   45   };
        !          1506:   46   AtoB!err,0;     /* start */
        !          1507:   47   0               /* hang */
        !          1508:   48  }
        !          1509: .P2
        !          1510: The protocol uses three message types: \f2ack\f1, \f2nak\f1, and
        !          1511: a special type \f2err\f1 that is used to model message distortions
        !          1512: on the communication channel between the two transfer processes.
        !          1513: The behavior of the channel is modeled explicitly with a channel
        !          1514: process.
        !          1515: There is also an
        !          1516: .CW assert
        !          1517: statement that claims a (faulty) invariant
        !          1518: relation between two local variables in the transfer processes.
        !          1519: .PP
        !          1520: Running \*s without options gives us a random simulation that
        !          1521: will only provide output when execution terminates, or if
        !          1522: a \f2printf\f1 statement is encountered.
        !          1523: In this case:
        !          1524: .P1 0
        !          1525: $ spin lynch
        !          1526: spin: "lynch" line 13: assertion violated
        !          1527: #processes: 4
        !          1528: proc  3 (transfer)     line 11 (state 15)
        !          1529: proc  2 (channel)      line 28 (state 6)
        !          1530: proc  1 (transfer)     line 13 (state 3)
        !          1531: proc  0 (:init:)       line 48 (state 6)
        !          1532: 4 processes created
        !          1533: $ 
        !          1534: .P2
        !          1535: There are no \f2printf\f1's in the specification, but execution
        !          1536: halts on an assertion violation.
        !          1537: Curious to find out more, we can repeat the run with more verbose
        !          1538: output, e.g. printing all receive events.
        !          1539: The result of that run is shown in Figure 1.
        !          1540: Most output will be self-explanatory.
        !          1541: .PP
        !          1542: The above simulation run ends in the same assertion violation.
        !          1543: Since the simulation resolves nondeterministic choices in a
        !          1544: random manner, this need not always be the case.
        !          1545: To force a reproducible run, the option
        !          1546: .CW -n\fIN
        !          1547: can be used.
        !          1548: For instance:
        !          1549: .P1 0
        !          1550: $ spin -r -n100 lynch
        !          1551: .P2
        !          1552: will seed the random number generator with the integer value 100
        !          1553: and is guaranteed to produce the same output each time it is executed.
        !          1554: .PP
        !          1555: The other options can add still more output to the simulation run,
        !          1556: but the amount of text can quickly become overwhelming.
        !          1557: An easy solution is to filter the output through \f2grep\f1.
        !          1558: For instance, if we are only interested in the behavior of the
        !          1559: channel process in the above example, we say:
        !          1560: .P1 0
        !          1561: $ spin -n100 -r lynch | grep "proc  2"
        !          1562: .P2
        !          1563: The results are shown in Figure 1.
        !          1564: .1C
        !          1565: .KF
        !          1566: .nf
        !          1567: .ps -2
        !          1568: .vs -3p
        !          1569: .ft CW
        !          1570: .TS
        !          1571: box expand;
        !          1572: l
        !          1573: l.
        !          1574:       $ spin -r lynch
        !          1575:       proc  1 (transfer) line  21, Recv err,0  <- queue 1 (chin)
        !          1576:       proc  2 (channel)  line  29, Recv nak,10 <- queue 2 (in)
        !          1577:       proc  3 (transfer) line  12, Recv nak,10 <- queue 3 (chin)
        !          1578:       proc  1 (transfer) line  15, Recv ack,10 <- queue 1 (chin)
        !          1579:       \&...
        !          1580:       proc  1 (transfer) line  15, Recv ack,12 <- queue 1 (chin)
        !          1581:       proc  2 (channel)  line  29, Recv ack,99 <- queue 2 (in)
        !          1582:       proc  3 (transfer) line  15, Recv ack,99 <- queue 3 (chin)
        !          1583:       proc  1 (transfer) line  15, Recv ack,99 <- queue 1 (chin)
        !          1584:       proc  2 (channel)  line  29, Recv ack,99 <- queue 2 (in)
        !          1585:       proc  3 (transfer) line  21, Recv err,0  <- queue 3 (chin)
        !          1586:       proc  1 (transfer) line  12, Recv nak,99 <- queue 1 (chin)
        !          1587:       spin: "lynch" line 13: assertion violated
        !          1588:       #processes: 4
        !          1589:       proc  3 (transfer) line 11 (state 15)
        !          1590:       proc  2 (channel)  line 28 (state 6)
        !          1591:       proc  1 (transfer) line 13 (state 3)
        !          1592:       proc  0 (:init:)   line 48 (state 6)
        !          1593:       4 processes created
        !          1594:       $ spin -n100 -r lynch | grep "proc  2"
        !          1595:       proc  2 (channel) line 29, Recv nak,10 <- queue 2 (in)
        !          1596:       proc  2 (channel) line 29, Recv ack,11 <- queue 2 (in)
        !          1597:       proc  2 (channel) line 29, Recv ack,12 <- queue 2 (in)
        !          1598:       proc  2 (channel) line 28 (state 6)
        !          1599: .TE
        !          1600: .fi
        !          1601: .ps +2
        !          1602: .vs +3p
        !          1603: .SP .5
        !          1604: .ce
        !          1605: \fBFigure 1.\fR  Simulation Run Output
        !          1606: .SP .5
        !          1607: .KE
        !          1608: .2C
        !          1609: ......
        !          1610: .IH "The Analyzer"
        !          1611: .PP
        !          1612: The simulation runs can be useful in quick debugging of
        !          1613: new designs, but by simulation alone we can not prove
        !          1614: that the system is really error free.
        !          1615: A validation of even very large models can be performed with the
        !          1616: .CW -a
        !          1617: and
        !          1618: .CW -t
        !          1619: options of \*s.
        !          1620: .PP
        !          1621: An exhaustive state space searching program for a protocol
        !          1622: model is generated as follows, producing five files, named \f2pan.[bchmt]\f1.
        !          1623: .P1 0
        !          1624: $ spin -a lynch
        !          1625: .P3
        !          1626: $ wc pan.[bchmt]
        !          1627: .P3
        !          1628:      92     326    2041 pan.b
        !          1629: .P3
        !          1630:     854    2502   17524 pan.c
        !          1631: .P3
        !          1632:     147     576    3475 pan.h
        !          1633: .P3
        !          1634:     307    1230    7493 pan.m
        !          1635: .P3
        !          1636:     177     548    3997 pan.t
        !          1637: .P3
        !          1638:    1577    5182   34530 total
        !          1639: .P2
        !          1640: The details are none too interesting: \f2pan.c\f1 contains
        !          1641: most of the C code for the analysis of the protocol.
        !          1642: File \f2pan.t\f1 contains a transition matrix that encodes
        !          1643: the protocol control flow; \f2pan.b\f1 and \f2pan.m\f1 contain
        !          1644: C code for forward and backward transitions and
        !          1645: \f2pan.h\f1 is a general header file.
        !          1646: The program can be compiled in two different ways: with a full
        !          1647: state space or with a bit state space.
        !          1648: .IH "Exhaustive Search"
        !          1649: .PP
        !          1650: The best method, that works up to system state spaces of
        !          1651: roughly 100,000 states, is to use the
        !          1652: default compilation of the program:
        !          1653: .P1 0
        !          1654: $ cc -o run pan.c
        !          1655: .P2
        !          1656: The executable program \f2run\f1 can now be executed to perform
        !          1657: the validation.
        !          1658: The validation is truly exhaustive: it tests all possible
        !          1659: event sequences in all possible orders.
        !          1660: It should, of course, find the same assertion violation.
        !          1661: .P1 0
        !          1662: $ run
        !          1663: assertion violated (i == last_i + 1))
        !          1664: pan: aborted
        !          1665: pan: wrote pan.trail
        !          1666: search interrupted
        !          1667: vector 64 byte, depth reached 56
        !          1668:       61 states, stored
        !          1669:        5 states, linked
        !          1670:        1 states, matched
        !          1671: hash conflicts: 0 (resolved)
        !          1672: (size 2^18 states, stack frames: 0/5)
        !          1673: .P2
        !          1674: The first line of the output announces the assertion violation
        !          1675: and attempts to give a first indication of the invariant that
        !          1676: was violated.
        !          1677: The violation was found after 61 states had been generated.
        !          1678: Hash "conflicts" gives the number
        !          1679: of hash collisions that happened during access to the state space.
        !          1680: As indicated,
        !          1681: all collisions are resolved in full search mode, since all states are
        !          1682: placed in a linked list.
        !          1683: The most relevant piece of output in this case, however, is on the
        !          1684: third line which tells us that a trail file was created that can
        !          1685: be used in combination with the simulator to recreate the error
        !          1686: sequence.
        !          1687: We can now say, for instance
        !          1688: .P1 0
        !          1689: $ spin -t -r lynch | grep "proc  2"
        !          1690: .P2
        !          1691: to determine the cause of the error.
        !          1692: Note carefully that the validator is guaranteed to find the
        !          1693: assertion violation if it is feasible.
        !          1694: If an exhaustive search does not report such a violation, it is
        !          1695: certain that \f2no\f1 execution execution sequence exists that can
        !          1696: violate the assertion.
        !          1697: .IH Options
        !          1698: .PP
        !          1699: The executable analyzer that is generated comes with a modest
        !          1700: number of options that can be checked as follows
        !          1701: .P1 0
        !          1702: $ run -?
        !          1703: -cN stop at Nth error (default=1)
        !          1704: -l  find non-progress loops
        !          1705: -mN max depth N (default=10k)
        !          1706: -wN hash table of 2^N entries (default=18)
        !          1707: .P2
        !          1708: Using a zero as an argument to the first option
        !          1709: forces the state space search to continue,
        !          1710: even if errors are found.
        !          1711: An overview of unexecutable (unreachable) code is given with every
        !          1712: complete run: either the default run if it did not find any
        !          1713: errors, or the run with option
        !          1714: .CW -c0 .
        !          1715: In this case the output is:
        !          1716: .P1 0
        !          1717: $ run -c0
        !          1718: assertion violated (i == (last_i + 1))
        !          1719: assertion violated (i == (last_i + 1))
        !          1720: assertion violated (i == (last_i + 1))
        !          1721: assertion violated (i == (last_i + 1))
        !          1722: assertion violated (i == (last_i + 1))
        !          1723: .P3
        !          1724: vector 64 byte, depth reached 60, errors: 5
        !          1725:      165 states, stored
        !          1726:        5 states, linked
        !          1727:       26 states, matched
        !          1728: hash conflicts: 1 (resolved)
        !          1729: (size 2^18 states, stack frames: 0/6)
        !          1730: 
        !          1731: unreached code :init: (proc 0):
        !          1732:        reached all 9 states
        !          1733: unreached code channel (proc 1):
        !          1734:         line 35 (state 9),
        !          1735:        reached: 8 of 9 states
        !          1736: unreached code transfer (proc 2):
        !          1737:         line 24 (state 18),
        !          1738:        reached: 17 of 18 states
        !          1739: .P2
        !          1740: There were five assertion violations, and some 165 unique
        !          1741: system states were generated.
        !          1742: Each state description (the \f2vector size\f1) took up 64 bytes
        !          1743: of memory; the longest non-cyclic execution sequence was 60.
        !          1744: There is one unreachable state both in the channel process and in
        !          1745: the transfer process.
        !          1746: In both cases the unreachable state is the control flow point
        !          1747: just after the do-loop in each process.
        !          1748: Note that both loops are indeed meant to be non-terminating.
        !          1749: .PP
        !          1750: The \f(CW-l\f1 option will cause the analyzer to search for
        !          1751: non-progress loops rather than deadlocks or assertion violations.
        !          1752: The option is explained in the section on ``More Advanced Usage.''
        !          1753: .PP
        !          1754: The executable analyzer has two other options.
        !          1755: By default the search depth is restricted to a rather
        !          1756: arbitrary 10,000 steps.
        !          1757: If the depth limit is reached, the search is truncated, making
        !          1758: the validation less than exhaustive.
        !          1759: To make certain that the search is exhaustive, make sure that the
        !          1760: "depth reached" notice is within the maximum search depth, and
        !          1761: if not, repeat the analysis with an explicit
        !          1762: .CW -m
        !          1763: argument.
        !          1764: .PP
        !          1765: The
        !          1766: .CW -m
        !          1767: option can of course also be used to truncate
        !          1768: the search explicitly, in an effort to find the shortest possible
        !          1769: execution sequence that violates a given assertion.
        !          1770: Such a truncated search, however, is not guaranteed to find every
        !          1771: possible violation, even within the search depth.
        !          1772: .PP
        !          1773: The last option
        !          1774: .CW -w\fIN
        !          1775: can only affect the run time, not
        !          1776: the scope, of an analysis with a full state space.
        !          1777: This "hash table width" should normally be set equal to,
        !          1778: or preferably higher than,
        !          1779: the logarithm of the expected number of unique system states generated
        !          1780: by the analyzer.
        !          1781: (If it is set too low, the number of hash collisions will increase
        !          1782: and slow down the search.)
        !          1783: The default
        !          1784: .I N
        !          1785: of 18 handles up to 262,144 system states, which should
        !          1786: suffice for almost all applications of a full state space analysis.
        !          1787: .IH "Bit State Space Analysis"
        !          1788: .PP
        !          1789: It can easily be calculated what the memory requirements of an analysis
        !          1790: with a full state space are|reference(holzmann atttj).
        !          1791: If, as in the example we have used, the protocol requires 64 bytes
        !          1792: of memory to encode one system state, and we have a total of 2MB
        !          1793: of memory available for the search, we can store up to 32,768 states.
        !          1794: The analysis fails if there are more reachable states in the
        !          1795: system state space.
        !          1796: So far, \*s is the \f2only\f1 validation system that can avoid this trap.
        !          1797: All other existing automated validation system (irrespective on
        !          1798: which formalism they are based) simply run out of memory and
        !          1799: abort their analysis without returning a useful answer to the user.
        !          1800: .PP
        !          1801: The coverage of a conventional analysis goes down rapidly when
        !          1802: the memory limit is hit, i.e. if there are
        !          1803: twice as many states in the full state space than we can store,
        !          1804: the effective coverage of the search is only 50% and so on.
        !          1805: \*S does substantially better in those cases by using the bit state
        !          1806: space storage method|reference(holzmann atttj).
        !          1807: The bit state space can be included by compiling the analyzer as follows:
        !          1808: .P1 0
        !          1809: $ cc -DBITSTATE -o run pan.c
        !          1810: .P2
        !          1811: The analyzer compiled in this way
        !          1812: should of course find the same assertion violation again:
        !          1813: .P1 0
        !          1814: $ run
        !          1815: assertion violated (i == ((last_i + 1))
        !          1816: pan: aborted
        !          1817: pan: wrote pan.trail
        !          1818: search interrupted
        !          1819: vector 64 byte, depth reached 56
        !          1820:       61 states, stored
        !          1821:        5 states, linked
        !          1822:        1 states, matched
        !          1823: hash factor: 67650.064516
        !          1824: (size 2^22 states, stack frames: 0/5)
        !          1825: $ 
        !          1826: .P2
        !          1827: In fact, for small to medium size problems there is very little
        !          1828: difference between the full state space method and the bit state
        !          1829: space method (with the exception that the latter is somewhat
        !          1830: faster and uses substantially less memory).
        !          1831: The big difference comes for larger problems.
        !          1832: The last two lines in the output are useful in estimating
        !          1833: the \f2coverage\f1 of a large run.
        !          1834: The maximum number of states that the bit state space can
        !          1835: accommodate is written on the last line (here @2 sup 22@ bytes or about 32 million
        !          1836: bits = states).
        !          1837: The line above it gives the \f2hash factor\f1: roughly
        !          1838: equal to the maximum number of states divided by the actual
        !          1839: number of states.
        !          1840: A large hash factor (larger than 100) means, with high reliability,
        !          1841: a coverage of 99% or 100%.
        !          1842: As the hash factor approaches 1 the coverage approaches 0%.
        !          1843: .PP
        !          1844: Note carefully that the analyzer realizes a partial coverage \f2only\f1
        !          1845: in cases where traditional validators are either unable to perform a
        !          1846: search, or realize a far smaller coverage.
        !          1847: In \f2no\f1 case will \*s produce an answer that is less reliable than
        !          1848: that produced by other automated validation systems (quite on the contrary).
        !          1849: .PP
        !          1850: The object of a bit state validation is to achieve a hash factor
        !          1851: larger than 100 by allocating the maximum amount of memory
        !          1852: for the bit state space.
        !          1853: For the best result obtainable: use the
        !          1854: .CW -w\fIN
        !          1855: option to size the state space to precisely the amount
        !          1856: of real (not virtual) memory available on your machine.
        !          1857: By default,
        !          1858: .I N
        !          1859: is 22, corresponding to a state space of 4MB.
        !          1860: For example, if your machine has 128MB of real memory, you can use
        !          1861: .CW -w27
        !          1862: to analyze systems with up to a billion reachable states.
        !          1863: .SP 2
        !          1864: .NH
        !          1865: \*P Reference Manual
        !          1866: .PP
        !          1867: This section describes the language \*P proper.
        !          1868: As much as possible, the presentation follows the example
        !          1869: from the
        !          1870: .CW C
        !          1871: reference manuals|reference(cbook).
        !          1872: It does not cover possible restrictions or extensions of
        !          1873: specific implementations.
        !          1874: The current implementation of \*s, for instance,
        !          1875: has an extra keyword
        !          1876: .CW printf ,
        !          1877: to access the corresponding
        !          1878: .UX
        !          1879: library function.
        !          1880: .IH "Lexical Conventions"
        !          1881: .PP
        !          1882: There are five classes of tokens: identifiers, keywords, constants,
        !          1883: operators and statement separators.
        !          1884: Blanks, tabs, newlines, and comments serve only to separate tokens.
        !          1885: If more than one interpretation is possible, a token is
        !          1886: taken to be the longest string of characters that can
        !          1887: constitute a token.
        !          1888: .ix lexical conventions
        !          1889: .ix tokens
        !          1890: .IH Comments
        !          1891: .PP
        !          1892: Any string started with
        !          1893: .CW /*
        !          1894: and terminated with
        !          1895: .CW */
        !          1896: is a comment.
        !          1897: Comments may not be nested.
        !          1898: .ix comments
        !          1899: .IH Identifiers
        !          1900: .PP
        !          1901: An identifier is a single letter, period, or underscore
        !          1902: followed by zero or more letters, digits, periods, or underscores.
        !          1903: .ix identifiers
        !          1904: .IH Keywords
        !          1905: .PP
        !          1906: The following identifiers are reserved for use as keywords:
        !          1907: .ix keywords
        !          1908: .KS
        !          1909: .ft CW
        !          1910: .ps -1
        !          1911: .vs -1
        !          1912: .TS
        !          1913: center;
        !          1914: l l l.
        !          1915: assert atomic  bit
        !          1916: bool   break   byte
        !          1917: chan   do      fi
        !          1918: goto   if      init
        !          1919: int    len     mtype
        !          1920: never  printf  od
        !          1921: of     proctype        run
        !          1922: short  skip    timeout
        !          1923: .ps +1
        !          1924: .vs +1
        !          1925: .TE
        !          1926: .KE
        !          1927: .IH Constants
        !          1928: .PP
        !          1929: A constant is a sequence of digits representing a decimal integer.
        !          1930: There are no floating point numbers in \*P.
        !          1931: .ix constants
        !          1932: Symbolic names for constants can be defined in two ways.
        !          1933: The first method is to use a C-style macro definition
        !          1934: .P1 0
        !          1935: #define        NAME    value
        !          1936: .P2
        !          1937: The second method is to use the keyword
        !          1938: .CW mtype
        !          1939: (see ``declarations'' below).
        !          1940: .IH Expressions
        !          1941: .PP
        !          1942: The following operators can be used to build expressions.
        !          1943: .ix expressions
        !          1944: .ix operators
        !          1945: .KS
        !          1946: .TS
        !          1947: center;
        !          1948: lFCW.
        !          1949: + \- * \/ %
        !          1950: > >= < <= == != !
        !          1951: && ||
        !          1952: & | ~ >> <<
        !          1953: .TE
        !          1954: .KE
        !          1955: .PP
        !          1956: Most operators are binary.
        !          1957: The logical negation \f2!\f1 and the minus \f2\-\f1
        !          1958: operator can be both unary and binary, depending on context.
        !          1959: Expressions are used, for instance, in assignments of the type
        !          1960: .CW "a = expression" ,
        !          1961: with
        !          1962: .CW a
        !          1963: a variable.
        !          1964: .ix assignment
        !          1965: There is also one unary operator that applies to message channels:
        !          1966: .P1 0
        !          1967: len
        !          1968: .P2
        !          1969: It measures the number of messages an existing channel holds.
        !          1970: There is one unary operator that is used for process instantiations:
        !          1971: .P1 0
        !          1972: run
        !          1973: .P2
        !          1974: And, finally, there are two binary operators
        !          1975: .P1 0
        !          1976: ! ?
        !          1977: .P2
        !          1978: which are used for sending and receiving messages (see below).
        !          1979: .IH Declarations
        !          1980: .PP
        !          1981: .ix declarations
        !          1982: Processes, channels, and variables must be declared before they can be used.
        !          1983: Variables and channels can be declared either locally,
        !          1984: within a process, or globally.
        !          1985: A process can only be declared globally in a
        !          1986: .CW proctype
        !          1987: declaration.
        !          1988: Local declarations may appear anywhere in a process body.
        !          1989: .IH Variables
        !          1990: .PP
        !          1991: .ix variables
        !          1992: .ix local variables
        !          1993: .ix global variables
        !          1994: .ix initializers
        !          1995: A variable declaration is started by a keyword indicating the
        !          1996: basic data type of the variable,
        !          1997: .CW bit ,
        !          1998: .CW bool ,
        !          1999: .CW byte ,
        !          2000: .CW short ,
        !          2001: or
        !          2002: .CW int ,
        !          2003: followed
        !          2004: by one or more identifiers, optionally followed by
        !          2005: an initializer.
        !          2006: .P1 0
        !          2007: byte name1, name2 = 4, name3
        !          2008: .P2
        !          2009: By default all variables are initialized to zero.
        !          2010: An initializer, if specified, must be a constant.
        !          2011: The table below summarizes the width and attributes of each
        !          2012: basic data type.
        !          2013: .KS
        !          2014: .ps -1
        !          2015: .vs -2
        !          2016: .TS
        !          2017: center;
        !          2018: l l l
        !          2019: lFCW n r.
        !          2020: =
        !          2021: Name   Size (bits)     Usage
        !          2022: _
        !          2023: bit    1       unsigned
        !          2024: bool   1       unsigned
        !          2025: byte   8       unsigned
        !          2026: short  16      signed
        !          2027: int    32      signed
        !          2028: _
        !          2029: .TE
        !          2030: .ps +1
        !          2031: .vs +2
        !          2032: .KE
        !          2033: The names \f2bit\f1 and \f2bool\f1
        !          2034: are synonyms for a single bit of
        !          2035: information.
        !          2036: A \f2byte\f1 is an unsigned quantity that can store a value between
        !          2037: 0 and 255.
        !          2038: \f2Short\f1s and \f2int\f1s are signed quantities that
        !          2039: differ only in the range of values they can hold.
        !          2040: .PP
        !          2041: An array of variables is declared as follows:
        !          2042: .P1 0
        !          2043: int name1[N]
        !          2044: .P2
        !          2045: where
        !          2046: .CW N
        !          2047: is a constant.
        !          2048: An array can have a just a single constant as an initializer.
        !          2049: If specified it is used to initialize all elements of the array.
        !          2050: .PP
        !          2051: Symbolic names for constants, e.g. message types,
        !          2052: can, optionally, be defined in a declaration
        !          2053: of the type
        !          2054: .P1 0
        !          2055: mtype = { namelist }
        !          2056: .P2
        !          2057: where
        !          2058: .CW namelist
        !          2059: is a comma separated list of symbolic names.
        !          2060: .IH "Message Channels"
        !          2061: .PP
        !          2062: A message channel can be declared, for instance, as follows:
        !          2063: .ix channels
        !          2064: .P1 0
        !          2065: chan name[N] of { short, short }
        !          2066: .P2
        !          2067: where
        !          2068: .CW N
        !          2069: is a constant that specifies the maximum number of messages
        !          2070: that can be stored in the channel.
        !          2071: A list of one or more data types (or the channel type
        !          2072: .CW chan )
        !          2073: enclosed in curly braces defines the type of the messages that can
        !          2074: be passed through the channel.
        !          2075: All channels are initialized to be empty.
        !          2076: .IH Processes
        !          2077: .PP
        !          2078: .ix process
        !          2079: A process declaration starts with the keyword
        !          2080: .CW proctype
        !          2081: followed by a name, a list of formal parameters
        !          2082: enclosed in round braces, and
        !          2083: a sequence of statements and local
        !          2084: variable declarations.
        !          2085: The body of process declaration is enclosed in curly braces.
        !          2086: .P1 0
        !          2087: proctype name( /* parameter decls */ )
        !          2088: {
        !          2089:        /* statements */
        !          2090: }
        !          2091: .P2
        !          2092: .IH Statements
        !          2093: .PP
        !          2094: .ix statements
        !          2095: .ix gotos
        !          2096: .ix labels
        !          2097: .ix skip
        !          2098: There are twelve types of statements:
        !          2099: .KS
        !          2100: .TS
        !          2101: center;
        !          2102: a a a.
        !          2103: .ft CW
        !          2104: .ps -1
        !          2105: .vs -1
        !          2106: assertion      assignment      atomic
        !          2107: break  declaration     expression
        !          2108: goto   receive selection
        !          2109: repetition     send    timeout
        !          2110: .ft
        !          2111: .ps +1
        !          2112: .vs +1
        !          2113: .TE
        !          2114: .KE
        !          2115: Each statement may be preceded by a label: a name followed by a colon.
        !          2116: A statement can only be passed if it is executable.
        !          2117: To determine its executability the statement can be evaluated:
        !          2118: if evaluation returns a zero value the statement is blocked.
        !          2119: In all other cases the statement is executable and can be passed.
        !          2120: The act of passing the statement after a successful evaluation is
        !          2121: called the ``execution'' of the statement.
        !          2122: There is one so-called \fIpseudo\fR-statements
        !          2123: .CW skip ,
        !          2124: a null statement equivalent to \(CW(1)\f1; it is always executable.
        !          2125: It has no effect when executed, but may be needed
        !          2126: to satisfy syntax requirements.
        !          2127: The evaluation of an assertion statement
        !          2128: .CW assert(condition)
        !          2129: has no effect if the condition holds, but aborts the
        !          2130: running process if evaluation of the condition returns a
        !          2131: zero result (the boolean value ``false'').
        !          2132: .PP
        !          2133: .CW goto
        !          2134: statements can be used to transfer control to any labeled statement
        !          2135: within the same process or procedure.
        !          2136: They also are always executable.
        !          2137: Assignments have been discussed above, they are
        !          2138: always executable.
        !          2139: A declaration is also always executable.
        !          2140: Expressions are only executable if they return a non-zero value.
        !          2141: That is, the expression \(CW0\fR (zero) is never executable, and
        !          2142: similarly \(CW1\fR always is executable.
        !          2143: Below we consider the remaining statements: selection, repetition,
        !          2144: send, receive, break, timeout, and atomic statements.
        !          2145: .IH Selection
        !          2146: .PP
        !          2147: .ix if statement
        !          2148: .ix case selection
        !          2149: .ix nondeterminism
        !          2150: A selection statement is started with the keyword
        !          2151: .CW if ,
        !          2152: followed by
        !          2153: a list of one or more `options' and terminated with the keyword
        !          2154: .CW fi .
        !          2155: Every `option' is started with the flag \f(CW::\fR followed by any sequence
        !          2156: of statements.
        !          2157: One and only one option from a selection statement will
        !          2158: be selected for execution.
        !          2159: The first statement of an option determines
        !          2160: whether the option can be selected or not.
        !          2161: If more than one option is executable, one will be selected at random.
        !          2162: Note that this randomness makes the language a nondeterministic one.
        !          2163: .IH "Repetition and Break"
        !          2164: .PP
        !          2165: .ix do statement
        !          2166: .ix repetition
        !          2167: A repetition or
        !          2168: .CW do
        !          2169: statement is similar to a selection statement, but is executed
        !          2170: repeatedly until either a
        !          2171: .CW break
        !          2172: statement is executed or a
        !          2173: .CW goto
        !          2174: jump will transfer control outside the cycle.
        !          2175: The keywords of the repetition statement are
        !          2176: .CW do
        !          2177: and
        !          2178: .CW od
        !          2179: instead of the
        !          2180: .CW if
        !          2181: and
        !          2182: .CW fi
        !          2183: of selection.
        !          2184: The
        !          2185: .CW break
        !          2186: statement will terminate the innermost repetition
        !          2187: statement in which it is executed.
        !          2188: The use of a \(CWbreak\fR statement outside a
        !          2189: repetition statement is illegal.
        !          2190: ......
        !          2191: .IH "Atomic Sequences"
        !          2192: .PP
        !          2193: The keyword
        !          2194: .CW atomic
        !          2195: introduces an atomic sequence of statements, that is
        !          2196: to be executed as one indivisible step.
        !          2197: The syntax is as follows
        !          2198: .P1 0
        !          2199: atomic { sequence }
        !          2200: .P2
        !          2201: Logically the sequence of statements is now equivalent
        !          2202: to one single statement.
        !          2203: It is a run-time error if any statement that is part of an
        !          2204: atomic sequence is found to be unexecutable.
        !          2205: The safest is therefore to include only assignments and
        !          2206: local conditions in atomic sequences, but no sends or receives.
        !          2207: Labeling local computations as atomic can bring an important
        !          2208: reduction of the complexity of a validation model.
        !          2209: For the lazy, \*s has an option (\f(CW-q\f1) that tries to find
        !          2210: the most obvious ``atomicable'' sequences in the code,
        !          2211: but the user can often do better by hand.
        !          2212: .IH Send
        !          2213: .PP
        !          2214: .ix i/o statements
        !          2215: .ix send
        !          2216: The syntax of a send statement is:
        !          2217: .P1 0
        !          2218: expr1!expr2
        !          2219: .P2
        !          2220: where
        !          2221: .CW expr1
        !          2222: returns the identity of a channel, e.g. obtained from a
        !          2223: .CW chan
        !          2224: operation, and
        !          2225: .CW expr2
        !          2226: returns a value to be appended to the channel.
        !          2227: The send statement is not executable (blocks) if the addressed channel is full
        !          2228: or does not exist.
        !          2229: .ix value transfer
        !          2230: If more than one value is to be passed from sender to receiver, the expressions
        !          2231: are written in a comma separated list:
        !          2232: .P1 0
        !          2233: expr1!expr2,expr3,expr4
        !          2234: .P2
        !          2235: Equivalently, this may be written
        !          2236: .P1 0
        !          2237: expr1!expr2(expr3,expr4) .
        !          2238: .P2
        !          2239: .IH Receive
        !          2240: .PP
        !          2241: .ix i/o statements
        !          2242: .ix receive
        !          2243: .ix value transfer
        !          2244: The syntax of the receive statement is:
        !          2245: .P1 0
        !          2246: expr1?name
        !          2247: .P2
        !          2248: where
        !          2249: .CW expr1
        !          2250: returns the name of a channel and
        !          2251: .CW name
        !          2252: is a variable or a constant.
        !          2253: If a constant is specified the receive statement is only executable
        !          2254: if the channel exists and
        !          2255: the oldest message stored in the channel contains the same value.
        !          2256: If a variable is specified, the receive statement is executable
        !          2257: if the channel exists and contains any message at all.
        !          2258: The variable in that case will receive the value of the message
        !          2259: that is retrieved.
        !          2260: If more than one value is sent per message, the receive statement
        !          2261: also take a comma separated list of variables and constants
        !          2262: .P1 0
        !          2263: expr1?name1,name2,...
        !          2264: .P2
        !          2265: which again is syntactically equivalent to
        !          2266: .P1 0
        !          2267: expr1?name1(name2,...)
        !          2268: .P2
        !          2269: Each constant in this list puts an extra condition on the
        !          2270: executability of the receive: it must be matched by the
        !          2271: value of the corresponding message field of the
        !          2272: message to be retrieved.
        !          2273: The variable fields retrieve the values of the corresponding
        !          2274: message fields on a receive.
        !          2275: .PP
        !          2276: Placing square brackets around the clause after the `?'
        !          2277: in the receiver operation converts it into a condition,
        !          2278: that is true only if the corresponding receive operation
        !          2279: is executable.
        !          2280: It can be used freely in any type of composite boolean condition,
        !          2281: and it has no side-effects when evaluated.
        !          2282: .PP
        !          2283: A last type of operation allowed on channels is
        !          2284: .P1 0
        !          2285: len(expr)
        !          2286: .P2
        !          2287: where
        !          2288: .CW expr
        !          2289: returns the identity of an instantiated channel.
        !          2290: The operation returns the number of messages in
        !          2291: the channel specified, or zero if the channel does not exist.
        !          2292: .IH Timeout
        !          2293: .PP
        !          2294: The timeout condition is a modeling feature that by definition becomes true
        !          2295: only if no statement in any of the running processes is executable.
        !          2296: It has no effect when executed.
        !          2297: .IH "Macros and Include Files"
        !          2298: .PP
        !          2299: .ix macros
        !          2300: .ix include files
        !          2301: .ix preprocessor
        !          2302: The source text of a specification is processed by the C|reference(cbook)
        !          2303: preprocessor for macro-expansion and file inclusions.
        !          2304: .NH
        !          2305: Summary
        !          2306: .PP
        !          2307: In the first part of this memo
        !          2308: we have introduced a notation for modeling concurrent
        !          2309: systems, including but not limited to asynchronous
        !          2310: data communication protocols, in a language named \*P.
        !          2311: The language has several unusual features.
        !          2312: All communication between processes takes
        !          2313: place via either messages or shared variables.
        !          2314: Both synchronous and asynchronous communication
        !          2315: are modeled as two special cases of a general message
        !          2316: passing mechanism.
        !          2317: Every statement in \*P can potentially model delay: it is
        !          2318: either executable or not, in most cases depending on the state
        !          2319: of the environment of the running process.
        !          2320: Process interaction and process coordination is thus at
        !          2321: the very basis of the language.
        !          2322: More about the design of \*P, of the validator \*s, and
        !          2323: its application to protocol design, can be found in |reference(holzmann spinbook).
        !          2324: .PP
        !          2325: \*P is deliberately a validation modeling language, not a programming language.
        !          2326: There are, for instance, no elaborate abstract data types,
        !          2327: or more than a few basic types of variable.
        !          2328: A validation model is an abstraction of a protocol implementation.
        !          2329: The abstraction maintains the essentials of the process interactions,
        !          2330: so that it can be studied in isolation.
        !          2331: It suppresses implementation and programming detail.
        !          2332: .PP
        !          2333: The syntax of \*P expressions, declarations, and assignments
        !          2334: is loosely based on the language
        !          2335: .CW C |reference(cbook).
        !          2336: The language was influenced significantly by the ``guarded command languages''
        !          2337: of E.W. Dijkstra |reference(dijkstra guarded) and C.A.R. Hoare
        !          2338: |reference(hoare csp).
        !          2339: There are, however, important differences.
        !          2340: Dijkstra's language had no primitives for process interaction.
        !          2341: Hoare's language was based exclusively on synchronous
        !          2342: communication.
        !          2343: Also in Hoare's language, the type
        !          2344: of statements that could appear in the guards of an option was
        !          2345: restricted.
        !          2346: The semantics of the selection and cycling statements
        !          2347: in \*P is also rather different from other guarded
        !          2348: command languages: the statements are not aborted when all guards
        !          2349: are false but they block: thus providing the required synchronization.
        !          2350: .PP
        !          2351: With minimal effort \*s allows the user to generate sophisticated
        !          2352: analyzers from \*P validation models.
        !          2353: Both the \*s software itself, and the analyzers it can generate,
        !          2354: are written in ANSII C and are portable across
        !          2355: .UX
        !          2356: systems.
        !          2357: They can be scaled to fully exploit the physical limitations
        !          2358: of the host computer, and deliver within those
        !          2359: limits the best possible analyses that can be realized
        !          2360: with the current state of the art in protocol analysis.
        !          2361: .NH
        !          2362: References
        !          2363: .LP
        !          2364: |reference_placement
        !          2365: .af H1 A
        !          2366: .nr H1 1
        !          2367: .nr H2 0
        !          2368: .SH
        !          2369: Appendix: Building A Validation Suite
        !          2370: .PP
        !          2371: The first order of business in using \*s for
        !          2372: a validation is the construction of a
        !          2373: faithful model in \*P of the problem at hand.
        !          2374: The language is deliberately kept small.
        !          2375: The purpose of the modeling is to extract those
        !          2376: aspects of the system that are relevant to the
        !          2377: coordination problem being studied.
        !          2378: All other details are suppressed.
        !          2379: Formally: the model is a reduction of the
        !          2380: system that needs to be equivalent to the full system
        !          2381: only with respect to the properties that are being validated.
        !          2382: Once a model has been constructed, it becomes
        !          2383: the basis for the construction of a series of,
        !          2384: what we may call, ``validation suites'' that
        !          2385: are used to verify its properties.
        !          2386: To build a validation suite we can prime the
        !          2387: model with assertions.
        !          2388: The assertions can formalize invariant relations
        !          2389: about the values of variables or about allowable
        !          2390: sequences of events in the model.
        !          2391: .NH 2
        !          2392: An Example
        !          2393: .PP
        !          2394: As a first example we take the following solution
        !          2395: to the mutual exclusion problem, discussed earlier,
        !          2396: published in 1966 by H. Hyman in the Communications of the ACM.
        !          2397: It was listed, in pseudo Algol, as follows.
        !          2398: .P1 0
        !          2399:   1 \f3Boolean array\f2 b(0;1) \f3integer\f2 k, i,\f(CW
        !          2400:   2 \f3comment\f2 process i, with i either 0 or 1;\f(CW
        !          2401:   3 \f2C0:     b(i) := \f3false\f2;\f(CW
        !          2402:   4 \f2C1:     \f3if\f2 k != i \f3then begin\f2\f(CW
        !          2403:   5 \f2C2:     \f3if\f2 not (b(1-i) \f3then go to\f2 C2;\f(CW
        !          2404:   6    \f3else\f2 k := i; \f3go to\f2 C1 \f3end\f2;\f(CW
        !          2405:   7    \f3else\f2 critical section;\f(CW
        !          2406:   8    \f2b(i) := \f3true\f2;\f(CW
        !          2407:   9    \f2remainder of program;\f(CW
        !          2408:  10    \f3go to\f2 C0;\f(CW
        !          2409:  11    \f3end\f(CW
        !          2410: .P2
        !          2411: The solution, as Dekker's earlier solution, is for two processes,
        !          2412: numbered 0 and 1.
        !          2413: Suppose we wanted to prove that Hyman's solution truly
        !          2414: guaranteed mutually exclusive access to the critical section.
        !          2415: Our first task is to build a model of the solution in \*P.
        !          2416: While we're at it, we can pick some more useful names for
        !          2417: the variables that are used.
        !          2418: .P1 0
        !          2419:    1  bool want[2];    /* Bool array b */
        !          2420:    2  bool turn;       /* integer    k */
        !          2421:    3  
        !          2422: .P3
        !          2423:    4  proctype P(bool i)
        !          2424:    5  {
        !          2425:    6   want[i] = 1;
        !          2426: .P3
        !          2427:    7   do
        !          2428:    8   :: (turn != i) ->
        !          2429:    9           (!want[1-i]);
        !          2430:   10           turn = i
        !          2431: .P3
        !          2432:   11   :: (turn == i) ->
        !          2433:   12           break
        !          2434:   13   od;
        !          2435: .P3
        !          2436:   14   skip; /* critical section */
        !          2437:   15   want[i] = 0
        !          2438:   16  }
        !          2439: .P3
        !          2440:   17  
        !          2441: .P3
        !          2442:   18  init { run P(0); run P(1) }
        !          2443: .P2
        !          2444: We can generate, compile, and run a validator for this
        !          2445: model, to see if there are any major problems, such as
        !          2446: a global system deadlock.
        !          2447: .P1 0
        !          2448: $ spin -a hyman0
        !          2449: $ cc pan.c
        !          2450: $ a.out
        !          2451: full statespace search for:
        !          2452: assertion violations and invalid endstates
        !          2453: vector 20 byte, depth reached 19, errors: 0
        !          2454:       79 states, stored
        !          2455:        0 states, linked
        !          2456:       38 states, matched       total: 117
        !          2457: hash conflicts: 4 (resolved)
        !          2458: (size 2^18 states, stack frames: 3/0)
        !          2459: 
        !          2460: unreached code _init (proc 0):
        !          2461:        reached all 3 states
        !          2462: unreached code P (proc 1):
        !          2463:        reached all 12 states
        !          2464: .P2
        !          2465: The model passes this first test.
        !          2466: What we are really interested in, however, is if
        !          2467: the algorithm guarantees mutual exclusion.
        !          2468: There are several ways to proceed.
        !          2469: The simplest is to just add enough information
        !          2470: to the model that we can express the correctness
        !          2471: requirement in a \*P assertion.
        !          2472: .P1 0
        !          2473:    1  bool want[2];
        !          2474:    2  bool turn;
        !          2475:    3  byte cnt;
        !          2476:    4  
        !          2477: .P3
        !          2478:    5  proctype P(bool i)
        !          2479:    6  {
        !          2480: .P3
        !          2481:    7   want[i] = 1;
        !          2482: .P3
        !          2483:    8   do
        !          2484:    9   :: (turn != i) ->
        !          2485:   10           (!want[1-i]);
        !          2486:   11           turn = i
        !          2487: .P3
        !          2488:   12   :: (turn == i) ->
        !          2489:   13           break
        !          2490:   14   od;
        !          2491:   15   skip; /* critical section */
        !          2492: .P3
        !          2493:   16   cnt = cnt+1;
        !          2494:   17   assert(cnt == 1);
        !          2495:   18   cnt = cnt-1;
        !          2496:   19   want[i] = 0
        !          2497:   20  }
        !          2498: .P3
        !          2499:   21  
        !          2500: .P3
        !          2501:   22  init { run P(0); run P(1) }
        !          2502: .P2
        !          2503: We have added a global variable
        !          2504: .CW cnt
        !          2505: that is incremented upon each access to the
        !          2506: critical section, and decremented upon each exit
        !          2507: from it.
        !          2508: The maximum value that this variable should ever
        !          2509: have is 1, and it can only have this value when
        !          2510: a process is inside the critical section.
        !          2511: .P1 0
        !          2512: $ spin -a hyman1
        !          2513: $ cc pan.c
        !          2514: $ a.out
        !          2515: assertion violated (cnt==1)
        !          2516: pan: aborted (at depth 15)
        !          2517: pan: wrote pan.trail
        !          2518: full statespace search for:
        !          2519: assertion violations and invalid endstates
        !          2520: search was not completed
        !          2521: vector 20 byte, depth reached 25, errors: 1
        !          2522:      123 states, stored
        !          2523:        0 states, linked
        !          2524:       55 states, matched       total: 178
        !          2525: hash conflicts: 42 (resolved)
        !          2526: (size 2^18 states, stack frames: 3/0)
        !          2527: .P2
        !          2528: The validator claims that the assertion can be violated.
        !          2529: We can use the error trail to check it with \*s's \f(CW-t\f1 option:
        !          2530: .P1 0
        !          2531: $ spin -t -p hyman1
        !          2532: proc  0 (_init)        line 24 (state 2)
        !          2533: proc  0 (_init)        line 24 (state 3)
        !          2534: .P3
        !          2535: proc  2 (P)    line 8 (state 7)
        !          2536: proc  2 (P)    line 9 (state 2)
        !          2537: .P3
        !          2538: proc  2 (P)    line 10 (state 3)
        !          2539: proc  2 (P)    line 11 (state 4)
        !          2540: .P3
        !          2541: proc  1 (P)    line 8 (state 7)
        !          2542: proc  1 (P)    line 12 (state 5)
        !          2543: .P3
        !          2544: proc  1 (P)    line 15 (state 10)
        !          2545: proc  2 (P)    line 8 (state 7)
        !          2546: .P3
        !          2547: proc  2 (P)    line 12 (state 5)
        !          2548: proc  2 (P)    line 15 (state 10)
        !          2549: .P3
        !          2550: proc  2 (P)    line 16 (state 11)
        !          2551: proc  2 (P)    line 17 (state 12)
        !          2552: .P3
        !          2553: proc  2 (P)    line 18 (state 13)
        !          2554: proc  1 (P)    line 16 (state 11)
        !          2555: .P3
        !          2556: proc  1 (P)    line 17 (state 12)
        !          2557: spin: "hyman1" line 17: assertion violated
        !          2558: .P3
        !          2559: step 17, #processes: 3
        !          2560:                want[0] = 1
        !          2561:                _p[0] = 12
        !          2562:                turn[0] = 1
        !          2563:                cnt[0] = 2
        !          2564: .P3
        !          2565: proc  2 (P)    line 18 (state 13)
        !          2566: proc  1 (P)    line 17 (state 12)
        !          2567: proc  0 (_init)        line 24 (state 3)
        !          2568: 3 processes created
        !          2569: .P2
        !          2570: Here is another way to catch the error.
        !          2571: We again lace the model with the information that
        !          2572: will allow us to count the number of processes
        !          2573: in the critical section.
        !          2574: .P1 0
        !          2575:    1  bool want[2];
        !          2576:    2  bool turn;
        !          2577:    3  byte cnt;
        !          2578:    4  
        !          2579: .P3
        !          2580:    5  proctype P(bool i)
        !          2581:    6  {
        !          2582:    7   want[i] = 1;
        !          2583: .P3
        !          2584:    8   do
        !          2585:    9   :: (turn != i) ->
        !          2586:   10           (!want[1-i]);
        !          2587:   11           turn = i
        !          2588: .P3
        !          2589:   12   :: (turn == i) ->
        !          2590:   13           break
        !          2591:   14   od;
        !          2592: .P3
        !          2593:   15   cnt = cnt+1;
        !          2594:   16   skip;   /* critical section */
        !          2595:   17   cnt = cnt-1;
        !          2596:   18   want[i] = 0
        !          2597:   19  }
        !          2598: .P3
        !          2599:   20  
        !          2600: .P3
        !          2601:   21  proctype monitor()
        !          2602:   22  {
        !          2603:   23   assert(cnt == 0 || cnt == 1)
        !          2604:   24  }
        !          2605: .P3
        !          2606:   25  
        !          2607: .P3
        !          2608:   26  init {
        !          2609:   27   run P(0); run P(1); run monitor()
        !          2610:   28  }
        !          2611: .P2
        !          2612: The invariant condition on the value of counter
        !          2613: .CW cnt
        !          2614: is now place in a separate process
        !          2615: .CW monitor()
        !          2616: (the name is immaterial).
        !          2617: The extra process runs along with the two others.
        !          2618: It will always terminate in one step, but it
        !          2619: could execute that step at \f2any\f1 time.
        !          2620: The systems modeled by \*P and validated by \*s
        !          2621: are completely asynchronous.
        !          2622: That means that the validation of \*s take into
        !          2623: account \f2all\f1 possible relative timings of
        !          2624: the three processes.
        !          2625: In a full validation, the assertion therefore
        !          2626: can be evaluated at any time during the lifetime
        !          2627: of the other two processes.
        !          2628: If the validator reports that it is not violated
        !          2629: we can indeed conclude that there is no execution
        !          2630: sequence at all (no way to select relative speeds for
        !          2631: the three processes) in which the assertion can be
        !          2632: violated.
        !          2633: The setup with the monitor process is therefore an
        !          2634: elegant way to check the validity of a system invariant.
        !          2635: The validation produces:
        !          2636: .P1 0
        !          2637: $ spin -a hyman2
        !          2638: $ cc pan.c
        !          2639: $ a.out
        !          2640: assertion violated ((cnt==0)||(cnt==1))
        !          2641: pan: aborted (at depth 15)
        !          2642: pan: wrote pan.trail
        !          2643: full statespace search for:
        !          2644: assertion violations and invalid endstates
        !          2645: search was not completed
        !          2646: vector 24 byte, depth reached 26, errors: 1
        !          2647:      368 states, stored
        !          2648:        0 states, linked
        !          2649:      379 states, matched       total: 747
        !          2650: hash conflicts: 180 (resolved)
        !          2651: (size 2^18 states, stack frames: 4/0)
        !          2652: .P2
        !          2653: Because of the extra interleaving of the two processes
        !          2654: with a third monitor, the number of system states that
        !          2655: had to be searched has increased, but the error is again
        !          2656: correctly reported.
        !          2657: .br
        !          2658: .NE 8v
        !          2659: .NH 2
        !          2660: Another Example
        !          2661: .PP
        !          2662: Not always can a correctness requirement be cast in
        !          2663: terms of a global system invariant.
        !          2664: Here is an example that illustrates this.
        !          2665: It is a simple alternating bit protocol, modeling
        !          2666: the possibility of message loss, and distortion,
        !          2667: and extended with negative acknowledgements.
        !          2668: .P1 0
        !          2669:    1  #define MAX      5
        !          2670:    2  
        !          2671:    3  mtype = { mesg, ack, nak, err };
        !          2672:    4  
        !          2673: .P3
        !          2674:    5  proctype sender(chan in, out)
        !          2675:    6  {        byte o, s, r;
        !          2676:    7  
        !          2677:    8   o=MAX-1;
        !          2678:    9   do
        !          2679:   10   :: o = (o+1)%MAX; /* next msg */
        !          2680:   11  again: if
        !          2681:   12         :: out!mesg(o,s) /* send */
        !          2682:   13         :: out!err(0,0)  /* distort */
        !          2683:   14         :: skip       /* or lose */
        !          2684:   15         fi;
        !          2685: .P3
        !          2686:   16         if
        !          2687:   17         :: timeout   -> goto again
        !          2688:   18         :: in?err(0,0) -> goto again
        !          2689:   19         :: in?nak(r,0) -> goto again
        !          2690:   20         :: in?ack(r,0) ->
        !          2691:   21           if
        !          2692:   22           :: (r == s) -> goto progress
        !          2693:   23           :: (r != s) -> goto again
        !          2694:   24           fi
        !          2695:   25         fi;
        !          2696:   26  progress:        s = 1-s /* toggle seqno */
        !          2697:   27   od
        !          2698:   28  }
        !          2699:   29  
        !          2700: .P3
        !          2701:   30  proctype receiver(chan in, out)
        !          2702:   31  {        byte i;         /* actual input   */
        !          2703:   32   byte s;         /* actual seqno   */
        !          2704:   33   byte es;        /* expected seqno */
        !          2705:   34   byte ei;        /* expected input */
        !          2706:   35  
        !          2707:   36   do
        !          2708:   37   :: in?mesg(i, s) ->
        !          2709:   38           if
        !          2710:   39           :: (s == es) ->
        !          2711:   40                   assert(i == ei);
        !          2712:   41  progress:                es = 1 - es;
        !          2713:   42                   ei = (ei + 1)%MAX;
        !          2714:   43                   if
        !          2715:   44   /* send,   */   :: out!ack(s,0)
        !          2716:   45   /* distort */   :: out!err(0,0)
        !          2717:   46   /* or lose */   :: skip
        !          2718:   47                   fi
        !          2719: .P3
        !          2720:   48           :: (s != es) ->
        !          2721: .P3
        !          2722:   49                   if
        !          2723: .P3
        !          2724:   50   /* send,   */   :: out!nak(s,0)
        !          2725:   51   /* distort */   :: out!err
        !          2726:   52   /* or lose */   :: skip
        !          2727: .P3
        !          2728:   53                   fi
        !          2729: .P3
        !          2730:   54           fi
        !          2731:   55   :: in?err(0,0) ->
        !          2732:   56           out!nak(s,0)
        !          2733: .P3
        !          2734:   57   od
        !          2735:   58  }
        !          2736:   59  
        !          2737: .P3
        !          2738:   60  init {
        !          2739: .P3
        !          2740:   61   chan s_r [1] of { byte,byte,byte };
        !          2741:   62   chan r_s [1] of { byte,byte,byte };
        !          2742: .P3
        !          2743:   63   atomic {
        !          2744: .P3
        !          2745:   64           run sender(r_s, s_r);
        !          2746:   65           run receiver(s_r, r_s)
        !          2747: .P3
        !          2748:   66   }
        !          2749: .P3
        !          2750:   67  }
        !          2751: .P2
        !          2752: To test the proposition that this protocol will
        !          2753: correctly transfer data, the model has already
        !          2754: been primed for the first validation runs.
        !          2755: First, the sender is setup to transfer an infinite
        !          2756: series of integers as messages, where the value
        !          2757: of the integers are incremented modulo
        !          2758: .CW MAX .
        !          2759: The value of
        !          2760: .CW MAX
        !          2761: is not really too interesting, as long as it is
        !          2762: larger than the range of the sequence numbers in
        !          2763: the protocol: in this case 2.
        !          2764: We want to verify that data that is sent can only be
        !          2765: delivered to the receiver without any deletions or reorderings,
        !          2766: despite the possibility of arbitrary message loss.
        !          2767: The assertion on line 40 verifies precisely that.
        !          2768: Note that if it were ever possible for the protocol to
        !          2769: fail to meet the above requirement, the assertion can be violated.
        !          2770: .PP
        !          2771: A first validation run reassures us that this is not possible.
        !          2772: .P1 0
        !          2773: $ spin -a ABP0
        !          2774: $ cc pan.c
        !          2775: $ a.out
        !          2776: full statespace search for:
        !          2777: assertion violations and invalid endstates
        !          2778: vector 40 byte, depth reached 131, errors: 0
        !          2779:      346 states, stored
        !          2780:        1 states, linked
        !          2781:      125 states, matched        total: 472
        !          2782: hash conflicts: 17 (resolved)
        !          2783: (size 2^18 states, stack frames: 0/25)
        !          2784: 
        !          2785: unreached code _init (proc 0):
        !          2786:        reached all 4 states
        !          2787: unreached code receiver (proc 1):
        !          2788:        line 58 (state 24)
        !          2789:        reached: 23 of 24 states
        !          2790: unreached code sender (proc 2):
        !          2791:        line 28 (state 27)
        !          2792:        reached: 26 of 27 states
        !          2793: .P2
        !          2794: But, be careful.
        !          2795: The result means that all data that is delivered, is
        !          2796: delivered in the correct order without deletions etc.
        !          2797: We did not check that the data \f2will\f1 necessarily be delivered.
        !          2798: It may be possible for sender and receiver to cycle
        !          2799: through a series of states, exchanges erroneous messages,
        !          2800: without ever making effective progress.
        !          2801: To check this, the state in the sender and in the receiver
        !          2802: process that unmistakingly signify progress, were labeled
        !          2803: as a ``progress states.''
        !          2804: (In fact, either one by itself would suffice.)
        !          2805: .PP
        !          2806: We should now be able to demonstrate the absence of
        !          2807: infinite execution cycles that do not pass through any
        !          2808: of these progress states.
        !          2809: We can use the same executable from the last run, but
        !          2810: this time we perform a loop-check.
        !          2811: .P1 0 
        !          2812: $  a.out -l
        !          2813: pan: non-progress cycle (at depth 6)
        !          2814: pan: wrote pan.trail
        !          2815: full statespace search for:
        !          2816: assertion violations and non-progress loops
        !          2817: search was not completed
        !          2818: vector 44 byte, depth reached 8, loops: 1
        !          2819:       12 states, stored
        !          2820:        1 states, linked
        !          2821:        0 states, matched       total: 13
        !          2822: hash conflicts: 0 (resolved)
        !          2823: (size 2^18 states, stack frames: 0/1)
        !          2824: .P2
        !          2825: There are non-progress cycles.
        !          2826: The first one encountered is dumped into the error trail
        !          2827: by the validator, and we can inspect it.
        !          2828: The results are shown in the first half of Figure 2.
        !          2829: The channel can distort or lose the message infinitely often;
        !          2830: true, but not too exciting as an error scenario.
        !          2831: To see how many non-progress cycles there are, we can use the \f(CW-c\f1 flag.
        !          2832: If we set its numeric argument to zero, only
        !          2833: a total count of all errors will be printed.
        !          2834: .P1 0
        !          2835: $ a.out -l -c0
        !          2836: full statespace search for:
        !          2837: assertion violations and non-progress loops
        !          2838: vector 44 byte, depth reached 137, loops: 92
        !          2839:      671 states, stored
        !          2840:        2 states, linked
        !          2841:      521 states, matched        total: 1194
        !          2842: hash conflicts: 39 (resolved)
        !          2843: (size 2^18 states, stack frames: 0/26)
        !          2844: .P2
        !          2845: There are 92 cases to consider, and we could look at each
        !          2846: one, using the \f(CW-c\f1 option (\f(CW-c1\f1, \f(CW-c2\f1, \f(CW-c3\f1, ...etc.)
        !          2847: But, we can make the job a little easier by at least
        !          2848: filtering out the errors caused by infinite message loss.
        !          2849: We label all loss events (lines 13, 43, and 48) as
        !          2850: progress states, using label names with the common 8-character
        !          2851: prefix ``progress,'' and look at the cycles that remain.
        !          2852: (Labels go behind the ``::'' flags.)
        !          2853: .P1 0
        !          2854: $ spin -a ABP1
        !          2855: $ cc pan.c
        !          2856: .P3
        !          2857: $ a.out -l
        !          2858: pan: non-progress cycle (at depth 133)
        !          2859: pan: wrote pan.trail
        !          2860: .P3
        !          2861: full statespace search for:
        !          2862: assertion violations and non-progress loops
        !          2863: search was not completed
        !          2864: .P3
        !          2865: vector 44 byte, depth reached 136, loops: 1
        !          2866: .P3
        !          2867:      148 states, stored
        !          2868:        2 states, linked
        !          2869:        2 states, matched        total: 152
        !          2870: .P3
        !          2871: hash conflicts: 0 (resolved)
        !          2872: (size 2^18 states, stack frames: 0/26)
        !          2873: .P2
        !          2874: This time, the trace reveals an honest and a serious bug in the protocol.
        !          2875: The second half of Figure 2 shows the trace-back.
        !          2876: .1C
        !          2877: .KF
        !          2878: .nf
        !          2879: .ps -2
        !          2880: .vs -3p
        !          2881: .ft CW
        !          2882: .TS
        !          2883: box expand;
        !          2884: l
        !          2885: l.
        !          2886:       $ spin -t -r -s ABP0
        !          2887:       <<<<<START OF CYCLE>>>>>
        !          2888:       proc  1 (sender)   line  13, Send err,0,0 -> queue 2 (out)
        !          2889:       proc  2 (receiver) line  55, Recv err,0,0 <- queue 2 (in)
        !          2890:       proc  2 (receiver) line  56, Send nak,0,0 -> queue 1 (out)
        !          2891:       proc  1 (sender)   line  19, Recv nak,0,0 <- queue 1 (in)
        !          2892:       spin: trail ends after 12 steps
        !          2893:       step 12, #processes: 3
        !          2894:                _p[0] = 6
        !          2895:       proc  2 (receiver)       line 36 (state 21)
        !          2896:       proc  1 (sender) line 11 (state 6)
        !          2897:       proc  0 (_init)  line 67 (state 4)
        !          2898:       3 processes created
        !          2899:       $ 
        !          2900:       $ spin -t -r -s ABP1
        !          2901:       \&...
        !          2902:       proc  2 (receiver) line  39, Recv mesg,0,0 <- queue 2 (in)
        !          2903:       proc  2 (receiver) line  47, Send err,0,0  -> queue 1 (out)
        !          2904:       proc  1 (sender)   line  20, Recv err,1,0  <- queue 1 (in)
        !          2905:       proc  1 (sender)   line  12, Send mesg,0,0 -> queue 2 (out)
        !          2906:       proc  2 (receiver) line  39, Recv mesg,0,0 <- queue 2 (in)
        !          2907:       proc  2 (receiver) line  52, Send nak,0,0  -> queue 1 (out)
        !          2908:       proc  1 (sender)   line  21, Recv nak,0,0  <- queue 1 (in)
        !          2909:       proc  1 (sender)   line  12, Send mesg,0,0 -> queue 2 (out)
        !          2910:       proc  2 (receiver) line  39, Recv mesg,0,0 <- queue 2 (in)
        !          2911:       proc  2 (receiver) line  52, Send nak,0,0  -> queue 1 (out)
        !          2912:       <<<<<START OF CYCLE>>>>>
        !          2913:       proc  1 (sender)   line  21, Recv nak,0,0  <- queue 1 (in)
        !          2914:       proc  1 (sender)   line  12, Send mesg,0,0 -> queue 2 (out)
        !          2915:       proc  2 (receiver) line  39, Recv mesg,0,0 <- queue 2 (in)
        !          2916:       proc  2 (receiver) line  52, Send nak,0,0  -> queue 1 (out)
        !          2917:       spin: trail ends after 226 steps
        !          2918:       \&...
        !          2919: .TE
        !          2920: .fi
        !          2921: .ps +2
        !          2922: .vs +3p
        !          2923: .SP .5
        !          2924: .ce
        !          2925: \fBFigure 2.\fR  Error Trails - Extended Alternating Bit Protocol
        !          2926: .SP .5
        !          2927: .KE
        !          2928: .2C
        !          2929: .PP
        !          2930: After a single positive acknowledgement is distorted
        !          2931: and transformed into an
        !          2932: .CW err
        !          2933: message, sender and receiver get caught in an infinite
        !          2934: cycle, where the sender will stubbornly repeat the last
        !          2935: message for which it did not receive an acknowledgement,
        !          2936: and the receiver, just as stubbornly, will reject that
        !          2937: message with a negative acknowledgment.
        !          2938: .NH 2
        !          2939: Digging Deeper
        !          2940: .PP
        !          2941: This manual can only give an outline of the
        !          2942: main features of \*s, and the more common
        !          2943: ways in which it can be used for validations.
        !          2944: There is a small number of \*s features that
        !          2945: have not been discussed here, but that may be useful
        !          2946: for tackling non-standard validation problems.
        !          2947: \*S, for instance, can give \*P processes access
        !          2948: to extra system information, such as the current
        !          2949: values of normally invisible local variables,
        !          2950: or the current execution states of remote processes.
        !          2951: With this extra information it may be easier in
        !          2952: some cases to build accurate assertions about
        !          2953: required system behavior.
        !          2954: .PP
        !          2955: \*S also allows for a straightforward validation of ``tasks.''
        !          2956: That is, if the user formalizes a task that is claimed to be
        !          2957: performed by the system, \*s can quickly either prove or
        !          2958: disprove that claim.
        !          2959: The tasks can be used directly to verify any
        !          2960: propositional temporal logic formula
        !          2961: on the behavior of a system.
        !          2962: .PP
        !          2963: \*S also allows the user to formalize ``reductions'' of
        !          2964: the system state space, which can be used
        !          2965: to restrict a search it to a user defined subset.
        !          2966: With this method it becomes trivial to verify quickly
        !          2967: whether or not a given error pattern is within the range of
        !          2968: behaviors of a system, even when a complete validation is
        !          2969: considered to be infeasible.
        !          2970: .PP
        !          2971: For details about these alternative uses of \*P and
        !          2972: the \*s software, refer to [5].

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