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

3.3.1 CTL Specifications

A CTL specification is given as a formula in the temporal logic CTL, introduced by the keyword `SPEC'. The syntax of this declaration is:

spec_declaration :: "SPEC" spec_expr

spec_expr   :: ctl_expr

The syntax of CTL formulas recognized by the NuSMV parser is as follows:

ctl_expr ::
        simple_expr                 ;; a simple boolean expression
        | "(" ctl_expr ")"
        | "!" ctl_expr              ;; logical not
        | ctl_expr "&" ctl_expr     ;; logical and
        | ctl_expr "|" ctl_expr     ;; logical or
        | ctl_expr "->" ctl_expr    ;; logical implies
        | ctl_expr "<->" ctl_expr   ;; logical equivalence
        | "EG" ctl_expr             ;; exists globally
        | "EX" ctl_expr             ;; exists next state
        | "EF" ctl_expr             ;; exists finally
        | "AG" ctl_expr             ;; forall globally
        | "AX" ctl_expr             ;; forall next state
        | "AF" ctl_expr             ;; forall finally
        | "E" "[" ctl_expr "U" ctl_expr "]" ;; exists until
        | "A" "[" ctl_expr "U" ctl_expr "]" ;; forall until

It is an error for an expressions in a CTL formula to contain a `next()' operator or to have non-boolean components, i.e. subformulas which evaluate to a value other than 0 or 1. Also, simple_expr in CTL formulas can not contain case statements.

It is also possible to specify invariants, i.e. propositional formulas which must hold invariantly in the model. The corresponding command is `INVARSPEC', with syntax:

checkinvar_declaration :: "INVARSPEC" simple_expr ";"

This statement corresponds to

SPEC  AG simple_expr ";"

but can be checked by a specialized algorithm during reachability analysis.