CAESAR.OPEN manual page
Table of Contents

Name - OPEN/CAESAR connection for the LOTOS language

Synopsis [-link|-include] [caesar_opt] spec[.lotos] [cc_opt] prog[.a|.c|.o] [prog_opt]


Taking as input a LOTOS specification spec.lotos and an OPEN/CAESAR program prog[.a|.c|.o], generates an executable program prog. To do so, 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 automatically invokes caesar if the graph module spec.c does not exist or is out of date. 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). 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, attempts to fetch it in the OPEN/CAESAR binary library $CADP/bin.`arch`.

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

If prog.o is not present in the current directory, 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, 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, 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.


Select include mode. Not a default option.

Select link mode. Default option.

The options caesar_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: spec.lotos -O prog.a
or spec.lotos -O prog.c
or spec.lotos -O prog.o
or -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.


Hubert Garavel (INRIA Rhone-Alpes)


LOTOS specification (input)

implementation in C of data types

external type C implementation

external function C implementation

graph module gen. by CAESAR from spec.lotos      

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

exploration module (archive, input)

exploration module (source, input)

exploration module (object code, input)

executable program (output)


temporary files

interface of the graph module

interfaces of the storage module

object code of the storage module

library of exploration modules (source)

library of exploration modules (archive)

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

Directives for installation are given in files $CADP/INSTALLATION_*.

Recent changes and improvements to this software are reported and commented in file $CADP/HISTORY.


Please report new bugs to

Table of Contents