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


3.1.1.2 Set Expressions

A set expression has the following syntax:

set_elem :: atom     ;; a symbolic constant
         |  number   ;; a numeric constant

set_expr ::
         "{" set_elem "," ... "," set_elem "}"  ;; set definition
         |  simple_expr "in" simple_expr        ;; set inclusion predicate
         |  simple_expr "union" simple_expr     ;; set union

A set can be defined by enumerating its elements inside curly braces `{...}'. The elements of the set can be numbers or symbolic constants. 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.



NuSMV <nusmv@irst.itc.it>