Table of Contents
caesar - compilation & verification of LOTOS specifications
caesar
[
-aldebaran] [
-analysis] [
-bcg] [
-cc options] [
-comments] [
-english] [
-error]
[
-exec] [
-exit] [
-external] [
-e7] [
-e7old] [
-force] [
-french] [
-functionality]
[
-gc] [
-gradual] [
-graph] [
-indent] [
-iso] [
-map] [
-monitor] [
-more command] [
-network]
[
-newstyle] [
-oldstyle] [
-open] [
-root instantiation] [
-safety] [
-silent] [
-simulator]
[
-trigger optimization] [
-verbose] [
-version] [
-v3] [
-v4] [
-warning]
filename[
.lotos]
Taking as input
filename.lotos, which is a LOTOS program, and
filename.h, which is the concrete implementation in C of the abstract data
types defined in the LOTOS source text,
caesar translates it to a C program
and/or a finite state automaton. This allows to execute, simulate, and/or
verify LOTOS programs.
- -aldebaran
- Generate output file filename.aut,
which contains the automaton in the AUT textual format. Not a default option.
- -analysis
- Analyze filename.lotos in order to detect errors and stop. The following
phases are performed: syntactic analysis, static semantic analysis, restriction,
expansion and generation. This option does not generate any output, except
error diagnostics. Not a default option.
- -bcg
- Generate output file filename.bcg,
which contains automaton in the BCG (Binary-Coded Graphs) format. Default
option unless one of the following options is set: -aldebaran, -graph, -exec,
or -open.
- -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.
- -comments
- Issue a warning message for each LOTOS sort or operation
that is not properly labelled by a special comment of the form
(*!...*). Not
a default option.
- -english
- Print messages in English. Opposite of -french. This
option overrides the $CADP_LANGUAGE environment variable (see ENVIRONMENT
VARIABLES below).
- -error
- A file, filename.err, is generated by caesar. It contains
detailed error diagnostics. When it terminates, caesar displays the content
of this file on the screen, using the $CADP/src/com/cadp_more command,
unless -error option is set.
- -exec
- Generate the kernel module filename.c to
be used in the EXEC/CAESAR environment. Not a default option.
- -exit
- Perform
network reduction in order to replace all tau-transitions derived from a
LOTOS enabling operator ">>" by epsilon-transitions, often leading to a smaller
graph. This transformation preserves safety and trace equivalence, but
neither strong, branching, nor observational equivalence. Not a default
option.
- -external
- Generate a file filename.c.proto containing skeletons for
EXEC/CAESAR's gate functions, i.e., functions associated to all visible gates
of the LOTOS specification. These functions are incomplete and have to be
completed manually (at the places marked "...") with input/output operations
so as to interface the LOTOS specification with its real environment. This
option must be used together with the -exec option. Not a default option.
Note: if filename.c.proto already exists in the current directory, caesar
will not overwrite it, because it might have been modified manually.
- -e7
- Do not perform the new (BDD based) optimization E7, which removes dead
transitions, still preserving strong equivalence. Not a default option.
- -e7old
- Perform the old (explicit-state based) optimization E7 instead of the new
(BDD based) optimization E7. Not a default option.
- -force
- Force caesar to
regenerate filename.c even if not necessary. This option is only meaningful
if caesar is used with options -exec (EXEC/CAESAR mode), -open (OPEN/CAESAR
mode), or -simulator. Not a default option. By default caesar will attempt
not to regenerate filename.c if this file already exists in the current
directory, and if it has been modified more recently than
(1) the corresponding LOTOS file (filename.lotos, filename.lot, or filename.l),
(2) than any LOTOS library transitively included (using the "library" clause)
in this LOTOS file, and
(3) than any C file transitively included (using the "#include" clause)
in filename.c itself.
- -french
- Print messages in French. Opposite of -english.
This option overrides the $CADP_LANGUAGE environment variable (see ENVIRONMENT
VARIABLES below).
- -functionality
- Do not check functionality constraints (``
exit''
and ``noexit''). Not a default option.
- -gc
- Invoke the Boehm-Demers garbage collector
to reuse the (potentially large) amounts of memory that have been allocated
for abstract data types and that are no longer used. This option is especially
suitable for LOTOS descriptions involving dynamic data structures, such
as: lists, queues, stacks, etc. Not a default option.
- -gradual
- Apply the optimizations
gradually when generating the network. By default, the optimizations are
applied only after the network is fully generated. Using this option, the
optimizations are applied to each sub-network generated from each operand
of a parallel composition operator. This option is slower, but it can be
useful for dealing with larger LOTOS descriptions and/or for generating
smaller networks. Not a default option.
- -graph
- Generate output file filename.gph,
which contains the automaton in an undocumented, disk space expensive format.
Not a default option.
- -indent
- Do not format using the shell-script located
in $CADP/src/com/cadp_indent the file filename.c.proto generated by option
-external. Not a default option.
- -iso
- Use the standard LOTOS semantics defined
in ISO 8807, disabling several non-standard language enhancements implemented
in caesar. Namely, this option: (1) considers "i" and "I" as reserved keywords,
thus preventing to declare any identifier named "i" or "I"; (2) enforces
the standard (and seemingly questionable) semantics for flattening parameterized
types, instead of the modified semantics proposed in the document "$CADP/doc/*/Garavel-Sighireanu-95.*".
Not a default option.
- -map
- Generate filename.map, which gives correspondence
between sort and operation names occuring in filename.lotos and C type and
function names occuring in filename.h. Not a default option.
- -monitor
- Open
a window for monitoring in real-time the generation of a BCG graph (see
option "-bcg" above). Not a default option.
- -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.
- -network
- Generate output file
filename.net, which contains the Petri net in an undocumented format. Not
a default option.
- -newstyle
- When generating skeletons for EXEC/CAESAR's gate
functions (see -external option above), use the new-style function declarations
(i.e., with prototypes) introduced in ANSI/ISO Standard C. This option must
be used together with the -external option. Default option when option -external
is selected.
- -oldstyle
- When generating skeletons for EXEC/CAESAR's gate functions
(see -external option above), use the old-style function declarations (i.e.,
without prototypes) available in Kerninghan and Ritchie C. This option is
only applicable when gate functions are not overloaded, i.e., when each gate
is always used with the same number of offers, and with offers of the same
sorts and same directions (input or output). This option must be used together
with the -external option. Not a default option.
- -open
- Generate the graph module
filename.c to be used in the OPEN/CAESAR environement. Not a default option.
- -root instantiation
- Restrict the behaviour of the specification to the specified
instantiation, meaning that the behaviour-expression occurring after the
behaviour keyword is actually replaced by instantiation. instantiation is
a character string (preferably enclosed in single quotes) denoting a LOTOS
process instantiation. It can have either the form '
P' or the form 'P [G1,
..., Gn]', where P is a process-identifier defined in filename.lotos, and where
G1, ..., Gn are gate-identifiers. If '[G1, ..., Gn]' is omitted, it will be replaced
by the formal gate-parameters list of process P. There should be at most
one process named P in filename.lotos. This process P should have no value-parameters
(an instantiation to process P' with value-parameters should be encapsulated
in the definition of another process P without value parameters, to which
the -root is applicable). Not a default option.
- -safety
- Perform network reduction
in order to replace all tau-transitions by epsilon-transitions, often leading
to a smaller graph. This transformation preserves safety and trace equivalence,
but neither strong, branching, nor observational equivalence. Not a default
option.
- -silent
- Execute silently. Opposite of -verbose. Default option is -verbose.
- -simulator
- Generate the simulator program filename.c and stop, neither compiling
nor removing this file. This option is useful when the simulator program
is so large that it breaks the C compiler, or when it compiles and executes
too slowly. In such case, filename.c can be compiled and run on a more efficient
machine. Not a default option.
- -trigger optimization
- Print statistics about
which optimizations cause a given optimization to become effective. This
option is only useful for CAESAR's development. Not a default option.
- -verbose
- Report activities and progress, including errors, to the user's screen. Opposite
of -silent. Default option is -verbose.
- -version
- Display the current version
number of the software and stop. Not a default option.
- -v3
- Do not perform
optimization V3, which discovers variables whose values remain constant
during the simulation phase, and replaces them by constants. Not a default
option.
- -v4
- Do not perform optimization V4, which evaluates statically guards
whose value is constant and removes transitions whose guard is false. Not
a default option.
- -warning
- Suppress all warning diagnostics, at the risk
of leaving actual issues in the LOTOS specification undetected. Not a default
option.
- $CADP_LANGUAGE
- If this variable is set, its
value determines the language in which diagnostic messages will be reported.
Possible values are 'french' and 'english'. Incorrect values will be ignored
silently. If this variable is unset, it is given the default value 'french'.
- $CADP_CC
- If this variable is set, its value determines the name of the
C compiler that will be invoked by caesar. See file $CADP/INSTALLATION for
detailed information about this variable. If this variable is unset, the
script-shell $CADP/src/com/cadp_cc will automatically determine the C compiler
to be used by default.
- $CADP_TMP
- If this variable is set, its value determines
the directory in which temporary files are created. If this variable is
unset, it is given the default value '/tmp'.
- $PAGER
- If this variable is set,
its value will be used by the script-shell $CADP/src/com/cadp_more to display
any error messages or warnings.
When the source is erroneous,
error messages are issued. Exit status is 0 if everything is alright, 1
otherwise.
Hubert Garavel and Wendelin Serwe (INRIA Rhone-Alpes)
- filename.lotos
- LOTOS specification (input)
- filename.h
- implementation in C
of data types (input)
- filename.c
- C code of the simulator (output of -simulator)
- filename.c
- C code of the graph module (output of -open)
- filename.c
- C code
of the kernel module (output of -exec)
- filename.c.proto
- skeleton for gate
functions (output of -external)
- filename.aut
- automaton for ALDEBARAN (output)
- filename.net
- default Petri net format (output)
- filename.gph
- debugging automaton
for debugging (output)
- filename.err
- detailed error messages (output)
- filename.map
- ADT correspondence table (output)
- libname.lib
- user ADT library (input)
- $CADP/lib/libname.lib
- predefined ADT library (input)
- $CADP/src/com/cadp_cc
- C compiler shell
- $CADP/src/com/cadp_more
- pager shell
- $CADP/gc
- Boehm-Demers
garbage collector (input)
- $CADP/LICENSE
- license file
- $CADP_TMP/*.c
- C code generated during type survey (temporary)
- $CADP_TMP/*.c
- C code generated during optimization (temporary)
- $CADP_TMP/*.x
- binary
code for type survey (temporary)
- $CADP_TMP/*.x
- binary code for optimization
(temporary)
- $CADP_TMP/*.x
- binary code of simulator program (temporary)
- $CADP_TMP/*.inf
- results of information phase (temporary)
- $CADP_TMP/*.tsv
- results of type
survey (temporary)
- $CADP_TMP/*.bpn
- Basic Petri Net for optimization (temporary)
- $CADP_TMP/*.oe7
- results of old optimization E7 (temporary)
- $CADP_TMP/*.ov3
- results of optimization V3 (temporary)
- $CADP_TMP/*.ov4
- results of optimization
V4 (temporary)
- $CADP_TMP/*.ov7
- results of optimization V7 (temporary)
CAESAR Reference Manual, OPEN/CAESAR Reference Manual,
aldebaran
,
bcg
,
caesar.adt
,
caesar.bdd
Additional information is
available from the CADP Web page located at http://cadp.inria.fr
Directives
for installation are given in file $CADP/INSTALLATION.
Recent changes and
improvements to this software are reported and commented in file $CADP/HISTORY.
Known bugs are described in the Reference Manual of CAESAR. Please report
new bugs to
Hubert.Garavel@inria.fr
Table of Contents
