next up previous
Next: Hierarchical Names

CTL Syntax

Yuji Kukimoto

The VIS Group. University of California, Berkeley.

Jae-Young Jang

The VIS Group. University of Colorado, Boulder.

Wed Feb 12 14:01:32 MST 1997

CTL (Computation Tree Logic) is a language used to describe properties of systems. This document describes the CTL syntax used in VIS. For the semantics of CTL, the reader should refer to the following paper.

E. M. Clarke, E. A. Emerson and A. P. Sistla, Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems, vol 8-2, pages 244-263, April, 1986

This syntax should be followed when VIS users create CTL files and fairness constraint files for the commands model_check and read_fairness, respectively.

The syntax for CTL is:

TRUE, FALSE, and var-name=value are CTL formulas, where var-name is the full hierarchical name of a variable, and value is a legal value in the domain of the variable. var-name1 == var-name2 is the atomic formula that is true if var-name1 has the same value as var-name2. Currently it can be used only in the Boolean domain. (It cannot be used for variables of enumerated types.) var-name1[i:j] == var-name2[k:l] can be used if the lengths of vectors are the same. Vector variables, the syntax of hierarchical names, and macro define are described at the end of this document. The following character set may be used for var-names and values:

       A-Z a-z 0-9 ^ ? | / [ ] + * $ < > ~ @ _ # % : " ' .

If f and g are CTL formulas, then so are the following:

    (f), f * g, f + g, f ^ g, !f, f -> g, f <-> g,
    AG f, AF f, AX f, EG f, EF f, EX f, A(f U g) and E(f U g).

AX:n(f) is allowed as a shorthand for AX(AX(...AX(f)...)), where n is the number of invocations of AX. EX:n(f) is defined similarly. Binary operators must be surrounded by spaces, i.e. f + g is a CTL formula while f+g is not. The same is true for U in until formulas. Once parentheses are inserted, the spaces can be omitted, i.e. (f)+(g) is a valid formula. Unary temporal operators and their arguments must be separated by spaces unless parentheses are used.

The symbols have the following meaningsgif.

    * -- AND, + -- OR, ^ -- XOR, ! -- NOT, -> -- IMPLY, <-> -- EQUIV

Operator Precedence:

High

    !

    AG, AF, AX, EG, EF, EX

    *

    +

    ^

    <->

    ->

    U
Low

An entire formula should be followed by a semicolon. All text from # to the end of a line is treated as a comment. The model checker ( mc) package is used to decide whether or not a given FSM satisfies a given CTL formula. See the help file for the model_check command for more details.





next up previous
Next: Hierarchical Names



Jae-Young Jang
Wed Feb 12 14:01:23 MST 1997
You are not logged in 
Contact 
©2002-2017 U.C. Regents