Go to the first, previous, next, last section, table of contents.


3.2.2 Input Variables

A state of the model is an assignment of values to a set of state variables. These variables (and also instances of modules) are declared by the notation:

ivar_declaration :: "IVAR"
             atom ":" type ";"
             atom ":" type ";"
             ...

The type associated with a variable declaration can be either a boolean, a scalar, a user defined module, or an array of any of these (including arrays of arrays) (See section 3.2.1 State Variables).



NuSMV <nusmv@irst.itc.it>