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

3.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 Kripke structure. The structure of next expressions is similar to the structure of simple expressions (See section 3.1.1 Simple Expressions). The difference is that next expression allow to refer to next state variables. The grammar is depicted below.

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

set_next_expr and case_next_expr are the same as set_simple_expr (see section 3.1.1.2 Set Expressions) and case_simple_expr (see section 3.1.1.1 Case Expressions) 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) | C) is a shorthand for the formula (next(A) & next(B)) | next(C). It is an error if in the scope of the next operator occurs another next operator.