Note that an array in SMV is not really a data type. It is simply a collection of signals with similar names. This means that it is possible to declare an ``array'' whose elements have different types, by simply declaring the elements individually. For example:
state[0] : {ready, willing};
state[1] : {ready, willing, able};
state[2] : {ready, willing, able, exhausted};
See section 10.10, however, for a discussion on the
consequences of such a declaration for array references in expressions.