- 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
Reading Input
On an initial introduction to PROMELA it may strike one as odd that there is a generic output statement to communicate information to the user in the form of the printf, but there is no matching scanf statement to read information from the input. The reason is that we want verification models to be closed to their environment. A model must always contain all the information that could possibly be required to verify its properties. It would be rather clumsy, for instance, if the model checker would have to be stopped dead in its tracks each time it needed to read information from the userβs keyboard.
Outputs, like printf, are harmless in this context, since they generate no new information that can affect future behavior of the executing process, but the executing of an input statement like scanf can cause the modification of variable values that can impact future behavior. If input is required, its source must always be represented in the model. The input can then be captured with the available primitives in PROMELA, such as sends and receives.
In one minor instance we deviate from this rather strict standard. When SPIN is used in simulation mode, there is a way to read characters interactively from a user-defined input. To enable this feature, it suffices to declare a channel of the reserved type STDIN in a PROMELA model. There is only one message field available on this predefined channel, and it is of type int. The model in Figure 3.2 shows a simple word count program as an example.
Figure 3.2 Word Count Program Using STDIN Feature
chan STDIN; int c, nl, nw, nc; init { bool inword = false; do :: STDIN?c -> if :: c == -1 -> break /* EOF */ :: c == '\n' -> nc++; nl++ :: else -> nc++ fi; if :: c == ' ' || c == '\t' || c == '\n' -> inword = false :: else -> if :: !inword -> nw++; inword = true :: else /* do nothing */ fi fi od; assert(nc >= nl); printf("%d\t%d\t%d\n", nl, nw, nc) }
We can simulate the execution of this model (but not verify it) by invoking SPIN as follows, feeding the source text for the model itself as input.
$ spin wc.pml < wc.pml 27 85 699 1 process created
PROMELA supports a small number of other special purpose keywords that can be used to fine-tune verification models for optimal performance of the verifiers that can be generated by SPIN. We mention the most important of these here. (This section can safely be skipped on a first reading.)