LOTOS.OPEN manual page
Table of Contents

Name

lotos.open - OPEN/CAESAR connection for the LOTOS language

Synopsis

lotos.open [-link|-include] [lotos_opt] spec[.lotos] [cc_opt] prog[.a|.c|.o] [prog_opt]

Description

Taking as input a LOTOS specification spec.lotos and an OPEN/CAESAR program prog[.a|.c|.o], lotos.open generates an executable program prog. To do so, lotos.open performs appropriate calls to caesar , caesar.adt , and the C compiler, avoiding recompilation whenever possible. Finally, prog is executed.

According to the principles of the OPEN/CAESAR architecture, prog is obtained by combining three different modules:

Processing of the Graph Module

lotos.open automatically invokes caesar if the graph module spec.c does not exist or is out of date.

lotos.open automatically invokes caesar.adt if the abstract data type implementation spec.h does not exist or is out of date. However, if spec.h exists and has not been generated using caesar.adt , it will not be overwritten, even if it is out of date (in this case, a warning is issued).

lotos.open takes into account the dependencies possibly created by spec.c, spec.h, spec.t, and spec.f.

Processing of the Exploration Module

The exploration module prog[.a|.c|.o] is supposed to contain an OPEN/CAESAR application program, such as exhibitor , terminator , xsimulator ...

The exploration module can be supplied in three different forms. It can be either an archive file (with .a suffix), or a source C program (with .c suffix) or an object code file (with .o suffix).

If prog.a is not present in the current directory, lotos.open attempts to fetch it in the OPEN/CAESAR binary library $CADP/bin.`arch`.

If prog.c is not present in the current directory, lotos.open attempts to fetch it in the OPEN/CAESAR source library $CADP/src/open_caesar.

If prog.o is not present in the current directory, lotos.open attempts to fetch it in the OPEN/CAESAR binary library $CADP/bin.`arch`.

If no suffix (.a, .c, .o) is specified on the command line for the exploration module prog, lotos.open will make successive attempts to fetch this exploration module: first, as a source C program with .c suffix; then as an archive file with .a suffix; finally as an object code file with suffix .o.

Determination of Include or Link Mode

If the exploration module is in source form, lotos.open examines prog.c in order to determine automatically whether link mode or include mode should be used.

If the exploration module is in archive form or in object code form, only the link mode is allowed.

Options

-include
Select include mode. Not a default option.

-link      
Select link mode. Default option.

The options lotos_opt, if any, are passed to caesar and to caesar.adt .

The options cc_opt, if any, are passed to the C compiler.

The options prog_opt if any, are passed to prog.

Examples:

lotos.open spec.lotos -O prog.a
or
lotos.open spec.lotos -O prog.c
or
lotos.open spec.lotos -O prog.o
or
lotos.open -comments -gc spec.lotos prog -size 1000

Exit Status

When the source is erroneous, error messages are issued. Exit status is 0 if everything is alright, 1 otherwise.

Author

Hubert Garavel (INRIA Rhone-Alpes)

Name

Originally, this command was named caesar.open; this name was changed to lotos.open in February 2020 for increased clarity and consistency.

Operands

spec.lotos
LOTOS specification (input)

spec.h      
implementation in C of data types

spec.t      
external type C implementation

spec.f      
external function C implementation

spec.c      
graph module gen. by CAESAR from spec.lotos      

spec.o      
object code gen. by the C compiler. from spec.c      

prog.a      
exploration module (archive, input)

prog.c      
exploration module (source, input)

prog.o      
exploration module (object code, input)

prog      
executable program (output)

Files

/tmp/lotos.open.*
temporary files

$CADP/incl/caesar_graph.h
interface of the graph module

$CADP/incl/caesar_*.h
interfaces of the storage module

$CADP/bin.`arch`/libcaesar.a
object code of the storage module

$CADP/src/open_caesar/*.c
library of exploration modules (source)

$CADP/bin.`arch`/*.a
library of exploration modules (archive)

$CADP/bin.`arch`/*.o
library of exploration modules (object code)

See Also

OPEN/CAESAR Reference Manual, caesar , caesar.adt , lotos

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 new bugs to Hubert.Garavel@inria.fr

Table of Contents