NAME
never - for declaring a temporal claim and standard Büchi acceptance.

SYNTAX
never { sequence }

DESCRIPTION
Any valid Promela fragment can in principle appear inside a never claim sequence, but it violates the purpose of the temporal claims to use any statement that can have side effects on the system state. This rules out assignments, and message send or receive operations, but preserves all control-flow constructs and all conditional expressions, including all boolean channel poll operations.

The sequence of statements that defines the never claim is normally composed entirely of propositions (boolean expressions) on the global system state.

A Promela model defines an asynchronous interleaving product of the concurrent behaviors of all processes. A temporal claim allows for the specification of precise correctness claims about the types of execution sequences that are expected or allowed to be part of this interleaving product. The temporal claim makes a formal statement of the possible orders in which propositions on the reachable system states can become true and false during system execution.

To achieve this, the statements in a never claim are used to follow or monitor the executions of the system. The following is achieved by having the verifier compute a synchronous (instead of an asynchronous) product of the sequence specified in the temporal claim, with the interleaving sequences specified in the remainder of the system. This synchronous product can be thought of as the construction of a new automaton, in which every state is defined as a pair (s,n) with s a state from the global system, and n a state from the temporal claim. Every transition in the new automaton is similarly defined by a pair of transitions, with the first element a statement from the system, and the second a proposition from the claim. In other words, every transition in this final synchronous product is defined as a joint transition of the system and the claim. Of course, that transition can only occur if the proposition from the second half of the transition pair evaluates to true in the first half of the state pair in the source state of the transition.

Starting from the initial system state, the never claim will move before any step in the system is taken (this is necessary to make sure we can evaluate a proposition for the initial system state itself). Consider, for instance, the following little program (with thanks to Rob Gerth):

byte aap;



proctype noot()

{

mies:

	skip

}



init {

	aap = run noot()

}



never {

	do

	:: noot[aap]@mies -> break

	:: else

	od

}

never {

	true;	/* or 'skip' */

	do

	:: noot[aap]@mies -> break

	:: else

	od

}

Note that it is not allowed to try to shortcut this method by attempting:

byte aap = run noot();	/* invalid global initialization */

Never claims can be difficult to produce manually, especially claims that are closed under stuttering, as is required to preserve the correct operation of Spin's builtin partial order reduction algorithm. The recommended use is therefore to specify all temporal claims as LTL formulae, and to use Spin's builtin algorithm to convert these into never claim.

Special variables and operators that are reserved for us in never claims are: _last , np_ , pc_value() , enabled() , and remoterefs .

EXAMPLES
To translate an LTL formula into a never claim, we have to consider first whether the formula expresses a positive or a negative property. A positive property expresses a good behavior that we would like our system to have. A negative property expresses a bad behavior that we claim the system does not have. A never claim can expresses only a negative claim, which means that positive claims must be negated before they can be translated into a claim.

Suppose that the LTL formula <>[] p , with p a boolean expression, expresses a negative claim (i.e., it is considered a correctness violation if there exists any execution sequence in which eventually p can remain true infinitely long). This can be written in a never claim as:

never {	/* <>[]p */

	do

	:: skip	/* <> = after an arbitrarily long prefix */

	:: p -> break	/* p becomes true */

	od;

accept:	do

	:: p	/* and remains true forever after */

	od

}

If the LTL formula expressed a positive property, we first have to invert it to the corresponding negative property. For instance, if we claim that, immediately from the initial state forward the value of p must remain true, the negation is: ![]p which can be translated into a never claim. The requirement says that it is a violation if p eventually becomes false (does not always remain true).

never {	/* ![]p = <>!p*/

	do

	:: skip

	:: !p -> break

	od

}

never {

	do

	:: p

	:: !p -> break

	od

}

never { do :: assert(p) od }

NOTES
Never claims can be used to specify a Büchi automaton, and the matching of the behavior specified in a never claim can formally be defined as standard Büchi acceptance. Büchi acceptance, though, is defined only over infinite execution sequences, not finite ones. Since Promela models can also express properties of terminating system behaviors, we have to define the semantics of the never claims also for those behaviors. Spin uses standard stuttering semantics to define the mapping from terminating executions to pseudo-infinite ones. In effect this means that the final state of any terminating system execution is thought to persist forever, and repeated with a dummy self-loop. As a further syntactical convenience, the final state of the never claim itself is defined to be accepting, i.e., it abbreviates the iteration:

accept: do :: skip od

It is good practice to confine the use of accept labels to never claims, and to generate never claims from LTL formulae directly.

SEE ALSO
ltl(1), accept(2), notrace(2), trace(2), _last(5), enabled(5), np_(5), pc_value(5), remoterefs(5).