Promela Reference -- skip(1)

`skip`

NAME
skip - shorthand for a dummy, nil statement.

SYNTAX
skip

DESCRIPTION
The keyword skip is a meta term that is translated by the Spin lexical analyzer into the constant value one (1), just like the predefined boolean constant true . The intended use of the shorthand is stand-alone, as a dummy statement. When used as a statement, the skip is interpreted as a special case of a condition statement. This condition statement is always executable, and has no effect when executed, other than a possible change of the control-state of the executing process.

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 for a goto jump to that point. Because only statements can be prefixed by a label, we must use a dummy skip statement as a placeholder in those cases.

EXAMPLES

proctype A()
{
L0:	if
	:: cond1 -> goto L1 /* jump to end    */
	:: else -> skip     /* skip redundant */
	fi;

	...

L1:	skip
}

The skip statement that follows label L1 is required in this example. The use of the skip statement following the else guard in the selection structure above is redundant. The above selection can be written more tersely as:

L0:	if
	:: cond1 -> goto L1
	:: else
	fi;

Because Promela is an asynchronous language, the skip is never needed, nor effective, to introduce delay in process executions. In Promela, by definition, there can always be an arbitrary, and unknowable, delay between any two subsequent statement executions in a proctype body. This semantics correspond to the golden rule of concurrent systems design that forbids assumptions about the relative execution speed of asynchronous processes in a concurrent system.

When Spin's weak fairness constraint is enforced we can tighten this semantics a little, to conform to, what is known as, Dijkstra's finite progress assumption. In this case, when control reaches a statement, and that statement is and remains executable, we can are allowed to assume that the statement will be executed within a finite period of time (i.e., we can exclude the case where the delay would be infinite).

NOTES
The opposite of skip is the zero condition statement (0) , which is never executable. In cases where such a blocking statement might be needed, often an assertion statement is more effective. Note that assert(false) and assert(0) are equivalent. Similarly, assert(true) and assert(1) are equivalent and indistinguishable from both assert(skip) and skip .

Because skip is intercepted in the lexical analyzer as a meta term, it does not appear literally in error traces. It will only show up as its numeric equivalent (1).

Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage (Page updated: 28 November 2004)

`Promela`

`Meta Term`

`skip`