In the absence of an explicit initializer, all array elements are initialized to zero.
Data initialization happens in the initial system state, for globally declared variables, and in the initial process state, for process local variables. The latter is independent of where in a proctype body the variable declaration is placed.
byte state[N]with N a constant, declares an array of N bytes, all initialized to zero, that can be assigned and referred to in statements such as
state = state + 5 * state[3*2/n]where n is a constant or a variable declared elsewhere. An array index can be an arbitrary, side effect free, Promela expressions. The valid range of indices for array state , declared above, is 0 .. N-1 .
An array of bit or bool variables is stored by the verifier as an array of unsigned char , and therefore saves no memory over byte arrays.
Multi-dimensional arrays can be constructed indirectly with the use of typedef definitions. See typedef(2).
The use of an index value outside the declared range triggers a runtime error in Spin. This default array-index bound checking can be turned off during verifications (if desired for efficiency reasons) if the pan.c source is compiled with the additional directive -DNOBOUNDCHECK .