- 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 Structures
PROMELA has a simple mechanism for introducing new types of record structures of variables. The following example declares two such structures, and uses them to pass a set of data from one process to another in a single, indivisible operation:
typedef Field {
short f = 3;
byte g
};
typedef Record {
byte a[3];
int fld1;
Field fld2;
chan p[3];
bit b
};
proctype me(Field z) {
z.g = 12
}
init {
Record goo;
Field foo;
run me(foo)
}
We have defined two new data types named Field and Record, respectively. The local variable goo in the init process is declared to be of type Record. As before, all fields in the new data types that are not explicitly initialized (e.g., all fields except f in variables of type Field) are by default initialized to zero. References to the elements of a structure are written in a dot notation, as in for instance:
goo.a[2] = goo.fld2.f + 12
A variable of a user-defined type can be passed as a single argument to a new process in run statements, as shown in the example, provided that it contains no arrays. So in this case it is valid to pass the variable named foo as a parameter to the run operator, but using goo would trigger an error message from SPIN about the hidden arrays. In the next section we shall see that these structure type names can also be used as a field declarator in channel declarations.
The mechanism for introducing user-defined types allows for an indirect way of declaring multidimensional arrays, even though PROMELA supports only one-dimensional arrays as first class objects. A two-dimensional array can be created, for instance, as follows:
typedef Array {
byte el[4]
};
Array a[4];
This creates a data structure of sixteen elements, that can now be referenced as a[i].el[j].
As in C, the indices of an array of N elements range from zero to N-1.