Promela Reference -- Skip(1)

`Skip(1)`

NAME
skip - shorthand for a dummy, nill statement.

SYNTAX
skip

DESCRIPTION
The keyword skip is a meta-term that is translated by the Spin lexical analyzer into the Boolean constant 1 , i.e., into true . This means that skip could be used as part of an expression. It's intended use is, however, stand-alone, as if it were a statement. In this case, the skip is interpreted as a condition statement (see condition(4)). This condition statement is always executable, and has no effect, other than to change the control-state of the process that executes it.

EXAMPLES
There are few cases where a skip statement is needed to satisfy syntax requirements. A common use is to make it possible to place a label at the end of a statement sequence , to allow a goto jump (see goto(3)) to that point. Because only statements can be prefixed by a label, we must use a dummy skip statement as a place-holder:

proctype A()

{

L0:	if

	:: cond1 -> goto L1	/* jump to the end of the sequence */

	:: else -> skip		/* the "-> skip" is redundant here */

	fi;



	...



L1:	skip

}

One is tempted to use also a skip statement after the else guard in the first selection structure above, to indicate that processing is to continue at the control state that immediately follows the selection construct. This is harmless, but redundant. The above selection could be written more tersely as:

L0:	if

	:: cond1 -> goto L1

	:: else

	fi;

Because Promela is an asynchronous language, the skip is never needed to introduce delay in process executions. In Promela there is by definition an arbitrary, and unknowable, delay in between any two statements in a proctype body. If control reaches a statement, and that statement is and remains executable, the only thing known is that the statement will be executed within a finite period of time. This corresponds to Dijkstra's finite progress assumption for concurrent systems, and it respects the rule that no assumptions may be made about the relative execution speeds of asynchronous processes. The only possible exception to this rule may be to influence the outcome of random simulations by using redundant skip statements.

NOTES
The opposite of skip would be the condition statement (0) , which would never be executable. Early versions of Spin indeed contained the keyword halt with this interpretation. Newer versions of Spin, however, do not. In cases where a halt might be needed, often an assert(4) statement is more effective, e.g., assert(false) , or assert(0) .

The skip short-hand is an equivalent of true , and halt , if it existed, would be the equivalent of false .

Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage (Page Updated: 16 December 1997)

`Promela`

`Meta Terms`

`Skip(1)`