Promela Reference -- timeout(5)

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.

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.

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:

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