What is CADP?
Home Page Tools Overview Current Status Recent Changes
Installation
How to obtain CADP? Usage Statistics
Documentation
FAQ Tutorials Publications Manual Pages Demo Examples Wikipedia
CADP Community
Newsletters Education & Training Case Studies Research Tools Forum
CADP Resources
VLSAT Benchmarks VLTS Benchmarks Other Resources
About CADP
Contributors

Table of Contents

Name

lpp - LNT pre-processor

Synopsis

lpp [-version] [-silent | -verbose] [-force] [-more command] [input[.lnt]] [output[.lnt]]

Description

lpp is a pre-processor that operates on LNT code. lpp was designed to be used in conjunction with lnt2lotos, which translates LNT code into LOTOS and expects to have its input previously expanded by lpp.

lpp was developed to palliate the fact that the LNT language supports notations for literal constants (such as numbers, characters, strings, etc.) that do not exist in LOTOS. lpp expands such notations into lower-level algebraic terms that are compatible with the LOTOS syntax. These terms use the algebraic sorts and operations contained in the LNT_V1 predefined library of CADP.

• If no input file name is specified on the command line, or if the input file name is the "-" string, lpp acts as a pipe, i.e., it reads from standard input and writes to standard output. In this case, no output file name must be specified on the command line.
• If an input file name (different from "-") is specified on the command line, it should contain only letters, digits, and underscores. The extension .lnt, if absent from the command line, will be appended automatically, so that lpp will read input.lnt.
• If no output file name is specified on the command line, the expanded code produced by lpp is written to a file named input.lnt, which is placed in a special directory that lpp creates if it does not exist already. If the creation of the directory fails, lpp issues an error message and stops. The name of this directory is either given by the environment variable $LNTGEN, if this variable is set, or is ./LNTGEN. Note that ./LNTGEN (or $LNTGEN) is created relative to the directory from which the user calls lpp, not relative to the directory containing the input file.
• If an output file name is specified on the command line, it should contain only letters, digits, and underscores. The extension .lnt, if absent from the command line, will be appended automatically, so that the expanded code produced by lpp is written to output.lnt.

To ensure that the input file will not be overwritten, lpp stops if the output file is the same as the input file.

To avoid clashes between generated files and user-written files, lpp writes a special tag at the end of each generated file. This tag is a comment containing the name and the version of lpp that generated the file. lpp uses this tag for two purposes:

• To prevent lpp from overwriting a file that was not generated by itself: if the output file already exists but has no special tag or has an invalid tag indicating that the file was not generated by the right tool, lpp issues an error message and stops.
• To avoid unnecessary compilations: lpp pre-processes an LNT file only if the source file was modified since the last translation, or if the output file was generated by an older version of lpp.

Options

-silent

Execute silently, reporting only errors. This is the opposite of -verbose. The default option is -verbose.

-verbose

Report activities and progress, including errors, to the user's screen. This is the opposite of -silent. The default option is -verbose.

-version

Display the tool version and exit.

-force

Overwrite the output file, even if it was edited by the user or does not need to be updated.

-more command

Use command to display the error messages, instead of "$CADP/src/com/cadp_more", which is the default. command is a shell command (preferably enclosed in quotes or double quotes) containing the pathname of the chosen pager, possibly followed by a list of options. Not a default option.

Environment Variables

$LNTGEN

The target directory of the output file. This environment variable has no effect if an output file argument is supplied.

Exit Status

If no error occurred, 0, otherwise 1.

Authors

David Champelovier, Hubert Garavel, Yves Guerte, Wendelin Serwe, Gideon Smeding (INRIA Rhone-Alpes)

See Also

caesar.adt , caesar , lotos , lnt.open , lnt2lotos , and the "Reference Manual of the LNT to LOTOS Translator" available from http://cadp.inria.fr/publications/Champelovier-Clerc-Garavel-et-al-10.html

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 any bugs to cadp@inria.fr

---

Table of Contents

• Name
• Synopsis
• Description
• Options
• Environment Variables
• Exit Status
• Authors
• See Also
• Bugs