Promela |
Declarator |
arrays |
NAME
arrays
-
syntax for declaring and initializing a one-dimensional
array of variables.
SYNTAX
typename name '[' const ']' [ = any_expr ]
DESCRIPTION
An object of any predefined or user-defined
datatype can be declared either as a scalar or as an array.
The array elements are distinguished from one another
by their array index. As in the C language,
the first element in an array always has index zero.
The number of elements in an array must be specified in the
array declaration with an integer constant
(i.e., it cannot be specified with an expression).
If an initializer is present, the initializing expression
is evaluated once, and all array elements are initialized
to the same resulting value.
In the absence of an explicit initializer, all array elements are initialized to zero.
Data initialization for global variables happens in the initial system state. All process local variables are initialized at process instantiation. The moment of creation and initialization of a local variable is independent of the precise place within the proctype body where the variable declaration is placed.
EXAMPLES
The declaration
byte state[N]with N a constant declares an array of N bytes, all initialized to zero by default. The array elements can be assigned to and referred to in statements such as
state[0] = state[3] + 5 * state[3*2/n]where n is a constant or a variable declared elsewhere. An array index in a variable reference can be any valid (i.e., side-effect free) Promela expression. The valid range of indices for the array state , as declared here, is 0..N-1 .
NOTES
Scalar objects are treated as shorthands for
array objects with just one element.
This means that references to scalar objects
can always be suffixed with
[0] without triggering a complaint from the Spin parser.
Be warned, therefore, that if two arrays are
declared as
byte a[N], b[N];then the assignment
a = b;will have the same effect as
a[0] = b[0];and will not copy all the elements of the arrays.
An array of bit or bool variables is stored by the verifier as an array of unsigned char variable, and therefore saves no memory over a byte array. It can be better, therefore, to use integers in combination with bit-masking operations to simulate operations on a bit-array when memory is tight. The same rules apply here as would apply for the use of bit-arrays in C programs.
Multidimensional arrays can be constructed indirectly with the use of typedef definitions.
The use of an array index value outside the declared range triggers a run-time error in Spin. This default array-index bound checking can be turned off during verifications, if desired, for increased performance. This can be done by compiling the pan.c source with the additional directive -DNOBOUNDCHECK .
SEE ALSO
chan
datatypes
mtype
typedef
|
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 28 November 2004) |