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


3.1.1 Simple Expressions

Simple expressions are expressions built only from current state variables. Simple expressions can be used to specify sets of states, e.g. the initial set of states. The syntax of simple expressions is as follows:

simple_expr ::
          atom                            ;; a symbolic constant
        | number                          ;; a numeric constant
        | "TRUE"                          ;; The boolean constant "TRUE"
        | "FALSE"                         ;; The boolean constant "FALSE"
        | var_id                          ;; a variable identifier
        | "(" simple_expr ")"
        | "!" simple_expr                 ;; logical not
        | simple_expr "&" simple_expr     ;; logical and
        | simple_expr "|" simple_expr     ;; logical or
        | simple_expr "->" simple_expr    ;; logical implication
        | simple_expr "<->" simple_expr   ;; logical equivalence
        | simple_expr "=" simple_expr     ;; equality
        | simple_expr "<" simple_expr     ;; less than
        | simple_expr ">" simple_expr     ;; greater than
        | simple_expr "<=" simple_expr    ;; less than or equal
        | simple_expr ">=" simple_expr    ;; greater than or equal
        | simple_expr "+" simple_expr     ;; integer addition
        | simple_expr "-" simple_expr     ;; integer subtraction
        | simple_expr "*" simple_expr     ;; integer multiplication
        | simple_expr "/" simple_expr     ;; integer division
        | simple_expr "mod" simple_expr   ;; integer remainder
        | set_simple_expr                 ;; a set simple_expression
        | case_simple_expr                ;; a case expression

A var_id, (see section 3.2.10 Identifiers) or identifier, is a symbol or expression which identifies an object, such as a variable or a defined symbol. Since a var_id can be an atom, there is a possible ambiguity if a variable or defined symbol has the same name as a symbolic constant. Such an ambiguity is flagged by the interpreter as an error.

The order of parsing precedence for operators from high to low is:

*,/
+,-
mod
=,<,>,<=,>=
!
&
|
->,<->

Operators of equal precedence associate to the left. Parentheses may be used to group expressions.



NuSMV <nusmv@irst.itc.it>