|
  
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 meanings .
* -- 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: Hierarchical Names
Jae-Young Jang
Wed Feb 12 14:01:23 MST 1997
|
