XTL manual page
Table of Contents

Name

xtl - evaluation of value-based temporal logic formulas

Synopsis

xtl [ -cc options ] [-create] [-english] [-expand] [-french] [-remove] [-silent] [ -tmp directory ] [-update] [-verbose] [-version] [-warning] file1[.xtl] file2[.bcg]

Description

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:

A detailed description of the XTL language is available in the xtl-lang manual page.

Options

-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 extra warning messages. Not a default option.

Environment Variables

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

Exit status is 0 if everything is alright, 1 otherwise.

Diagnostics

When the source XTL file file1[.xtl] is erroneous, error messages are issued.

Author

Radu Mateescu (INRIA Rhone-Alpes / VASY)

Operands

filename.xtl
XTL source program (input)

filename.bcg
LTS in BCG format (input)

filename.xp
XTL expanded program (output)

Files

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)

See Also

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.

Bugs

Please report bugs to Radu.Mateescu@inria.fr


Table of Contents