Table of Contents
xtl - evaluation of value-based temporal logic formulas
xtl
[
-cc options ] [
-create] [
-depend] [
-english] [
-expand] [
-french] [
-remove] [
-silent]
[
-source file:line ] [
-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.
A detailed description of the
XTL language is available in the xtl-lang
manual page.
- -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.
- -depend
- Display the list of library files included (directly or transitively)
in the file file1[.xtl] and stop. This list may be incomplete if the XTL
program is syntactically incorrect. If present, this option has precedence
over all the other options. 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.
- -source file:line
- Change the file name and line number displayed in error messages as if
the XTL program was contained in file file starting at line line (instead
of starting at line 1 in file file1[.xtl]). This option has effect only on
the messages triggered by the errors occurring in the top-level file file1[.xtl].
The messages triggered by the errors occurring in the included libraries
(if any) are left unchanged.
- -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 extra
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_2 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)
bcg
,
bcg_io
,
xtl
.
Additional information is available from the CADP Web page located at http://cadp.inria.fr
Directives for installation are given in files $CADP/INSTALLATION_*.
Recent
changes and improvements to this software are reported and commented in
file $CADP/HISTORY.
Please report bugs to
Radu.Mateescu@inria.fr
Table of Contents
