Promela |
Predefined |
timeout(5) |
NAME
timeout
-
a system defined condition.
SYNTAX
timeout
DESCRIPTION
Timeout
can be considered to be a predefined global read-only variable,
that has the value
true
in all global system states where no
statement is executable in any active process, and
false
in all other states (see
Intro(0)).
A timeout , used as a guard in a selection or repetition construct, provides an escape from a system hang state. It allows a process to abort waiting for a condition that can no longer become true, for example, an input from an empty channel.
EXAMPLES
L1: do :: q?message -> &... :: timeout -> break od; L2: &...The following example uses timeout to implement a watchdog process that sends a reset message to a channel named guard each time the system comes to a standstill.
active proctype watchdog()
{ do
:: timeout -> guard!reset
od
}
NOTES
The
timeout
statement carries no value: it does not specify a
timeout interval, but a timeout possibility.
The default
timeout
statement does not model the possibility of a
premature expiration of a timer in a real system.
If this is required, it can be achieved by redefining
the keyword in a macro definition, for instance as follows.
#define timeout skip
SEE ALSO
else(5).
|
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |