Table of Contents
exp.open - OPEN/CAESAR connection for EXP networks of communicating
] [-hidden string
] [-coaction string
] [-network format
Taking as input filename.exp,
a network of communicating automata in the EXP 2.0, see exp
an OPEN/CAESAR program user
generates an OPEN/CAESAR graph
This file is then compiled into filename.o
and an executable
resulting from the combination of filename.o
is produced. Finally, user
According to the principles of the
OPEN/CAESAR architecture, user is obtained by combining three different
- the graph module is generated from filename.exp
- the storage module
is the standard OPEN/CAESAR library
- the exploration module is user[.a|.c|.o]
The exploration module user
supposed to contain an OPEN/CAESAR application program, such as evaluator
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 user.a is not present in the current directory, exp.open attempts to fetch
it in the OPEN/CAESAR binary library $CADP/bin.`arch`.
If user.c is not present
in the current directory, exp.open attempts to fetch it in the OPEN/CAESAR
source library $CADP/src/open_caesar.
If user.o is not present in the current
directory, exp.open attempts to fetch it in the OPEN/CAESAR binary library
If no suffix (.a, .c, .o) is specified on the command line
for the exploration module user, exp.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 .o suffix.
- Perform on-the-fly partial order reduction
modulo branching bisimulation. This yields a generally smaller graph, which
is equivalent modulo branching bisimulation to the graph obtained using
the -strong option. The used technique is based on prioritization of so-called
tau-confluent transitions [Pace-Lang-Mateescu-03]. This is not a default option.
- Force the distinction between lowercase and uppercase characters
in labels occurring within the operators used in filename.exp. This is the
default option if no reference language is selected or if the reference
language is E-LOTOS or mCRL. In other cases, labels occurring within the
operators used in filename.exp are automatically turned to uppercase. Therefore,
labels in LTSs should also be uppercase, except possibly the strings representing
the hidden label, termination label, and co-action prefix.
- Set CCS as
the reference language. This is not a default option. See Section LANGUAGE
PARAMETERS of exp
- -coaction string
- Set string so as to
prefix CCS co-action labels; string is named co-action prefix. See Section
CCS PARALLEL COMPOSITION of exp
for more information about the co-action
- Set CSP as the reference language. This is not a default option.
See Section LANGUAGE PARAMETERS of exp
- Perform on-the-fly partial order reduction preserving deadlocks. This yields
a generally smaller graph, which contains the same deadlocks as the graph
obtained using the -strong option. This is not a default option.
- Set E-LOTOS as the reference language. This is not a default
option. See Section LANGUAGE PARAMETERS of exp
- -hidden string
- Set string as denoting the hidden label in BCG files of both the communicating
automata and of the automaton corresponding to their composition. The default
value depends on the reference language, see Section LANGUAGE PARAMETERS
Note that many CADP tools (such as for instance
, etc.) require the hidden label to be written
"i". If it is written differently, e.g., "tau", then one may use the "-hidden
i" option and hide "tau" in each communicating automaton, by using the
hiding operator of EXP 2.0.
Note also that the hidden label is usually written
"tau" in the FC2 format. During conversion from FC2 communicating automata
into BCG, "tau" labels are automatically renamed into "i" by the bcg_io
tool. Therefore, since bcg_io is systematically called to translate FC2
components into the BCG format, the hidden label should be set to "i",
using "-hidden i", even though some component is in the FC2 format, with
"tau" denoting the hidden label.
- Record a history of each label.
The history can be read using the CAESAR_INFORMATION_LABEL function of
the OPEN/CAESAR API. With the -history option, it is possible to set FORMAT_LABEL
(see the OPEN/CAESAR manual) to a natural number up to 3 (instead of 2
o The behaviour of CAESAR_INFORMATION_LABEL with FORMAT_LABEL
set to 0 or 1 is described in the OPEN/CAESAR documentation.
o If FORMAT_LABEL
is equal to 2, then information about the synchronisations involved in
the computation of each label is displayed under the form of a synchronisation
o If FORMAT_LABEL is equal to 3, then the displayed synchronisation
vector is extended with information about hidings and renamings performed
to produce the label.
This is not a default option.
- Print structural
information about the LTSs referenced in filename.exp and stop. See bcg_info
for more information.
- Generate an OPEN/CAESAR graph module that does
not depend on BCG files. This option cannot be combined with -branching,
-deadpreserving, -weaktrace, and/or the priority operator. Debugging option,
not available in official releases of CADP.
- -interface interface_directives
- This option allows to generate a refined interface as explained in the
This option assumes that the composition of LTSs stored
in filename.exp corresponds to a system of concurrent processes S as follows:
The concurrent architecture of filename.exp is the same as the concurrent
architecture of S, and each LTS in filename.exp represents either the state
space (named concrete LTS in the sequel) or simply the set of labels (named
abstract LTS in the sequel) of the corresponding process in S; States and
transitions of abstract LTSs are irrelevant.
Consider processes P0, P1,
..., Pm of S, such that, in filename.exp, the LTS corresponding to P0 is abstract
and the LTSs corresponding to P1, ..., Pm are concrete. The -interface option
allows to synthesize an interface representing the synchronization constraints
imposed on P0 by P1, ..., Pm. This interface has the form of an OPEN/CAESAR
graph module stored in a file named filename.c and a list of synchronisation
labels stored in a file named filename.sync. The graph module can be translated
into an explicit LTS using the generator
tool. The resulting LTS
can then be given, together with filename.sync, to the projector
tool so as to restrict the behaviour of P0.
The interface_directives argument
has the form "nat:nat_list", where nat is a natural number and nat_list
is a list of natural numbers separated by blank characters. Each of these
natural numbers is an index corresponding to the rank of occurrence of
an LTS in filename.exp (once eventual .exp file names have been substituted
by the expression stored in the corresponding .exp files). Index 1 represents
the leftmost LTS. The left-hand side of ":" is the index of the LTS corresponding
to P0. The right-hand side of ":" is the list of indices of the LTSs corresponding
to P1, ..., Pm. interface_directives must be parsed as a single argument on
the command line and thus must be enclosed in quotes.
that some of the automata in filename.exp have been obtained by semi-composition
with "user-given" restriction interfaces, and compute the associated validation
predicates. Note that this option does not make sense outside a compositional
verification process using restriction interfaces. See projector
for more information about using restriction interfaces.
This is not a default option.
- Display the number of labels followed
by the list of labels potentially occurring in the state space of the input
network of communicating automata and stop. If the -interfaceuser option
is set, do not print the labels representing validation predicates (see
- Set LOTOS as the reference language. This is
not a default option. See Section LANGUAGE PARAMETERS of exp
- Set mCRL as the reference language. This is not a default option.
See Section LANGUAGE PARAMETERS of exp
- -network format
- Generate a network equivalent to filename.exp in one of "nupn", "pep", "tina",
"fc2", or "txt" format and stop:
If format is "nupn", exp.open generates
a file named filename.nupn, containing a Petri net in the NUPN (Nested Unit
Petri Net) file format [Garavel-15-a] (see caesar.bdd
for a description
of the NUPN format);
If format is "pep", exp.open generates a file named
filename.ll_net, containing a Petri net in the low-level PEP file format
If format is "tina", exp.open generates a file named
filename.tpn, containing a Petri net in the ``tpn'' format of the TINA toolbox
If format is "fc2", exp.open generates a file
named filename.fc2, containing a network of automata in the FC2 format [Bouali-Ressouche-Roy-deSimone-96].
If format is "txt", exp.open generates a file named filename.txt, containing
a description of the network of automata in an undocumented textual format.
This description includes the list of files containing the communicating
automata, the list of labels potentially occurring in the product and,
for each label, the list of synchronization vectors.
and fc2link tools are called internally to make the conversion from EXP
to FC2. Note however that fc2link is not provided within CADP but belongs
to the Fc2Tools distribution, which can be downloaded at http://www-sop.inria.fr/meije/verification.
Moreover, when converting EXP to FC2, the hidden event must be written
"i" (see -hidden option above and Section LANGUAGE PARAMETERS of exp
for details) because this is required by bcg_io
option does not require an exploration module. This is not a default option.
This option is not available if filename.exp contains a priority operator.
- Parsing of EXP behaviours is generally followed by a static semantics
verification phase to verify that behaviours are well-formed. Option -nocheck
skips this verification phase. This option should be used with caution since
the semantics of ill-formed behaviours is undefined. This is not a default
- Do as the -branching option and also attempt partial
minimization of the graph (on-the-fly) for stochastic branching bisimulation,
by giving priority to hidden actions over stochastic transitions (see the
manual page for details about stochastic transitions), thus
taking an account of the maximal progress of hidden actions.
silently. Opposite of -verbose. Default option is -verbose.
- Do not perform
partial order reduction of the graph. This is a default option.
- Set string as denoting the gate used to express behaviour termination.
The default value depends on the reference language, see Section LANGUAGE
PARAMETERS of exp
- Use the "-bcg -unparse" options
of bcg_io while converting LTSs in AUT, FC2, or SEQ formats into BCG. See
manual page for details about these options.
activities and progress, including errors, to the user's screen. Opposite
of -silent. Default option is -verbose.
- Display the version number
- Perform on-the-fly partial order reduction modulo weak
trace equivalence. This yields a generally smaller graph, which is equivalent
modulo weak trace equivalence to the graph obtained using the -strong option.
This is not a default option.
- if any, are passed to the C compiler.
- if any, are passed to user.
Exit status is 0 if
everything is all right, > 0 otherwise.
Berthomieu, P.-O. Ribet, and F. Vernadat. The tool TINA - Construction of Abstract
State Spaces for Petri Nets and Time Petri Nets. In International Journal
of Production Research, Vol. 42, No 14, July 2004.
Best and Bernd Grahlmann. "PEP Documentation and User Guide." http://parsys.informatik.uni-oldenburg.de/~pep/paper.html.
- Amar Bouali, Annie Ressouche, Valerie
Roy, and Robert de Simone. The Fc2Tools set: a Toolset for the Verification
of Concurrent Systems. In R. Alur and T.A. Henzinger, editors, Proceedings
of the 8th Conference on Computer-Aided Verification (New Brunswick, New
Jersey, USA). Lecture Notes in Computer Science volume 1102, Springer-Verlag,
- S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. "A
Theory of Communicating Sequential Processes." In Journal of the ACM, vol.
31, number 3, pages 560-599. ACM, 1984.
- Hubert Garavel. "Nested-Unit
Petri Nets: A Structural Means to Increase Efficiency and Scalability of
Verification on Elementary Nets." In R. Devillers and A. Valmari, editors,
Proceedings of the 36th International Conference on Application and Theory
of Petri Nets and Concurrency (Brussels, Belgium). Lecture Notes in Computer
Science volume 9115, Springer-Verlag, 2015. Available from http://cadp.inria.fr/publications/Garavel-15-a.html
- Hubert Garavel and Mihaela Sighireanu. "A Graphical
Parallel Composition Operator for Process Algebras." In J. Wu, Q. Gao, and
S.T. Chanson, editors, Proceedings of the Joint International Conference
on Formal Description Techniques for Distributed Systems and Communication
Protocols, and Protocol Specification, Testing, and Verification FORTE/PSTV'99
(Beijing, China). Kluwer Academic Publishers, 1999. Available from http://cadp.inria.fr/publications/Garavel-Sighireanu-99.html
- J.F. Groote and A. Ponse. "The syntax and semantics of mCRL."
In A. Ponse, C. Verhoef and S.F.M. van Vlijmen, editors, Algebra of Communicating
Processes '94, Workshops in Computing Series, Springer-Verlag, pp. 26-62, 1995.
Also appeared as: Technical Report CS-R9076, CWI, Amsterdam, 1990.
"LOTOS --- A Formal Description Technique Based on the Temporal Ordering of
Observational Behaviour." International Organization for Standardization
--- Information Processing Systems --- Open Systems Interconnection. International
Standard number 8807. Geneva, September 1989.
- ISO/IEC. "Enhancements
to LOTOS (E-LOTOS)." International Organization for Standardization --- Information
Technology. International Standard number 15437:2001. Geneva, September 2001.
- Frederic Lang. "EXP.OPEN 2.0: A Flexible Tool Integrating Partial
Order, Compositional, and On-the-fly Verification Methods." In J. van de Pol,
J. Romijn and G. Smith, editors, Proceedings of the 5th International Conference
on Integrated Formal Methods IFM'2005 (Eindhoven, The Netherlands). Lecture
Notes in Computer Science volume 3771, Springer-Verlag, 2005. Available from
- Frederic Lang. "Refined
Interfaces for Compositional Verification." In E. Najm, J.-F. Pradat-Peyre and
V. Viguie Donzeau-Gouge, editors, Proceedings of the 26th IFIP WG 6.1 International
Conference on Formal Techniques for Networked and Distributed Systems FORTE'2006
(Paris, France). Lecture Notes in Computer Science volume 4229, Springer-Verlag,
2006. Available from http://cadp.inria.fr/publications/Lang-06.html
Milner. "Communication and Concurrency." Prentice-Hall, 1989.
Pace, Frederic Lang, and Radu Mateescu. "Calculating tau-confluence compositionally."
In W.A. Hunt Jr. and F. Somenzi, editors, 15th Computer-Aided Verification conference
(CAV 2003), Lecture Notes in Computer Science volume 2725, Springer-Verlag,
2003. Available from http://cadp.inria.fr/publications/Pace-Lang-Mateescu-03.html
Versions 1.*: Marius Bozga, Jean-Claude Fernandez, and Laurent Mounier.
Versions 2.*: Frederic Lang and Hubert Garavel.
of communicating automata (input)
- graph module for filename.exp
- FC2 network (output, with -network fc2 option)
- low level PEP Petri net (output, with -network pep option)
- NUPN Petri net (output, with -network nupn option)
- TINA Petri
net (output, with -network tina option)
- exploration module (archive,
- exploration module (source, input)
- exploration module
(object code, input)
- executable program (output)
- ``exp.open'' shell script
- ``exp.open'' static library
- ``exp.open'' graph module generator
- OPEN/CAESAR interfaces
- OPEN/CAESAR library
- exploration modules (source)
- exploration modules (archive)
- exploration modules (object code)
is available from the CADP Web page located at http://cadp.inria.fr
for installation are given in files $CADP/INSTALLATION_*.
and improvements to this software are reported and commented in file $CADP/HISTORY.
Please report bugs to email@example.com
Table of Contents