Download NuSMV 2.2 User Manual

set_expr ::
" " set_elem "," ... "," set_elem " " ;; set definition
| simple_expr "in " simple_expr
;; set inclusion test
| simple_expr "union " simple_expr
;; set union
set_elem :: simple_expr
A set can be defined by enumerating its elements inside curly braces ‘ . . . ’. The
inclusion operator ‘in’ tests a value for membership in a set. The union operator
‘union’ takes the union of two sets. If either argument is a number or a symbolic
value instead of a set, it is coerced to a singleton set.
2.1.2 Next Expressions
While simple expressions can represent sets of states, next expressions relate current
and next state variables to express transitions in the FSM. The structure of next expressions is similar to the structure of simple expressions (See Section 2.1.1 [simple
expressions], page 6). The difference is that next expression allow to refer to next state
variables. The grammar is depicted below.
next_expr ::
atom
| number
| "TRUE"
| "FALSE"
| var_id
| "(" next_expr ")"
| "next" "(" simple_expr ")"
| "!" next_expr
| next_expr "&" next_expr
| next_expr "|" next_expr
| next_expr "xor" next_expr
| next_expr "->" next_expr
| next_expr "<->" next_expr
| next_expr "=" next_expr
| next_expr "!=" next_expr
| next_expr "<" next_expr
| next_expr ">" next_expr
| next_expr "<=" next_expr
| next_expr ">=" next_expr
| next_expr "+" next_expr
| next_expr "-" next_expr
| next_expr "*" next_expr
| next_expr "/" next_expr
| next_expr "mod" next_expr
| set_next_expr
| case_next_expr
;;
;;
;;
;;
;;
a symbolic constant
a numeric constant
The boolean constant 1
The boolean constant 0
a variable identifier
;;
;;
;;
;;
;;
;;
;;
;;
;;
;;
;;
;;
;;
;;
;;
;;
;;
;;
;;
;;
next value of an "expression"
logical not
logical and
logical or
logical exclusive or
logical implication
logical equivalence
equality
inequality
less than
greater than
less than or equal
greater than or equal
integer addition
integer subtraction
integer multiplication
integer division
integer remainder
a set next_expression
a case expression
set next expr and case next expr are the same as set simple expr (see
Section 2.1.1 [set expressions], page 7) and case simple expr (see Section 2.1.1
[case expressions], page 7) respectively, with the replacement of ”simple ” with
”next ”. The only additional production is "next" "(" simple expr ")",
which allows to “shift” all the variables in simple expr to the next state. The next
operator distributes on every operator. For instance, the formula next((A & B) |
8