FSP2LOTOS manual page
Table of Contents

Name

fsp2lotos - FSP to LOTOS translator

Synopsis

fsp2lotos [-version] [-pidlist] [-root root-process] filename[.lts]

Description

FSP (Finite State Processes) is a specification language for concurrent processes defined by Magee & Kramer (Imperial College, London). The fsp2lotos program translates an FSP specification to files that can be verified using CADP.

The input to fsp2lotos is an FSP file, which must have the extension .lts. If the user does not specify the extension .lts on the command line, it will be appended automatically and fsp2lotos will read filename.lts as input.

When fsp2lotos is called with the -root option and the name of a process root-process, then fsp2lotos translates root-process. Otherwise, fsp2lotos translates the first sequential process defined in filename.lts. In both cases, we call main process the process that fsp2lotos translates. The outputs are the following files:

The output files are placed in the directory whose path is given by the environment variable $FSPGEN, or in ./FSPGEN if this variable is not defined. Note that ./FSPGEN is created relative to the directory from which the user calls fsp2lotos, not relative to the directory containing the input file.

The SVL script can be run using the following Bourne shell commands:

cd ${FSPGEN:-FSPGEN}

svl svl-options

See svl for more information about the SVL tool and its options.

Once the SVL script has been executed, the generated file filename.exp can be manipulated as usual, using the EXP.OPEN tool. For instance, the BCG graph corresponding to the main process can be generated by running the following shell command:

exp.open filename.exp generator filename.bcg

See exp.open for more information about the EXP.OPEN tool and its options. Note: The name of the input file is used to construct the names of the output files, with particular rules when constructing the names of .lib files. For an input file filename.lts, fsp2lotos creates the LOTOS library FILENAME.lib, where FILENAME is constructed as follows:

Options

-version
Display the tool version and exit.

-pidlist
List the names of all processes that occur in the input file and exit. In other words, list all processes that can be used as main process (by instantiation with the -root option).

-root root-process
Use the process root-process as the main process, meaning that the generated files have the behaviour of the main process. Not a default option.

Notes About the Translation from FSP to LOTOS

Language Accepted As Input

The fsp2lotos translator supports the FSP language recognized by version 2.3 of LTSA.

In rare cases, fsp2lotos is unable to bind a local process call to its definition. If so, it issues an error message and then exits.

The following FSP constructs are not translated by fsp2lotos:

All correct FSP descriptions are accepted by fsp2lotos provided the root process is independent of those constructs. If the root process depends on any of those constructs, then fsp2lotos issues an error message and then exits.

Semantic Checks

The fsp2lotos translator does not fully check the correctness of the input FSP specification (parsing, type checking, binding, etc.). The "Build/Parse" menu of the LTSA tool should be used for such verifications. As a consequence, incorrect FSP input files may be accepted by fsp2lotos, in which case the result of the translation is irrelevant.

Translation of the Error State

The error state, represented by a state numbered -1 in LTSA, is represented by a state containing a self arc labeled by ERROR in the BCG graph corresponding to the root process.

Translation of the Non-observable Label

The non-observable label noted "tau" in FSP is represented as the LOTOS label "i" in the BCG graph corresponding to the root process.

Translation of Observable Labels

An observable FSP label is a sequence of elementary labels separated by the '.' symbol. Formally, any observable FSP label has the form A1.A2...An, where n is greater or equal to 1, and where each elementary label Ai is either a number (e.g., "-4", "0", "1") or an FSP identifier written in lower-case letters (e.g., "x", "y1", "read").

Each observable FSP label A1.A2...An is translated into a LOTOS label of the form "EVENT !L1.L2...Ln.NIL", where each Li is derived from the corresponding Ai according to the following rules: if Ai is a number, then Li is the same number; if Ai is an FSP identifier, then Li is the same identifier converted to upper-case letters. Such identifiers are declared in the Symbol LOTOS type defined in FILENAME.lib.

Operands

filename.lts
FSP specification (input)

$FSPGEN/filename.exp
Network of LTS (output)

$FSPGEN/filename.lotos
LOTOS code (output)

$FSPGEN/FILENAME.lib
LOTOS code (output)

$FSPGEN/filename.svl
SVL script (output)

$FSPGEN/filename.f
C code (output)

$FSPGEN/filename.t
C code (output)

Files

$CADP/lib/FSP_V1.lib
FSP predefined library (LOTOS code)

$CADP/incl/FSP_V1.h
FSP predefined library (C code)

Environment Variables

$FSPGEN
The target directory of the output files.

Exit Status

If the translation was successful the exit status is 0, even if warnings were issued during the execution. If any error occurred during translation, the exit status is 1.

Bibliography

Authors

Remi Herilier, Frederic Lang, and Gwen Salaun, with contributions from Hubert Garavel (all at INRIA Rhone-Alpes).

See Also

See the following reference manuals: bcg , caesar , caesar.adt , exp , exp.open , fsp.open , lotos , lotos.open , svl , svl-lang , xeuca .

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

The tool fsp2lotos may accept FSP specifications that are rejected by LTSA. In this case, incorrect code may be generated. Please report any mistranslations or other problems with fsp2lotos to cadp@inria.fr

Table of Contents