- 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
Selection
Using the relative values of two variables a and b we can define a choice between the execution of two different options with a selection structure, as follows:
if :: (a != b) -> option1 :: (a == b) -> option2 fi
The selection structure above contains two execution sequences, each preceded by a double colon. Only one sequence from the list will be executed. A sequence can be selected only if its first statement, that is, the first statement that follows the double colon, is executable. The first statement is therefore called the guard of the option sequence.
In the last example the guards are mutually exclusive, but they need not be. If more than one guard is executable, one of the corresponding sequences is selected nondeterministically. If all guards are unexecutable the process will block until at least one of them can be selected. There is no restriction on the type of statements that can be used as a guard: it may include sends or receives, assignments, printf, skip, etc. The rules of executability determine in each case what the semantics of the complete selection structure will be. The following example, for instance, illustrates the use of send statements as guards in a selection.
mtype = { a, b };
chan ch = [1] of { mtype };
active proctype A() { ch?a }
active proctype B() { ch?b }
active proctype C()
{ if
:: ch!a
:: ch!b
fi
}
The example defines three processes and one channel. The first option in the selection structure of the process of type C is executable if channel ch is non-full, a condition that is satisfied in the initial state. Since both guards are executable, the process of type C can arbitrarily pick one, and execute it, depositing a message in channel ch. The process of type A can execute its sole statement if the message sent was an a, where a is a symbolic constant defined in the mtype declaration at the start of the model. Its peer process of type B can execute its sole statement if the message is of type b, where, similarly, b is a symbolic constant.
If we switch all send statements for receive statements, and vice versa, we also get a valid PROMELA model. This time, the choice in C is forced by the message that gets sent into the channel, which in turn depends on the unknown relative speeds of execution of the processes of type A and B. In both versions of the model, one of the three running processes hangs at the end of system execution, and will fail to terminate.
A process of the following type either increments or decrements the value of variable count. Because assignments are always executable, the choice made here is truly a non-deterministic one that is independent of the initial value of the variable count.
byte count; /* initial value defaults to zero */
active proctype counter()
{
if
:: count++
:: count--
fi
}