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


3.2.1.1 Type Specifiers

A type specifier has the syntax:

type :: boolean
     |  "{" val "," val "," ... val "}"
     |  number ".." number
     |  "array" number ".." number "of" type
     |  atom [ "(" simple_expr "," simple_expr "," ...  ")" ]
     |  "process" atom [ "(" simple_expr "," ... "," simple_expr ")" ]

val  :: atom
     |  number

A variable of type boolean can take on the numerical values 0 and 1 (representing false and true, respectively). In the case of a list of values enclosed in quotes (where atoms are taken to be symbolic constants), the variable is a scalar which take any of these values. In the case of an array declaration, the first simple_expr is the lower bound on the subscript and the second simple_expr is the upper bound. Both of these expressions must evaluate to integer constants. Finally, an atom optionally followed by a list of expressions in parentheses indicates an instance of module atom (See section 3.2.9 MODULE declarations). The keyword causes the module to be instantiated as an asynchronous process (See section 3.2.12 Processes).



NuSMV <nusmv@irst.itc.it>