Promela Reference -- skip(1)


Meta Term


skip - shorthand for a dummy, nil statement.


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.


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: 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).

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)