nusmv

Data Type declaration


I want to declare an array called Machine consists of 4 elements. Each element is also an array of 2 elements, where, values of the first element are obtained from the enumeration: pressionLevel={below, normal, over} And the second one has values from the enumeration: action={start, pause, stop, restart}

My second question is how to access to elements of this array?

VAR

 pressionLevel={below, normal, over};

 action={start, pause, stop, restart};

 machine= array 1..4  -- how to continue this declaration?? --

enter image description here


Solution

  • AFAIK, arrays of arrays are not directly supported.

    You can either create a different name for each instance of an element module (see machine01), or scrap the element module and push its content within the machine module (see machine02).

    e.g.:

    MODULE element()
    VAR
        pressionLevel : { BELOW, NORMAL, OVER };
        action        : { START, PAUSE, STOP, RESTART };
    
    MODULE machine01()
    VAR
        el1 : element();
        el2 : element();
        el3 : element();
        el4 : element();
    
    MODULE machine02()
    VAR
        pressionLevel : array 1..4 of { BELOW, NORMAL, OVER };
        action        : array 1..4 of { START, PAUSE, STOP, RESTART };
    
    MODULE main()
    VAR
        m1 : machine01();
        m2 : machine02();
    

    The elements of an array can be accessed using constant indexes, e.g.:

    next(precisionLevel[0]) := BELOW
    

    When using the constraint-style modeling, it is easy to model something which has unintended consequences, or to write some constraint that is manageable for very small arrays but, for some reasons, it quickly blows up for larger ones. So I would advice using the assignment-style modeling only, or to expand a constraint like

    precisionLevel[i] = BELOW => ... some consequence ...
    

    as follows

     ((i = 0 & precisionLevel[0] = BELOW) => ... some consequence ...)
     &
     ((i = 1 & precisionLevel[1] = BELOW) => ... some consequence ...)
     &
     ...
    

    where i is a variable acting as an index for the array precisionLevel, and the constraint is expanded over the entire domain of i.