Promela |
Predefined |
timeout |
NAME
timeout -
a predefined, global, read-only, boolean variable.
SYNTAX
timeout
DESCRIPTION
Timeout is a predefined, global, read-only, boolean variable
that is true in all global system states where no
statement is executable in any active process,
and otherwise is false.
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.
EXAMPLES
The first example shows how
timeout can be used to implement a watchdog process that sends
a reset message to a channel named
guard each time the system enters a hang state.
active proctype watchdog() { do :: timeout -> guard!reset od }A more traditional use is to place a timeout as an alternative to a potentially blocking statement, to guard against a system deadlock if the statement becomes permanently blocked.
do :: q?message -> ... :: timeout -> break od
NOTES
The
timeout statement can not specify a timeout interval.
Timeout s are used to model only possible
system behaviors, not detailed real-time behavior.
To model premature expiration of timers, consider
replacing the
timeout variable with the constant value
true , for instance, as in:
#define timeout trueA timeout can be combined with other expressions to form more complex wait conditions, but can not be combined with else . Note that timeout , if used as a condition statement, can be considered to be a system level else statement. Where the else statement becomes executable only when no other statements within the executing process can be executed, a timeout statement becomes executable only when no other statements anywhere in the system can be executed.
SEE ALSO
condition
do
else
if
unless
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 28 November 2004) |