fsp2lotos [-version] [-pidlist] [-root root-process] filename[.lts]
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:
output files are placed in the directory whose path is given by the environment
$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:
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:
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:
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.
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.
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.
The non-observable label noted "tau" in FSP is represented as the LOTOS label "i" in the BCG graph corresponding to the root process.
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.
Remi Herilier, Frederic Lang, and Gwen Salaun, with contributions from Hubert Garavel (all at INRIA Rhone-Alpes).
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.
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 email@example.com