--- /dev/null
+An appendix to Chapter 6 of the book: some extra explanation on pid's
+and on temporal claims. Updated for Spin Version 2.0 - January 1995.
+
+PROCESS IDs
+
+In Spin 2.0 and later the never claim can refer to the control state
+of any process, but not to their local variables.
+This functionality is meant to be used for building correctness assertions
+with never claims. It should never be used for anything else.
+An example is
+ Receiver[pid]@place
+where `place' the name of a label within `proctype Receiver,' and
+`pid' is the value returned by the run statement that instantiated the
+copy of the Receiver proctype that we are interested in.
+
+There is a misleading suggestion in the book that says that you can
+usually guess the `pid's. Wiser is to always use the explicit value
+returned by the `run()' statement that instantiated the proces.
+Processes started with the `active' prefix obtain instantiation
+numbers starting at value 1, in the order in which they appear in the
+specification. Each process also has a local variable _pid that
+holds its own instantiation number.
+
+SPECIFYING TEMPORAL CLAIMS
+
+The body of a temporal claim is defined just like PROMELA proctype bodies.
+This means that all control flow structures, such as if-fi selections,
+do-od repetitions, and goto jumps, are allowed.
+There is, however, one important difference:
+
+ Every statement inside a temporal claim is (interpreted as) a condition.
+ A never claim should therefore never contain statements that can
+ have side-effects (assignments, communications, run-statements, etc.)
+
+Temporal claims are used to express behaviors that are considered undesirable
+or illegal. We say that a temporal claim is `matched' if the undesirable
+behavior can be realized, and thus the claim violated.
+
+The recommended use of a temporal claim is in combination with acceptance labels.
+There are two ways to `match' a temporal claim, depending on whether the
+undesirable behavior defines a terminating or a cyclic execution sequence.
+
+o A temporal claim is matched when it terminates (reaches its closing curly brace).
+ That is, the claim can be violated if the closing curly brace of the PROMELA
+ body of the claim is reachable for at least one execution sequence.
+
+o For a cyclic execution sequence, the claim is matched only when an explicit
+ acceptance cycle exists. The acceptance labels within temporal claims
+ are user defined, there are no defaults. This means that in the absence of
+ acceptance labels no cyclic behavior can be matched by a temporal claim.
+ It also means that to check a cyclic temporal claim, acceptance labels should
+ only occur within the claim and not elsewhere in the PROMELA code.
+
+
+SEMANTICS
+
+The normal system behavior of a PROMELA system is defined as the
+`asynchronous product' of the behaviors of the individual processes.
+Given an arbitrary system state, its successor states are obtained
+in two steps. In the first step all the executable (atomic) statements in the
+individual processes are identified. In the second step, each one of these
+statements is executed.
+Each single execution produces a successor state in the asynchronous product.
+The complete system behavior is thus defined recursively and
+represents all possible interleavings of the individual process behaviors.
+Call this asynchronous product machine the `global machine'.
+
+The addition of a temporal claim defines an additional `synchronous product'
+of this global machine with the state machine that defines the temporal
+claim. Call the latter machine the `claim machine', and call the new
+synchronous product the `labeled machine'.
+
+Every state in the labeled machine is a pair (p,q) with p a state in the global
+machine and q a state in the claim machine. Every transition in the labeled
+machine is similarly defined by a pair (r,s) with r a transition in the global
+machine and s a transition in the claim machine.
+In other words, every transition in the `synchronous' product is a joint move
+of the global machine and the claim machine.
+(By contrast, every transition in an `asynchronous' product would correspond
+to a single transition in either the global machine or the claim machine, thus
+interleaving transitions instead of combining them.)
+
+Since all statements in the claim machine are boolean propositions, the second
+half of the transition pair (r,s) is either true or false.
+Call all transitions where this proposition is true `matching transitions'.
+In a matching transition proposition s evaluates to true in state system state r.
+Notice that the claim machine has at least one stop state E, the state
+at the closing curly brace of the claim body.
+
+The semantics of temporal claims can now be summed up as follows.
+
+o If the labeled machine contains any sequence of matching transitions only,
+ that connects its initial state with a state (p,E) for any p, the temporal
+ claim can be matched by a terminating sequence (a correctness violation).
+
+o If the labeled machine contains any cycle of matching transitions only, that
+ passes through an acceptance state, the temporal claim can be matched by a
+ cyclic sequence.
+
+
+EXAMPLES
+
+Listed below are the equivalent PROMELA definitions for the three basic
+temporal properties defined by Zohar Manna & Amir Pnueli in
+``Tools and Rules for the Practicing Verifier'' Stanford University,
+Report STAN-CS-90-1321, July 1990, 34 pgs.
+
+The following descriptions are quoted from Manna & Pnueli:
+
+ ``There are three classes of properties we [...] believe to cover
+ the majority of properties one would ever wish to verify.''
+
+ 1. Invariance
+ ``An invariance property refers to an assertion p, and requires that p
+ is an invariant over all the computations of a program P, i.e. all
+ the states arising in a computation of P satisfy p. In temporal
+ logic notation, such properties are expressed by [] p, for a state
+ formula p.''
+
+ Corresponding Temporal Claim in PROMELA:
+ never {
+ do
+ :: p
+ :: !p -> break
+ od
+ }
+
+ 2. Response
+ ``A response property refers to two assertions p and q, and
+ requires that every p-state (a state satisfying p) arising in
+ a computation is eventually followed by a q-state.
+ In temporal logic notation this is written as p -> <> q.''
+
+ Corresponding Temporal Claim in PROMELA:
+ never {
+ do
+ :: true
+ :: p && !q -> break
+ od;
+ accept:
+ do
+ :: !q
+ od
+ }
+
+ Note that using (!p || q) instead of `skip' would check only the
+ first occurrence of p becoming true while q is false.
+ The above formalization checks for all occurrences, also future ones.
+ Strictly seen, therefore, the claim above uses a common interpretation
+ of the formula, requiring it to hold always, or: [] { p -> <> q }
+
+ 3. Precedence
+ ``A simple precedence property refers to three assertions p, q, and r.
+ It requires that any p-state initiates a q-interval (i.e. an interval
+ all of whose states satisfy q) which, either runs to the end of the
+ computation, or is terminated by an r-state.
+ Such a property is useful to express the restriction that, following
+ a certain condition, one future event will always be preceded by
+ another future event.
+ For example, it may express the property that, from the time a certain
+ input has arrived, there will be an output before the next input.
+ Note that this does not guarantee [require] that the output will actually
+ be produced. It only guarantees [requires] that the next input (if any)
+ will be preceded by an output. In temporal logic, this property is
+ expressed by p -> (q U r), using the unless operator (weak until) U.
+
+ Corresponding Temporal Claim in PROMELA:
+
+ never {
+ do
+ :: skip /* to match any occurrence */
+ :: p && q && !r -> break
+ :: p && !q && !r -> goto error
+ od;
+ do
+ :: q && !r
+ :: !q && !r -> break
+ od;
+ error: skip
+ }
+
+ Strictly again, this encodes: [] { p -> (q U r) }
+ To match just the first occurence, replace skip with (!p || r).
projects / lttv.git / blobdiff