Table of Contents
xtl - evaluation of value-based temporal logic formulas
xtl
[
-cc options ] [
-create] [
-english] [
-expand] [
-french] [
-remove] [
-silent] [
-tmp directory ] [
-update] [
-verbose] [
-version] [
-warning]
file1[
.xtl]
file2[
.bcg]
xtl takes as input
file1[
.xtl], which is a program written in
XTL (eXecutable Temporal Language), and evaluates it on
file2[
.bcg], which
contains an LTS (Labelled Transition System) encoded in the BCG (Binary
Coded Graph) format.
The XTL tool offers the following features:
- XTL supports
several temporal logics widely used. Currently, the following temporal logics
are supported: HML, CTL, ACTL, LTAC, as well as the modal mu-calculus. All
of them can be directly used by end-users to verify properties on BCG
graphs.
- Compared to other model-checkers, XTL is more expressive, because
it allows to handle the data values contained in states and transition
labels. These values can be used in temporal formulas, assigned to variables,
etc.
- Moreover, XTL is extensible. A user can define his/her own temporal
logic, as a library of operators written in XTL. This is the way in which
the currently available formalisms (HML, CTL, ACTL, LTAC and modal mu-calculus)
are implemented.
- Finally, XTL can also be used for other purpose than evaluation
of temporal formulas. Because it is a functional programming language, it
allows to perform any computation on BCG graphs: for instance, it can compute
the branching factor of a graph, print its list of labels, etc.
An overview
of the XTL language is presented below. The abstract syntax of each language
construct is defined by a BNF grammar and the semantics is described informally.
Terminal symbols are enclosed in double quotes. Optional elements are enclosed
in square brackets. Suspension points are used to denote zero or more repetitions
of an element. The meaning of grammar symbols is given in the table below.
The axiom of the grammar is the non-terminal symbol PG.
+--------+-------------------------------+
| Symbol | Description |
+========+===============================+
| K | constant |
| x | variable |
| T | simple type |
| G | gate |
| F | function |
| M | macro |
| P | macro parameter |
| E | expression |
| O | offer |
| D | variable declaration |
| RT | result type |
| OP | operator |
| FD | function definition |
| MD | macro definition |
| LI | library inclusion |
| ETD | external type declaration |
| EFD | external function declaration |
| EID | external include directive |
| ELD | external compile directive |
| PG | program |
+--------+-------------------------------+
An XTL program is evaluated over an LTS model generated from
a source program to be verified. This LTS, encoded in a BCG file, contains
the following elements:
- a set of states of the source program. A state is
represented as a tuple containing the values of all the variables of the
program (the so-called "state vector").
- a set of actions performed by the
program. An action (also called label) is represented as a list of typed
values. In BCG files generated from LOTOS programs, the labels have the
form G v1 ... vm (with m >= 0), where G is a gate name.
- a transition relation
between the states of the program. A transition, represented as a triple
(s1, a, s2), means that the program can move from state s1 to state s2
by performing action a.
- the initial state of the program.
Besides the above
elements, a BCG file contains also informations about the types and functions
of the source program (see "Binary Coded Graphs - Definition of the BCG
Format" for a complete description of the BCG file format, and see also
the bcg
manual page)
The lexical units of XTL are:
keywords,
identifiers and
separators. The keywords, listed below, must be
written in lower-case letters.
any | end_def | exists | of |
apply | end_exists | for | on |
assert | end_for | forall | then |
def | end_forall | from | to |
else | end_if | if | use |
else_if | end_let | in | where |
end_assert | end_use | let |
The
identifiers are grouped into two classes:
- external identifiers denote the
objects defined in the source program to be verified (these objects are
contained in the BCG file). These identifiers may be written like the internal
ones, as long as there is no clash between them and the normal identifiers
or the XTL keywords. In the latter case, external identifiers must be surrounded
by backquote characters (e.g.,
`let`) to avoid clashes. - internal identifiers
denote the objects defined in the XTL program (or predefined in the XTL
language). These identifiers may be either normal, i.e., built from letters,
digits and underscores (beginning with a letter or an underscore), or special,
i.e., built from the characters #, /, %, &, *, +, -, ., =, @, \, ^, ~, |, <, >, [,
]. In normal identifiers, no difference is made between lower- and uppercase
letters. The special identifiers are useful for mathematical and/or logical
notations (e.g., '+', '/\', etc.).
The separators are sequences containing space,
tab, and newline characters, as well as comments, enclosed between (* and
*).
XTL is a strongly-typed language: every
object used in an XTL program must have a unique type, which is statically
determined. XTL does not provide a mechanism for type definition, although
anonymous tuple types (see below) can be implicitly created. The types allowed
in XTL fall into the following classes:
- external types are imported from
the source program to be verified. These types are contained in the type
area of the BCG file and can be referenced in XTL programs using external
identifiers. Other externally defined types can be included in the XTL programs
by means of special directives (see DIRECTIVES below).
- internal types are
either predefined in the language, or defined by the user. Among the predefined
types, we can distinguish:
- o
-
boolean, integer, real, character, string.
These are the usual types defined in programming languages. They are equipped
with the usual operations, given in the table below.
+----------------------------------------+--------------------------+
| Operator | Meaning |
+========================================+==========================+
| true, false : -> boolean | boolean constants |
| not : boolean -> boolean | negation |
| or, and, implies, | connectors and |
| =, <> : boolean, boolean -> boolean | relational operators |
| replace : boolean, boolean -> boolean | replacement operator |
+----------------------------------------+--------------------------+
| -, + : integer, integer -> integer | binary minus, plus |
| - : integer -> integer | unary minus |
| *, div : integer, integer -> integer | multiplication, division |
| mod : integer, integer -> integer | modulo |
| ** : integer, integer -> integer | power |
| integer : real -> integer | real to integer |
| integer : character -> integer | character to integer |
| <, <=, >, >=, =, <> : | relational operators |
| integer, integer -> boolean | |
| replace : integer, integer -> integer | replacement operator |
+----------------------------------------+--------------------------+
| -, + : real, real -> real | binary minus, plus |
| - : real -> real | unary minus |
| *, / : real, real -> real | multiplication, division |
| ** : real, real -> real | power |
| real : integer -> real | integer to real |
| <, <=, >, >=, =, <> : | relational operators |
| real, real -> boolean | |
| replace : real, real -> real | replacement operator |
+----------------------------------------+--------------------------+
| -, + : character, integer -> character | subtract, add integer |
| character : integer -> character | integer to character |
| <, <=, >, >=, =, <> : | relational operators |
| character, character -> boolean | |
| replace : | |
| character, character -> character | replacement operator |
+----------------------------------------+--------------------------+
| null : -> string | empty string |
| length : string -> integer | string length |
| extract : string, integer -> character | character extraction |
| =, <> : string, string -> boolean | relational operators |
| replace : string, string -> string | replacement operator |
+----------------------------------------+--------------------------+
-
- All the binary operators op above (except "
extract" and "replace") are
infixed, i.e., their calls may be written "E1 op E2" (see FUNCTIONS below).
Unary minus must be written in functional notation (i.e., -(1) instead of
-1). The numerical, character, and string constants have a C-like syntax (e.g.,
12, 3.1416, 'a', '\n', "hello\n"). The boolean constants true and false are defined
as 0-ary functions.
The overloaded "replace" operator takes two arguments
of the same type and returns the second one. It is useful for use within
the "for" expressions (see EXPRESSIONS below).
- o
-
state, label, edge, stateset,
labelset, edgeset. These types, also called meta-types (because they refer
to the LTS model rather than to the objects defined in the source program
to be verified), denote the states, labels, edges, sets of states, sets
of labels, and sets of edges of the LTS, respectively. The table below
gives the predefined operators over these types ("set" denoting either
stateset, labelset, or edgeset). These operators allow to explore (forward
and/or backward) the transition relation of the LTS, to combine sets of
states, labels and edges, and also to obtain information about the LTS.
+-----------------------------------+-------------------------+
| Operator | Meaning |
+===================================+=========================+
| init : -> state | initial state |
| succ : state -> stateset | successor states |
| pred : state -> stateset | predecessor states |
| out : state -> edgeset | successor transitions |
| in : state -> edgeset | predecessor transitions |
| =, <> : state, state -> boolean | comparison operators |
| replace : state, state -> state | replacement operator |
+-----------------------------------+-------------------------+
| visible : label -> boolean | visibility test |
| =, <> : label, label -> boolean | comparison operators |
| replace : label, label -> label | replacement operator |
+-----------------------------------+-------------------------+
| source : edge -> state | transition source state |
| target : edge -> state | transition target state |
| label : edge -> label | transition label |
| succ : edge -> edgeset | successor transitions |
| pred : edge -> edgeset | predecessor transitions |
| =, <> : edge, edge -> boolean | comparison operators |
| replace : edge, edge -> edge | replacement operator |
+-----------------------------------+-------------------------+
| empty, false : -> set | empty set |
| full, true : -> set | full set |
| comp, not : set -> set | complementation |
| union, or : set, set -> set | union |
| inter, and : set, set -> set | intersection |
| implies : set, set -> set | implication |
| iff : set, set -> set | equivalence |
| diff : set, set -> set | difference |
| includes : set, set -> boolean | inclusion test |
| insert, remove : set, elem -> set | insertion, removal |
| among : elem, set -> boolean | membership |
| card : set -> number | cardinal |
| =, <> : set, set -> boolean | comparison operators |
| replace : set, set -> set | replacement operator |
+-----------------------------------+-------------------------+
-
- For convenience, some of the operators above are overloaded (see FUNCTIONS
below). Also, some of the set operators have synonyms (e.g.,
union has the
synonym or) allowing a more intuitive writing of boolean properties.
The
overloaded "replace" operator takes two arguments of the same type and
returns the second one. It is useful for use within the "for" expressions
(see EXPRESSIONS below).
- o
-
number. The BCG file format associates a unique
number to every state, label, and edge of the LTS. The XTL language provides
the number type for the manipulation of state, label, and edge numbers.
The table below gives the predefined operators of type number.
+------------------------------------+--------------------------+
| Operator | Meaning |
+====================================+==========================+
| number_of_states : -> number | number of states |
| number_of_labels : -> number | number of labels |
| number_of_edges : -> number | number of edges |
| number : state -> number | state number |
| number : label -> number | label number |
| number : edge -> number | edge number |
+------------------------------------+--------------------------+
| -, + : number, number -> number | binary minus, plus |
| *, div : number, number -> number | multiplication, division |
| mod : number, number -> number | modulo |
| ** : number, number -> number | power |
| number : character -> number | conversion from/to |
| character : number -> character | character |
| number : integer -> number | conversion from/to |
| integer : number -> integer | integer |
| number : real -> number | conversion from/to |
| real : number -> real | real |
| <, <=, >, >=, =, <> : | relational operators |
| number, number -> boolean | |
| replace : number, number -> number | replacement operator |
+------------------------------------+--------------------------+
-
- All arithmetic operators (except unary minus) and relational operators
of type
integer are also available for type number. Moreover, the values
belonging to these two types can be freely mixed within arithmetic and
relational expressions. The main difference between these two types concerns
the manipulation of large numbers: the maximum value of type integer is
2^31-1 = 2,147,483,647 on 32-bit machines and 2^63-1 = 9,223,372,036,854,775,807
on 64-bit machines, whereas the maximum value of type number is 2^32-1 = 4,294,967,295
on 32-bit machines and 2^64-1 = 18,446,744,073,709,551,615 on 64-bit machines.
Therefore, for large LTSs, any information concerning the LTS structure
(e.g., cardinality of state/edge/label subsets, depth/breadth of the LTS,
number of breadth-first levels, etc.) should be manipulated using values
of type number instead of type integer in order to avoid overflows.
Conversion
operators between the number type and the types character, integer, and
real are also provided. Constants of type number are written in decimal
notation preceded by a '#' character (e.g., #4294967295). An alternative way
of representing constants of type number that fit in the range of type
integer is by means of the conversion operator from integer to number (e.g.,
the values number(2147483647) and #2147483647 are the same).
- o
-
action.
The XTL language allows to print data values on the UNIX standard output
stream (stdout). The action type is associated to the XTL expressions that
print values on the output stream (that is, modify it by side-effect). The
table below gives the predefined operators of type action (T may be any
type).
+--------------------------------+------------------------+
| Operator | Meaning |
+================================+========================+
| nop : -> action | inaction |
| fby : action, action -> action | sequential composition |
| print : T -> action | value printing |
+--------------------------------+------------------------+
- o
- anonymous tuples. These types denote structures containing fields of
different types. The fields can be of any type (including anonymous tuples,
which enables nesting of tuples). These types are noted "(" T0"," ..."," Tn
")" and are essentially used in situations when several values must be
computed and returned simultaneously. The equivalence of tuple types is
defined structurally. The tuple values are noted "(" E0"," ..."," En ")" (see
EXPRESSIONS below).
The functions that can be used in an XTL program fall
into the following classes:
- external functions are defined in the source
program to be verified. They are contained in the function area of the BCG
file and can be referenced in XTL programs using external identifiers.
- internal
functions are either predefined in XTL (a list of the predefined functions
has been given in the above paragraphs), or user-defined (see FUNCTIONS
below for the syntax of function definitions).
The expressions
allowed in XTL use the following auxiliary constructs.
- Offers
- An offer
is a construct allowing to match a value contained in a transition label.
The offers have the following syntax:
O ::= "?" x ":" T
| "!" E
| "_"
An offer "?" x ":" T matches a value v iff v has the type T; in case
of matching, the variable x is also assigned the value v. An offer "!" E
matches a value v iff the expression E evaluates to v. An offer "_" (wildcard)
matches a value v of any type.
- Result types
- The result types denote either
simple types, or anonymous tuple types. They have the following syntax:
RT ::= T
| "(" RT0"," ..."," RTn ")"
These types may occur in variable declarations (see the next paragraph)
as well as in function declarations (see FUNCTIONS below).
- Variable declarations
- The variable declarations have the following syntax:
D ::= x ":" RT
| "any" RT
| "(" D0"," ..."," Dn ")"
A declaration x ":" RT defines the variable x of type RT. A declaration
"any" RT, which is meaningful only inside a declaration of anonymous tuple
type, defines a placeholder of type RT standing for a field of the tuple.
Declarations of the form "any" RT can occur only in the "let" expressions
(see below). A declaration "(" D0"," ..."," Dn ")" defines a tuple whose fields
are denoted by the variables and placeholders occurring inside D0, ..., Dn.
- Operators
- The operators occur in the "
for" expressions (see below); they
denote calls of binary functions on two arguments. They have the following
syntax:
OP ::= F
| "(" OP0"," ..."," OPn ")"
An F operator denotes a call of the binary function F. An "(" OP0"," ...","
OPn ")" operator denotes a call of a binary function on two arguments of
tuple type; the result is a tuple whose fields are the results of the calls
of OP0, ..., OPn on the corresponding fields of the arguments. There is a static
semantics constraint on the operators OP: their left arguments must have
the same types as their results.
The syntax of expressions is given by
the following grammar:
E ::= K
| F "(" E0"," ..."," En ")"
| E0 "of" RT
| E0 "->" "[" O0 ... On [ "..." ] [ "where" E1 ] "]"
| "{" E0"," ..."," En "}"
| "(" E0"," ..."," En ")"
| "let" D0 "=" E0"," ..."," Dn "=" En "in"
En+1
"end_let"
| "if" E0 "then" E'0
"else_if" E1 "then" E'1
...
"else_if" En "then" E'n
"else" E'n+1
"end_if"
| "assert" E0"," ..."," En "in"
En+1
"end_assert"
| "use" x0"," ..."," xn "in"
E
"end_use"
| "for" [ x0 ":" T0 [ "among" E0 ]"," ...","
xn ":" Tn [ "among" En ] ]
[ "in" D ]
[ "while" E'1 ]
[ "where" E'2 ]
"apply" OP
"from" E'3
"to" E'4
"end_for"
| "forall" x0 ":" T0 [ "among" E0 ]"," ...","
xn ":" Tn [ "among" En ]
"in"
En+1
"end_forall"
| "exists" x0 ":" T0 [ "among" E0 ]"," ...","
xn ":" Tn [ "among" En ]
"in"
En+1
"end_exists"
| "<|" OP "on" x0 ":" T0 [ "among" E0 ]"," ...","
xn ":" Tn [ "among" En ]
[ "where" E' ]
"|>" En+1
| "{" x ":" T [ "among" E0 ] "where" E1 "}"
The semantics of expressions is described informally below.
K
-
- is a literal constant of a predefined type (see TYPES, FUNCTIONS AND CONSTANTS
above).
F "(" E0"," ..."," En ")"
-
- denotes a call of the function F on the arguments E0, ..., En. The arguments
must be compatible (in number and types) with the formal parameters given
in the definition of F (see FUNCTIONS below).
E0 "of" RT
-
- specifies that expression E0 has type RT. This mechanism allows to solve
ambiguities that may be caused by function overloading (see FUNCTIONS below).
E0 "->" "[" O0 ... On [ "..." ] [ "where" E1 ] "]"
-
- is an expression of type
boolean, called matching expression. E0 must
be of type label or edge. The construct between "[" and "]" is called an
action pattern: it allows to match the content of the label denoted by
E0 (if E0 is of type label) or by label (E0) (if E0 is of type edge), possibly
extracting the values of its different fields. For convenience, in the
verification of LOTOS programs, the first offer O0 (intended to match a
gate) can be simply written G (i.e., without the "!" sign). The optional construct
"..." matches a sequence of zero or more values of any type. The variables
contained in O0, ..., On (if any) are visible in the optional expression E1,
which must be of type boolean. A matching expression matches a label G v1
... vm iff: m = n if "..." is absent, or m >= n otherwise; O0 matches G; O1, ...,
On match v1, ..., vn; E1, if present, evaluates to true in the context of
the variables assigned in the offers. A matching expression evaluates to
true in case of successful matching of a label (in this case, all the variables
contained in the offers have been initialized) and to false otherwise.
"{" E0"," ..."," En "}"
-
- denotes a value of type set defined explicitly (i.e., by enumerating all
its elements). The expressions E0, ..., En must all be of type
stateset, labelset,
or edgeset.
"(" E0"," ..."," En ")"
-
- denotes a value of type tuple, containing n fields whose values are
given by E0, ..., En.
"let" D0 "=" E0"," ..."," Dn "=" En "in"
En+1
"end_let"
-
- allows to declare and initialize variables. The types of the initialization
expressions E0, ..., En must be compatible with the types corresponding to
the declarations D0, ..., Dn. All the variables occurring in the declarations
Di are initialized with the values of Ei, and are visible in the expression
En+1. The "
let" expression also allows to extract the fields of tuple values
and to assign them to variables.
"if" E0 "then" E'0
"else_if" E1 "then" E'1
...
"else_if" En "then" E'n
"else" E'n+1
"end_if"
-
- allows the conditional evaluation of expressions. The expressions E0,
..., En must be of type
boolean, whereas E'0, ..., E'n+1 must be of the same type
(which is also the type of the "if" expression). The evaluation of an "if"
expression proceeds as follows: the conditions Ei are evaluated (for 1
<= i <= n) and the value of the "if" expression is equal to the value of
the first E'i for which Ei is true. If none of the conditions evaluates to
true, the resulting value is given by E'n+1. If a condition Ei is a matching
operator, the variables assigned by the offers inside Ei are visible only
in the corresponding expression E'i.
"assert" E0"," ..."," En "in"
En+1
"end_assert"
-
- allows to stop the execution of an XTL program if a given condition
does not hold. The expressions E0, ..., En must be of type
boolean. If all the
assertions evaluate to true, the value of the "assert" expression is equal
to the value of En+1; otherwise, the execution of the XTL program is interrupted
and an error message is displayed on the UNIX standard error stream (stderr).
"use" x0"," ..."," xn "in"
E
"end_use"
-
- uses the values of variables x0, ..., xn without changing their value and
then evaluates the expression E. The "use" expression allows to write XTL
programs in which every variable defined is used, which avoids the warnings
of the form "variable set but not used" issued during compilation of the
C code generated by XTL. Although the usage of the "use" expression is harmless
and does not impact in any way the evaluation of XTL expressions, it should
be employed only in the (rare) situations where it is really needed.
"for" [ x0 ":" T0 [ "among" E0 ]"," ...","
xn ":" Tn [ "among" En ] ]
[ "in" D ]
[ "while" E'1 ]
[ "where" E'2 ]
"apply" OP
"from" E'3
"to" E'4
"end_for"
-
- allows the iterative evaluation of expressions. The iteration variables
x0, ..., xn range over the iteration domains T0 [ "among" E0 ], ..., Tn [ "among"
En ], respectively. The expressions Ei must be of type "
set of Ti": thus,
iterations over sets of states, labels, or edges are allowed. There is an
exception concerning integer numbers and characters: for these types, domains
of the form "{" E1 "..." E2 "}", meaning all the integers (resp. characters)
between E1 and E2, are also allowed. The variables declared in the "in"
D declaration (if present) are called accumulators. Both iteration variables
and accumulators are visible in the expressions E'1, E'2 (if present), and
E'4, but not in E'3. The expressions E'1 and E'2 must be of type boolean.
Assuming
that all the optional constructs are present, the evaluation of a "for"
expression proceeds as follows. The accumulators are initialized to the
value of E'3. Let us note v the current values of the accumulators (v may
be of type tuple). Then, for each value of the iteration variables in their
corresponding domains, the expression v OP E'4 is evaluated and its result
is stored in the accumulators. The value of the "for" expression is equal
to the value of the accumulators obtained after the last iteration. The
"where" clause allows to perform only those iterations for which the expression
E'2 evaluates to true. The "while" clause allows to stop the iterations when
the expression E'1 becomes false.
Particular cases of "for" expressions may
be obtained by eliminating some (or all) of the optional constructs. If
the iteration variables are absent, the "for" becomes an infinite loop:
in this case, the "while" clause must be present in order to stop the evaluation.
If the "in" declaration is absent, the accumulator is implicit: it is used
internally to store the results of intermediate iterations, but it cannot
be used in E'1, E'2, nor E'4.
The "for" expressions are useful for describing
iterative computations. For instance, the expression below displays on the
standard output the sequence of Fibonacci numbers smaller than 1000:
for
in (xn_plus_1, xn: integer, a:action)
while xn < 1000
apply (replace, replace, fby)
from (1, 1, nop)
to (xn_plus_1 + xn, xn_plus_1,
print (xn) fby print ("\n"))
end_for
"forall" x0 ":" T0 [ "among" E0 ]"," ...","
xn ":" Tn [ "among" En ]
"in"
En+1
"end_forall"
-
- is the universal quantifier. It is equivalent to the following "
for"
expression:
"for" x0 ":" T0 [ "among" E0 ]"," ...","
xn ":" Tn [ "among" En ]
"apply" and
"from" true
"to" En+1
"end_for"
The type of En+1 may be either boolean, stateset, labelset, or edgeset.
In the three latter cases, the true and and operators correspond to full
set and set intersection, respectively (see TYPES, FUNCTIONS AND CONSTANTS
above).
"exists" x0 ":" T0 [ "among" E0 ]"," ...","
xn ":" Tn [ "among" En ]
"in"
En+1
"end_exists"
-
- is the existential quantifier. It is equivalent to the following "
for"
expression:
"for" x0 ":" T0 [ "among" E0 ]"," ...","
xn ":" Tn [ "among" En ]
"apply" or
"from" false
"to" En+1
"end_for"
The type of En+1 may be either boolean, stateset, labelset, or edgeset.
In the three latter cases, the false and or operators correspond to empty
set and set union, respectively (see TYPES, FUNCTIONS AND CONSTANTS above).
"<|" OP "on" x0 ":" T0 [ "among" E0 ]"," ...","
xn ":" Tn [ "among" En ]
[ "where" E' ]
"|>" En+1
-
- is an abbreviated form of the "
for" expression, called iterator. It is
equivalent to the following "for" expression:
"for" x0 ":" T0 [ "among" E0 ]"," ...","
xn ":" Tn [ "among" En ]
[ "where" E' ]
"apply" OP
"from" init_OP
"to" En+1
"end_for"
-
- Here init_OP is a "start" value associated by default to the operator
OP. Only the binary predefined operators that have initial values assigned
by default can be used in the iterators. These operators, together with
their initial values, are given in the table below (where "set" denotes
either
stateset, labelset, or edgeset).
+-----------------------------------+---------------+
| Operator OP | init_OP |
+===================================+===============+
| or : boolean, boolean -> boolean | false |
| and : boolean, boolean -> boolean | true |
| + : integer, integer -> integer | 0 |
| * : integer, integer -> integer | 1 |
| union, or : set, set -> set | empty, false |
| inter, and : set, set -> set | full, true |
| diff : set, set -> set | full |
| insert : set, elem -> set | empty |
| remove : set, elem -> set | full |
| fby : action, action -> action | nop |
+-----------------------------------+---------------+
The iterators allow to express iterative computations in a form close
to the mathematical notation. For example, the sum of the integer numbers
from 1 to 100 may be computed with the following iterator:
<| + on K:integer among { 1 ... 100 } |> K
Similarly, the number of transitions labelled with "SEND" actions may
be computed as follows:
<| + on T:edge where T -> [ SEND ... ] |> 1
"{" x ":" T [ "among" E0 ] "where" E1 "}"
-
- is a set value defined by specifying a predicate E1 characterizing the
elements of the set. This construct is also a particular case of "
for" expression:
"for" x ":" T [ "among" E0 ]
"where" E1
"apply" union
"from" empty
"to" "{" x "}"
"end_for"
The implicitly defined sets allow to compute sets of states, labels or
transitions in a form close to the mathematical notation. For example, the
set of deadlock states (i.e., states having no successors) can be computed
by the XTL expression below:
{ S:state where succ (S) = empty }
The XTL language allows to define and use functions. The syntax
of function definitions is given by the grammar below:
FD ::= "def" F "(" x1 ":" T1"," ..."," xn ":" Tn ")" ":" RT "="
[ FD1 ... FDm ]
E
[ "where" FDm+1 ... FDm+p ]
"end_def"
| "def" "_" F "_" "(" x1 ":" T1"," x2 ":" T2 ")" ":" RT "="
[ FD1 ... FDm ]
E
[ "where" FDm+1 ... FDm+p ]
"end_def"
The first construct above defines a function
F having the parameters
x1, ...,
xn of types
T1, ...,
Tn, the body
E, and returning a result of type
RT. The calls of
F have the form:
F "(" E1"," ..."," En ")"
where the arguments
E1, ...,
En must be compatible (in number and types)
with the parameters of
F. The result of the call is equal to the value of
E computed in a context in which the parameters
xi are assigned the values
of
Ei for all i between 1 and n. The body of
F may also contain definitions
of local functions, placed either before
E, or after
E and the keyword
"
where". These functions are visible only in the expression
E. Recursive
functions are allowed. Also, functions can be overloaded: several functions
with the same name, but different profiles, may be defined in the same
scope. In case of ambiguity of the type of a function call, the "
of" expression
may be used to precise a unique type (see EXPRESSIONS above).
The second
construct above defines a binary infixed function F having the parameters
x1, x2 of types T1, T2, and returning a result of type RT. The function
F behaves like an ordinary binary function, except that its calls may be
written either in the form F "(" E1"," E2 ")", or in the form E1 F E2. This
kind of functions allow to write expressions involving infixed operators
using a syntax close to the mathematical notation. For example, the predefined
function "+" over integers is in fact an infixed operator: the user may
write either + (1, 2), or 1 + 2. The infixed operators (both predefined
and user-defined) are right-associative: e.g., the expression 1 + 2 + 3 is
parsed as 1 + (2 + 3).
Functions can be, of course, recursive (either directly,
or transitively). For example, the recursive function below computes the
factorial of an integer number:
def fact (n:integer) : integer =
assert n >= 0 in
if n = 0 then
1
else
n * fact (n - 1)
end_if
end_assert
end_def
This function also checks whether its argument is greater or equal to
0 using an "
assert" expression; if this is not the case, the program execution
is aborted with an appropriate error message.
The XTL compiler allows
to define and use macros. The syntax of macro-definitions is given by the
following grammar:
MD ::= "macro" M "(" P1"," ..."," Pn ")" "="
<text>
"end_macro"
The above construct defines a macro
M having the parameters
P1, ...,
Pn
and the body <text>, which is a portion of text built using the characters
allowed by the XTL language (see LEXICAL ELEMENTS above). The calls of
M
have the form:
M "(" <text1>"," ..."," <textn> ")"
where the arguments <text1>, ..., <textn> are portions of XTL text. The result
of the call is <text> in which all the occurrences of the parameters
Pi have
been syntactically substituted with the arguments <texti>, for all i between
1 and n. The following syntactic restriction must be satisfied: the keywords
contained in each <texti> argument must be well-bracketed, i.e., if <texti> contains
a keyword opening an expression (e.g., "
for"), then <texti> must also contain
the corresponding keyword closing the expression (e.g., "
end_for"). This also
applies to the non-alphabetic keywords such as "
(", "
)", "
[", "
]", "
{",
"
}". A macro is visible from the point of its definition until the end of
the XTL program. The macros may be overloaded: several macros with the same
name, but different arities, may be defined in the same scope.
There
is also possible to include in the text of an XTL program external libraries,
typically containing definitions of temporal operators. The inclusion command
has the following syntax:
LI ::= "library" <file0.xtl>"," ..."," <filen.xtl>
"end_library"
At the compilation of the program, the above construct is syntactically
replaced with the contents of the files <file0.xtl>, ..., <filen.xtl>, placed one
after the other in this order. The XTL compiler searches the included files
first in the current directory, then in the directory referenced by
$CADP/src/xtl
(see OPTIONS below). Multiple inclusions of the same file are silently discarded,
unless the
-warning option is passed to the compiler (see OPTIONS below);
in this case, appropriate messages are issued.
The XTL compiler
allows to declare and use in an XTL program data types and functions implemented
externally in C. The directive for an external type declaration has the
following syntax:
ETD ::= "type" T
[ "!" "implementedby" "<C_type>" ]
[ "!" "comparedby" "<C_compare>" ]
[ "!" "enumeratedby" "<C_iterate>" ]
[ "!" "printedby" "<C_print>" ]
"end_type"
where
T is the identifier of the declared type and the optional pragmas
preceded by "!" refer to the C implementation of
T: <C_type> is the identifier
of the C type implementing
T; <C_compare> is an operator for comparing two
values of type
T; <C_iterate> is a macro allowing to iterate over all values
of type
T; and <C_print> is a printing function for values of type
T. The
C names declared by these pragmas cannot be used directly in the XTL program,
but are used in the C code generated by the XTL compiler. The directive
for an external function declaration has the following syntax:
EFD ::= "func" F "(" T1"," ..."," Tn ")" ":" RT
[ "!" "implementedby" "<C_func>" ]
"end_func"
where
F is the identifier of the declared function,
T1, ...,
Tn are the types
of its parameters, and
RT is the type of its result. The optional pragma
"implementedby" declares the name <C_func> of the C function implementing
F. This C identifier cannot be used in the XTL program, but is used in the
C code generated by the XTL compiler. The external types and functions declared
using the directives above may be implemented in (one or more) C files
file1.c, ..., filen.c that must be included in the C code generated by the XTL
compiler. This is done using the following external include directive:
EID ::= "include" "<file1>", ..., "<filen>" "end_include"
where <file1>, ..., <filen> are the names of the C source files (".c" and/or ".h")
that must be included. This directive is translated into corresponding "#include"
pre-processor commands in the C code generated by the XTL compiler. The compilation
and linkediting of the C modules included may require specific parameters.
These can be indicated to the XTL compiler using the following external
compile directive:
ELD ::= "flag" "<C_compiler_directives>" "end_flag"
where <C_compiler_directives> is a portion of command-line for invoking the
C compiler (typically containing "-I", "-L", and "-l" options) that specifies
the desired compilation parameters. This portion of command-line is used
by the XTL compiler when creating the binary file of the generated C code.
As an example, the XTL program below uses the CAESAR_ERROR() function for
error handling, which is declared externally in the "caesar_standard.h"
file and defined in the OPEN/CAESAR library libcaesar.a. Upon execution,
the program will output the error message and stop.
include
"caesar_standard.h"
end_include
flag
"-I/common/Cadp/incl -L/common/Cadp/bin.sun5 -lcaesar"
end_flag
func error (string) : action
! implementedby "CAESAR_ERROR"
end_func
error ("Here occurs a fatal error. Farewell.")
The syntax of an XTL program is given by the following grammar:
PG ::= [ ( FD1 | ETD1 | EFD1 | EID1 | ELD1 )
...
( FDm | ETDm | EFDm | EIDm | ELDm ) ]
[ MD1 ... MDp ]
[ LI1 ... LIr ]
E
[ "where"
[ MDp+1 ... MDp+q ]
[ LIr+1 ... LIr+s ]
( FDm+1 | ETDm+1 | EFDm+1 | EIDm+1 | ELDm+1 )
...
( FDm+n | ETDm+n | EFDm+n | EIDm+n | ELDm+n ) ]
The expression
E is the body of the program. There may also be lists of
function definitions, external directives, macro definitions, and/or library
inclusions, placed in the front of the program or at its end, after the
"
where" keyword. The functions defined by
FD1, ...,
FDm+n are visible in the
body
E of the program, as well as in all their bodies.
- -cc options
- Pass options to the C compiler when it is invoked. options is a list of
compiler options (enclosed in quotes or double quotes). These options are
appended to the compiler options, if any, contained in the $CADP_CC environment
variable (see ENVIRONMENT VARIABLES below). Not a default option.
- -create
- Force the dynamic library of file file2[.bcg] to be created, even if it
already exists in the current directory and if it is up-to-date. Not a default
option.
- -english
- Print messages in English. Opposite of -french. This option
overrides the $CADP_LANGUAGE environment variable (see ENVIRONMENT VARIABLES
below).
- -expand
- Expand the macro definitions and the XTL source files included
as libraries in the file file1[.xtl], producing as output a file file1.xp,
and stop. This option may be useful for debugging purposes. Not a default
option.
- -french
- Print messages in French. Opposite of -english. This option
overrides the $CADP_LANGUAGE environment variable (see ENVIRONMENT VARIABLES
below).
- -remove
- Remove the dynamic library of file file2[.bcg] after usage.
Not a default option.
- -silent
- Execute silently. Opposite of -verbose. Default
option is -verbose.
- -tmp directory
- Use directory to store the temporary files.
This option overrides the environment variable $CADP_TMP (see ENVIRONMENT
VARIABLES below). Not a default option.
- -update
- Do not create the dynamic
library of file file2[.bcg] if it already exists in the current directory
and if it is up-to-date. Default option.
- -verbose
- Animate the user's screen,
telling what is going on. Opposite of -silent. Default option.
- -version
- Display
the current version number of the XTL tool and stop. To be effective, this
option should occur as the first argument on the command line. Subsequent
options and/or arguments, if any, will be discarded.
- -warning
- Print warning
messages. Not a default option.
The following environment
variables are used:
- $CADP, $CADP_LANGUAGE, $CADP_CC, $CADP_TMP
- The meaning
of these variables is defined in the $CADP/INSTALLATION file.
- $XTL
- If this
variable is set, its value should reference the directory in which the
XTL package in installed. By default, this variable is supposed to be unset:
the XTL package is normally installed in the directory referenced by the
environment variable $CADP. Setting the $XTL variable should be avoided
in official distributions of the XTL package, since it may cause problems.
Exit status is 0 if everything is alright, 1 otherwise.
When
the source XTL file
file1[
.xtl] is erroneous, error messages are issued.
Radu Mateescu (INRIA Rhone-Alpes / VASY)
- filename.xtl
- XTL
source program (input)
- filename.bcg
- LTS in BCG format (input)
- filename.xp
- XTL expanded program (output)
- filename.o
- object file (temporary)
- filename@1.o
- dynamic BCG library (auxiliary)
- $CADP/LICENSE
- license file
- $CADP/src/com/cadp_cc
- C compiler shell
- $CADP/src/xtl/*.xtl
- predefined XTL
library (input)
- $CADP_TMP/xtl_*.c
- intermediate C code (temporary)
- $CADP_TMP/xtl_*.x
- binary code (temporary)
Binary Coded Graphs - Definition of the
BCG Format,
bcg
,
bcg_io
.
Additional information is available
from the CADP Web page located at http://cadp.inria.fr
Please report
bugs to
Radu.Mateescu@inria.fr
Table of Contents
