matrixpromelaspin

How to create two dimensional array in Promela?


To create matrix in C we need to write:

int[][] a = {{1,2,3},{1,2,3},{1,2,3}}

How can I create a matrix in Promela?


Solution

  • From the docs:

    Multidimensional arrays can be constructed indirectly with the use of typedef definitions.

    Also from the docs:

    EXAMPLES

    The first example shows how to declare a two-dimensional array of elements of type byte with a typedef.

    typedef array { /* typedefs must be global */
        byte aa[4]
    };
    init {
        array a[8];   /* 8x4 = 32 bytes total */
        a[3].aa[1] = 5
    }
    

    A better approach is to use one-dimensional arrays.