Promela |
Meta Terms |
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 .
SEE ALSO
false(1), true(1), assert(4), condition(4), else(5).
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |