- Types of Objects
- Processes
- Provided Clauses
- Data Objects
- Data Structures
- Message Channels
- Channel Poll Operations
- Sorted Send And Random Receive
- Rendezvous Communication
- Rules For Executability
- Assignments And Expressions
- Control Flow: Compound Statements
- Atomic Sequences
- Deterministic Steps
- Selection
- Repetition
- Escape Sequences
- Inline Definitions
- Reading Input
- Special Features
- Finding Out More
This chapter is from the book
This chapter is from the book
This chapter is from the book
Escape Sequences
The last type of compound structure to be discussed is the unless statement. This type of statement is used less frequently, but it requires a little more explanation. It is safe to skip this section on a first reading.
The syntax of an escape sequence is as follows:
{ P } unless { E }
where the letters P and E represent arbitrary PROMELA fragments. Execution of the unless statement begins with the execution of statements from P. Before each statement execution in P the executability of the first statement of E is checked, using the normal PROMELA semantics of executability. Execution of statements from P proceeds only while the first statement of E remains unexecutable. The first time that this ’guard of the escape sequence’ is found to be executable, control changes to it, and execution continues as defined for E. Individual statement executions remain indivisible, so control can only change from inside P to the start of E in between individual statement executions. If the guard of the escape sequence does not become executable during the execution of P, then it is skipped entirely when P terminates.
An example of the use of escape sequences is:
A;
do
:: b1 -> B1
:: b2 -> B2
...
od unless { c -> C };
D
As shown in the example, the curly braces around the main sequence (or the escape sequence) can be deleted if there can be no confusion about which statements belong to those sequences. In the example, condition c acts as a watchdog on the repetition construct from the main sequence. Note that this is not necessarily equivalent to the construct
A; do :: b1 -> B1 :: b2 -> B2 ... :: c -> break od; C; D
if B1 or B2 are non-empty. In the first version of the example, execution of the iteration can be interrupted at any point inside each option sequence. In the second version, execution can only be interrupted at the start of the option sequences.
An example application of an escape sequence is shown in Figure 3.1. Shown here is a somewhat naive model of the behavior of a pots ( plain old telephone service) system (cf. Chapter 14, p. 299).
Figure 3.1 Simple Model of a Telephone System
mtype = { offhook, dialtone, number, ringing,
busy, connected, hangup, hungup };
chan line = [0] of { mtype, chan };
active proctype pots()
{ chan who;
idle: line?offhook,who;
{ who!dialtone;
who?number;
if
:: who!busy; goto zombie
:: who!ringing ->
who!connected;
if
:: who!hungup; goto zombie
:: skip
fi
fi
} unless
{ if
:: who?hangup -> goto idle
:: timeout -> goto zombie
fi
}
zombie: who?hangup; goto idle
}
active proctype subscriber()
{ chan me = [0] of { mtype };
idle: line!offhook,me;
me?dialtone;
me!number;
if
:: me?busy
:: me?ringing ->
if
:: me?connected;
if
:: me?hungup
:: timeout
fi
:: skip
fi
fi;
me!hangup; goto idle
}
There are two processes in this system, a subscriber and the pots server. The subscriber process follows a strict regimen. After going offhook it always waits for a dial tone, and it always sends a number to be connected to when the dial tone message is received. After that it waits to receive either a busy or a ring tone. On seeing a busy tone, our idealized subscriber process hangs up and tries the call again. On seeing a ring tone, it either waits for the signal that the call is connected, or it impatiently hangs up. When connected, it waits for notification from the pots server that the remote party has disconnected the call, but if this does not come, it can timeout and terminate the call anyway.
The model of the subscriber behavior is fairly standard, requiring no unusual control-flow constructs. We can be more creative in modeling the pots server. The server process starts in its idle state by waiting for a subscriber to send an offhook signal together with the channel via which it wants to communicate with the server for this session. The server always complies by sending a dial tone, and then waits for the number to be dialed. Once the number has been received, either a busy tone or a ring tone is chosen, matching the subscriber’s expectations at this point in the call. A ring tone is followed by a connected signal, and after this the server process proceeds to the zombie state where it waits for the subscriber to hangup the phone, possibly, but not necessarily sending a hungup message first. Note that the skip and the goto zombie statements lead to the same next state in this case (meaning that the goto is really redundant here).
Note that we have not included any treatment for a subscriber hangup message in this main flow of the pots behavior. The reason is that we would like to model the fact that the behavior of the pots server can be interrupted at any point in this flow if a hangup message should unexpectedly arrive. Similarly, if the pots server gets stuck at any point in its flow, it should be possible to define a timeout option, without spelling out that very same option at any point in the main flow where the server could possibly get stuck. The escape clause of the unless construct spells out the two conditions under which the main flow should be aborted, and gives the actions that must be taken in each case. After a hangup, the server simply returns to its idle state, since it knows that the subscriber is back onhook. After a timeout, it moves to the zombie state.
A fragment of the output for a SPIN simulation run for this system follows. The run can in principle be continued ad infinitum, so it is prudent to filter the output from SPIN through a utility like more. The first two full executions, starting and ending with both processes in their idle state, look as follows:
$ spin -c pots.pml | more proc 0 = pots proc 1 = subscriber q\p 0 1 2 . line!offhook,1 2 line?offhook,1 1 who!dialtone 1 . me?dialtone 1 . me!number 1 who?number 1 who!ringing 1 . me?ringing 1 who!connected 1 . me?connected timeout 1 . me!hangup 1 who?hangup 2 . line!offhook,1 2 line?offhook,1 1 who!dialtone 1 . me?dialtone 1 . me!number 1 who?number 1 who!ringing 1 . me?ringing 1 . me!hangup 1 who?hangup
There are no surprises here. The model, though, cannot properly be called a verification model just yet. For that, we would have to add some statement of the requirements or properties that we would like this model to satisfy. We may well ask, for instance, if it is possible for the server to get stuck permanently in the zombie state. Only a verification run can give the answer to such questions.