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