- 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
Control Flow: Compound Statements
So far, we have mainly focused on the basic statements of PROMELA, and the way in which they can be combined to model process behavior. The main types of statements we have mentioned so far are: print and assignment statements, expressions, and send and receive statements.
We saw that run is an operator, which makes a statement such as run sender() an expression. Similarly, skip is not a statement but an expression: it is equivalent to (1) or true.
There are five types of compound statements in PROMELA:
-
Atomic sequences
-
Deterministic steps
-
Selections
-
Repetitions
-
Escape sequences
Another control flow structuring mechanism is available through the definition of macros and PROMELA inline functions. We discuss these constructs in the remaining subsections of this chapter.