- 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
Repetition
We can modify the last model to obtain a cyclic program that randomly changes the value of the variable up or down by replacing the selection structure with a repetition.
byte count;
active proctype counter()
{
do
:: count++
:: count--
:: (count == 0) -> break
od
}
As before, only one option can be selected for execution at a time. After the option completes, the execution of the repetition structure is repeated. The normal way to terminate the repetition structure is with a break statement. In the example, the loop can be broken only when the count reaches zero. Note, however, that it need not terminate since the other two options always remain executable. To force termination we could modify the program as follows:
active proctype counter()
{
do
:: (count != 0) ->
if
:: count++
:: count--
fi
:: (count == 0) -> break
od
}
A special type of statement that is useful in selection and repetition structures is the else statement. An else statement becomes executable only if no other statement within the same process, at the same control-flow point, is executable. We could try to use it in two places in the example, as follows:
active proctype counter()
{
do
:: (count != 0) ->
if
:: count++
:: count--
:: else
fi
:: else -> break
od
}
The first else, inside the nested selection structure, can never become executable though, and is therefore redundant (both alternative guards of the selection are assignments, which are always executable). The second use of the else, however, becomes executable exactly when !(count != 0) or (count == 0), and therefore preserves the option to break from the loop.
There is also an alternative way to exit the do-loop, without using a break statement: the infamous goto. This is illustrated in the following PROMELA implementation of Euclid’s algorithm for finding the greatest common divisor of two non-zero, positive numbers.
proctype Euclid(int x, y)
{
do
:: (x > y) -> x = x - y
:: (x < y) -> y = y - x
:: (x == y) -> goto done
od;
done:
printf("answer: %d\n", x)
}
init { run Euclid(36, 12) }
Simulating the execution of this model, with the numbers given, yields:
$ spin euclid.pml
answer: 12
2 processes created
The goto in this example jumps to a label named done. Multiple labels may be used to label the same statement, but at least one statement is required. If, for instance, we wanted to omit the printf statement behind the label, we must replace it with a dummy skip. Like a skip, a goto statement is always executable and has no other effect than to change the control-flow point of the process that executes it.
With these extra constructs, we can now also define a slightly more complete description of the alternating bit protocol (cf. p. 46).
mtype = { msg, ack };
chan to_sndr = [2] of { mtype, bit };
chan to_rcvr = [2] of { mtype, bit };
active proctype Sender()
{ bool seq_out, seq_in;
do
:: to_rcvr!msg(seq_out) ->
to_sndr?ack(seq_in);
if
:: seq_in == seq_out ->
seq_out = 1 - seq_out;
:: else
fi
od
}
active proctype Receiver()
{ bool seq_in;
do
:: to_rcvr?msg(seq_in) ->
to_sndr!ack(seq_in)
:: timeout -> /* recover from msg loss */
to_sndr!ack(seq_in)
od
}
The sender transmits messages of type msg to the receiver, and then waits for an acknowledgement of type ack with a matching sequence number. If an acknowledgement with the wrong sequence number comes back, the sender retransmits the message. The receiver can timeout while waiting for a new message to arrive, and will then retransmit its last acknowledgement.
The semantics of PROMELA’s timeout statement is very similar to that of the else statement we saw earlier. A timeout is defined at the system level, though, and an else statement is defined at the process level. timeout is a predefined global variable that becomes true if and only if there are no executable statements at all in any of the currently running processes. The primary purpose of timeout is to allow us to model recovery actions from potential deadlock states. Note carefully that timeout is a predefined variable and not a function: it takes no parameters, and in particular it is not possible to specify a numeric argument with a specific timebound after which the timeout should become executable. The reason is that the types of properties we would like to prove for PROMELA models must be fully independent of all absolute and relative timing considerations. The relative speeds of processes is a fundamentally unknown and unknowable quantity in an asynchronous system.