Promela Reference -- arrays(2)




arrays - syntax for declaring and initializing a one-dimensional array of variables.

typename name '[' const ']' [ = any_expr ]

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.

The declaration

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 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 .

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

then the assignment will have the same effect as 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 .


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 28 November 2004)