- 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
Data Objects
There are only two levels of scope in PROMELA models: global and process local. Naturally, within each level of scope, all objects must be declared before they can first be referenced. Because there are no intermediate levels of scope, the scope of a global variable cannot be restricted to just a subset of processes, and the scope of a process local variable cannot be restricted to specific blocks of statements. A local variable can be referenced from its point of declaration to the end of the proctype body in which it appears, even when it appears in a nested block (i.e., a piece of code enclosed in curly braces). This is illustrated by the following example:
Table 3.1. Basic Data Types
|
Type |
Typical Range |
|---|---|
|
bit |
0,1 |
|
bool |
false,true |
|
byte |
0..255 |
|
chan |
1..255 |
|
mtype |
1..255 |
|
pid |
0..255 |
|
short |
–215 .. 215 – 1 |
|
int |
–231 .. 231 – 1 |
|
unsigned |
0 .. 2n – 1 |
init {
/* x declared in outer block */
int x;
{ /* y declared in inner block */
int y;
printf("x = %d, y = %d\n", x, y);
x++;
y++;
}
/* y remains in scope */
printf("x = %d, y = %d\n", x, y);
}
When simulated this model produces the output:
$ spin scope.pml x = 0, y = 0 x = 1, y = 1 1 process created
Table 3.1 summarizes the basic data types in PROMELA, and the typical range of values that corresponds to each type on most machines.
The data type unsigned, like its counterpart in the C programming language, can be used to declare a quantity that is stored in a user-defined number of bits n, with 1 ≤ n ≤ 32. With just two exceptions, these data types can store only unsigned values. The two exceptions are short and int, which can hold either positive or negative values. The precise value ranges of the various types is implementation dependent. For short, int, and unsigned, the effective range matches those of the same types in C programs when compiled on the same hardware. For byte, chan, mtype, and pid, the range matches that of the type unsigned char in C programs. The value ranges for bit and bool are always restricted to two values.
Typical declarations of variables of these basic types include:
bit x, y; /* two single bits, initially 0 */ bool turn = true; /* boolean value, initially true */ byte a[12]; /* all elements initialized to 0 */ chan m; /* uninitialized message channel */ mtype n; /* uninitialized mtype variable */ short b[4] = 89; /* all elements initialized to 89 */ int cnt = 67; /* integer scalar, initially 67 */ unsigned v : 5; /* unsigned stored in 5 bits */ unsigned w : 3 = 5; /* value range 0..7, initially 5 */
Only one-dimensional arrays of variables are supported, although there are indirect ways of defining multidimensional arrays through the use of structure definitions, as we will see shortly. All variables, including arrays, are by default initialized to zero, independent of whether they are global or local to a process.
Variables always have a strictly bounded range of possible values. The variable w in the last example, for instance, can only contain values that can be stored in three bits of memory: from zero to seven. A variable of type short, similarly, can only contain values that can be stored in sixteen bits of memory (cf. Table 3.1). In general, if a value is assigned to a variable that lies outside its declared domain, the assigned value is automatically truncated. For instance, the assignment
byte a = 300;
results in the assignment of the value 44 (300%256). When such an assignment is performed during random or guided simulations, SPIN prints an error message to alert the user to the truncation. The warning is not generated during verification runs, to avoid generating large volumes of repetitive output.
As usual, multiple variables of the same type can be grouped behind a single type name, as in:
byte a, b[3] = 1, c = 4;
In this case, the variable named a is, by default, initialized to zero; all elements of array b are initialized to one, and variable c is initialized to the value four.
Variables of type mtype can hold symbolic values that must be introduced with one or more mtype declarations. An mtype declaration is typically placed at the start of the specification, and merely enumerates the names, for instance, as follows:
mtype = { appel, pear, orange, banana };
mtype = { fruit, vegetables, cardboard };
init {
mtype n = pear; /* initialize n to pear */
printf("the value of n is ");
printm(n);
printf("\n")
}
Of course, none of the names specified in an mtype declaration can match reserved words from PROMELA, such as init, or short.
As shown here, there is a special predefined print routine printm that can be used to print the symbolic name of an mtype variable. There can be multiple mtype declarations in a model, but distinct declarations do not declare distinct types. The last model, for instance, is indistinguishable to SPIN from a model with a single mtype declaration, containing the concatenation (in reverse order) of the two lists, as in:
mtype = { fruit, vegetables, cardboard,
appel, pear, orange, banana };
Because of the restricted value range of the underlying type, no more than 255 symbolic names can be declared in all mtype declarations combined. The SPIN parser flags an error if this limit is exceeded.