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


3.1.1.1 Case Expressions

A case expression has the following syntax:

case_simple_expr ::
          "case"
             simple_expr ":" simple_expr ";"
             simple_expr ":" simple_expr ";"
             ...
             simple_expr ":" simple_expr ";"
          "esac"

A case_simple_expr returns the value of the first expression on the right hand side of `:', such that the corresponding condition on the left hand side evaluates to 1. Thus, if simple_expr on the left side is true, then the result is the corresponding simple_expr on the right side. If none of the expressions on the left hand side evaluates to 1, the result of the case_expression is the numeric value 1. It is an error for any expression on the left hand side to return a value other than the truth values 0 or 1.



NuSMV <nusmv@irst.itc.it>