1
Download NuSMV 2.6 User Manual
Transcript
basic_expr : basic_expr ;
| case_body basic_expr : basic_expr ;
basic_expr ? basic_expr : basic_expr
Simple Expression
simple_expr :: basic_expr
Note that simple expressions cannot contain next operators.
Next Expression
next_expr :: basic_expr
Type Specifier
type_specifier ::
simple_type_specifier
| module_type_spicifier
simple_type_specifier ::
boolean
| word [ integer_number ]
| unsigned word [ integer_number ]
| signed word [ integer_number ]
| { enumeration_type_body }
| integer_number .. integer_number
| array integer_number .. integer_number
of simple_type_specifier
enumeration_type_body ::
enumeration_type_value
| enumeration_type_body , enumeration_type_value
enumeration_type_value ::
symbolic_constant
| integer_number
Module Type Specifier
module_type_specifier ::
| identifier [ ( [ parameter_list ] ) ]
| process identifier [ ( [ parameter_list ] ) ]
parameter_list ::
simple_expr
| parameter_list , simple_expr
State, Input and Frozen Variables
var_declaration :: VAR var_list
ivar_declaration :: IVAR simple_var_list
132
