EXP.OPEN manual page
Table of Contents

Name

exp.open - OPEN/CAESAR connection for networks of communicating automata

Synopsis

exp.open [-branching | -deadpreserving | -ratebranching | -strong | -weaktrace] [-case] [-debug] [-lotos | -elotos | -ccs | -csp | -mcrl] [-hidden string] [-termination string] [-coaction string] [-history] [-info] [-inline] [-interface interface_directives] [-interfaceuser] [-labels] [-network format] [-nocheck] [-silent | -verbose] [-unparse] [-version] filename[.exp] [cc_options] user[.a|.c|.o] [user_options]

Description

Taking as input filename.exp (which describes a network of communicating automata in the EXP 2.0 language defined below) and an OPEN/CAESAR program user[.a|.c|.o], exp.open generates an OPEN/CAESAR graph module filename.c. This file is then compiled into filename.o and an executable program user resulting from the combination of filename.o and user[.a|.c|.o] is produced. Finally, user is executed.

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

Processing of the Exploration Module

The exploration module user[.a|.c|.o] is supposed to contain an OPEN/CAESAR application program, such as evaluator , generator , ocis ...

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 $CADP/bin.`arch`.

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.

Overview of the Exp 2.0 Language

EXP 2.0 is a conservative extension of EXP 1.0, the input language of the previous version 1.0 of exp.open. EXP 2.0 allows to model networks of communicating automata (also called behaviours in the sequel) using operators of several languages.

In addition to LOTOS parallel composition and hiding [ISO-89], already implemented in EXP 1.0, EXP 2.0 contains operators taken from E-LOTOS [ISO-01], CCS [Milner-89], CSP [Brookes-Hoare-Roscoe-84], and mCRL [Groote-Ponse-90], as well as parallel composition using synchronisation vectors, and generalized operators for label hiding, renaming, and cutting (also called restriction in CCS or encapsulation in mCRL). EXP2.0 also contains a priority operator that allows to define priorities between transitions.

Since these operators are taken from various languages that are not always compatible (for instance, the hidden event is written "i" in LOTOS and E-LOTOS, "t" in CCS and CSP, "tau" in mCRL), exp.open allows to customize the graph module with respect to a particular language (called the reference language).

The customization operates on the following parameters:

Default values are associated to each of these parameters, depending on the reference language selected. For backward compatibility reasons, there is no reference language selected by default. See Section LANGUAGE PARAMETERS for details.

Beware that the aldebaran and exp2fc2 tools only work with EXP 1.0 descriptions.

The publication [Lang-05] provides an overview of exp.open 2.0 and its input language.

Options

-branching
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.

-case
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.

-ccs    
Set CCS as the reference language. This is not a default option. See Section LANGUAGE PARAMETERS below for details.

-coaction string
Set string so as to prefix CCS co-action labels; string is named co-action prefix. See Section CCS PARALLEL COMPOSITION below for more information about the co-action prefix.

-csp    
Set CSP as the reference language. This is not a default option. See Section LANGUAGE PARAMETERS below for details.

-deadpreserving
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.

-debug
Undocumented option.

-elotos
Set E-LOTOS as the reference language. This is not a default option. See Section LANGUAGE PARAMETERS below for details.

-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 below for details.

Note that many CADP tools (such as for instance bcg_min , aldebaran , 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 (see Section SYNTAX OF EXP 2.0 below).

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.

-history
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 otherwise):

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 vector.

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.

-info
Print structural information about the LTSs referenced in filename.exp and stop. See bcg_info for more information.

-inline
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 article [Lang-06].

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, see Section EXP FILE INCLUSION above). 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.

-interfaceuser
Indicate 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 and svl for more information about using restriction interfaces. This is not a default option.

-labels
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 -interfaceuser option).

-lotos
Set LOTOS as the reference language. This is not a default option. See Section LANGUAGE PARAMETERS below for details.

-mcrl
Set mCRL as the reference language. This is not a default option. See Section LANGUAGE PARAMETERS below for details.

-network format
Generate a network equivalent to filename.exp in one of "pep", "tina", or "fc2" format and stop:

If format is "pep", exp.open generates a file named filename.ll_net, containing a Petri net in the low-level PEP file format [Best-Grahlmann-98];

If format is "tina", exp.open generates a file named filename.tpn, containing a Petri net in the ``tpn'' format of the TINA toolbox [Berthomieu-Ribet-Vernadat-04];

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].

The bcg_io 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 below) because this is required by bcg_io and fc2link.

This 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.

-nocheck
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 option.

-ratebranching
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 bcg_min manual page for details about stochastic transitions), thus taking an account of the maximal progress of hidden actions.

-silent
Execute silently. Opposite of -verbose. Default option is -verbose.

-strong
Do not perform partial order reduction of the graph. This is a default option.

-termination string
Set string as denoting the gate used to express behaviour termination. The default value depends on the reference language, see Section LANGUAGE PARAMETERS below for details.

-unparse
Use the "-bcg -unparse" options of bcg_io while converting LTSs in AUT, FC2, or SEQ formats into BCG. See the bcg_io manual page for details about these options.

-verbose
Report activities and progress, including errors, to the user's screen. Opposite of -silent. Default option is -verbose.

-version
Display the version number and stop.

-weaktrace
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.

cc_options
if any, are passed to the C compiler.

user_options
if any, are passed to user.

Syntax of Exp 2.0

The syntax of EXP 2.0 is presented using a grammar in the Extended Backus-Naur Form (EBNF):

The EXP 2.0 grammar is presented in several parts, corresponding to the different languages supported. We write "B ::= ... | expression" to express that the definition of B is extended with expression. The entry point of the grammar is the non-terminal symbol AXIOM.

The following productions are common to all languages. IDF stands for any sequence of letters, digits, and underscores ("_"), which begins with a letter and does not end with an underscore. LTS stands for files containing an automaton, FILE for other files, G for gates, GL for gate lists, L for labels, and LL for label lists.

Comments of the form 

    (* <any text on one or several lines> *)
and 
    -- <any text on one line>
are allowed in EXP 2.0 behaviours. 
LTS ::= "<filename>"
     | IDF                 (* automaton without extension *)
     | "<filename>.bcg"
     | IDF.bcg             (* automaton in BCG format *)
     | "<filename>.aut"
     | IDF.aut             (* automaton in AUT format *)
     | "<filename>.seq"
     | IDF.seq             (* automaton in SEQ format *)
     | "<filename>.fc2
     | IDF.fc2             (* automaton in FC2 format *)
     | "<filename>.exp"    (* include file in EXP format *)
FILE ::= "<filename>"
      | IDF                (* file without extension *)
      | "<filename>(.hid|.hide)"
      | IDF(.hid|.hide)    (* hide file *)
      | "<filename>(.ren|.rename)"
      | IDF(.ren|.rename)  (* rename file *)
      | "<filename>.cut"
      | IDF.cut            (* cut file *)
G ::= IDF                  (* gate *)
   |  "<string denoting a gate>"
GL ::= [G (, G)*]          (* gate list *)
L ::= G                    (* label *)
   |  "<gate with offers>"
   |  "<regular expression denoting a gate>"
   |  "<regular expression denoting a gate with offers>" 
LL ::= [L (, L)*]          (* label list *)

Note that L can be a gate, or a gate followed by experiment offers, or a regular expression denoting a gate possibly followed by experiment offers. (See the definition of regular expressions in the regexp man page.) The gate of a label L is the sub-string starting at the beginning of L and ending at the first character !, ?, (, space, or tabulation, if any, or at the end of L otherwise.

For instance, "G", "G.*", "G !1", "G(1)", "G.* !.*" are labels, among which "G" is a gate, "G.*" is a regular expression denoting a gate or a gate with offers, "G !1" is a gate with offers, and "G.* !.*" is a regular expression denoting a gate with offers (following LOTOS syntax). Note that the syntax of offers is not restricted to LOTOS: "G(1, 2)" also denotes a gate with offers.

Double quotes around a label can be omitted if and only if the label is a gate satisfying the syntax of IDF, but they are mandatory to avoid syntactic ambiguities when a gate has the same name as a reserved EXP keyword (e.g. "cut", "all", etc.) or when a label contains special characters.

Note: all escape character sequences defined in the specification of ANSI C character constants, except octal numbers, hexadecimal numbers, and '\n', are allowed in labels and filenames enclosed in double quotes. These escape character sequences are replaced by a single character accordingly. Every '\' character that does not belong to an ANSI C escape character sequence is kept unchanged. For instance, '\"' and '\\' are replaced respectively by '"' and '\', whereas '\p' and '\(' are kept unchanged.

Lotos Operators


AXIOM ::= [[lotos] (behaviour | behavior)] B
B ::= LTS
   |  hide GL in B
   |  B "||" B
   |  B "|||" B
   |  B "|[" GL "]|" B
   |  (B)

Note that the LOTOS syntax corresponds exactly to EXP 1.0, except the "lotos" keyword, which was absent in EXP 1.0. In EXP 2.0, LOTOS operators are subsumed by E-LOTOS operators, but they are kept for backward compatibility with EXP 1.0.

E-lotos Operators


AXIOM ::= ...
       |  [[elotos] (behaviour | behavior)] B
B ::= ...
   |  [gate | total | partial] hide 
      ([all but] LL | using FILE) in B end hide
   |  [gate | total | single | multiple] rename
      (L -> L (, L -> L)* | using FILE) in B 
      end rename
   | [gate | label] par (all | S) in
     B ("||" B)+ end par
   | [gate | label] par (all | S) in
     LL -> B ("||" LL -> B)+ end par
S ::= [L [# N] (, L [# N])*]
N ::= <positive integer>

Ccs Operators


AXIOM ::= ...
       |  [[ccs] (behaviour | behavior)] B
B ::= ...
   |  B "|" B
   |  B \ L
   |  B \ "{" LL "}"
   |  B "[" L / L (, L / L)* "]"

Csp Operators


AXIOM ::= ...
       |  [[csp] (behaviour | behavior)] B
B ::= ...
   |  B "|||" B
   |  B "[|" "{" GL "}" "|]" B
   |  B "[" "{" GL "}" "||" "{" GL "}" "]" B
   |  B \ L
   |  B \ "{" LL "}"
   |  B "[[" L <- L (, L <- L)* "]]"

Mcrl Operators


AXIOM ::= ...
       |  [[mcrl] (behaviour | behavior)] 
          [comm C (, C)* end comm] B
C ::= G "|" G "=" G
B ::= ...
   |  B "||" B

The mCRL operators "hide", "rename", and "encaps" are subsumed by the operators "hide", "rename", and "cut" presented in Sections "E-LOTOS OPERATORS" above and "OTHER OPERATORS" below.

Other Operators


B ::= ...
   |  [gate | total | partial] cut 
      ([all but] LL | using FILE) in B end cut
   |  [gate | total | partial] prio
      ([all but] LL (> [all but] LL)+)+
      in B end prio
   |  [gate | label] par
      SV (, SV)* in B ("||" B)* end par
R ::= 
SV ::= (L |  _) ("*" (L |  _))* -> L

Syntax Conventions

EXP 2.0 satisfies the following precedence and associativity rules:

The syntax of EXP 2.0 is the union of all EBNF productions presented above, with the following exceptions:

Semantics of Exp 2.0

This section describes the semantics of all EXP 2.0 constructs.

Labelled Transition Systems

LTS may be the name of a file containing an automaton in one of the AUT (extension .aut), BCG (extension .bcg), FC2 (extension .fc2), or SEQ (extension .seq) file formats.

All automaton files must have a known extension. However, the extension may be omitted in the behaviour description if the automaton is in the BCG or in the AUT format. If LTS does not exist in the current directory, exp.open will first attempt to open LTS.bcg. If LTS.bcg does not exist in the current directory, exp.open will then attempt to open LTS.aut.

Use of the BCG format is recommended since exp.open will automatically convert other formats to BCG using the bcg_io tool.

Exp File Inclusion

LTS may also be the name of an EXP file (extension .exp) within double quotes. In this case, the contents of this EXP file is simply copied inside the current EXP expression. This allows to split large expressions into a hierarchy of EXP files.

Example: The expression 

   "a.exp" || "b.bcg"
where file "a.exp" contains the expression 
   hide A in "a.bcg"
is equivalent to 
   hide A in "a.bcg" || "b.bcg"
Note that this is parsed as 
   hide A in ("a.bcg" || "b.bcg")
hence parentheses may be required to avoid lexical scoping issues.

Generalized Hiding


  [gate | total | partial] hide [all but] LL in B end hide
| [gate | total | partial] hide using FILE in B end hide
will hide the labels found in B using the given hiding rules. These rules can be specified either as a list of labels (first form), or using an external file FILE (second form).

In the first case, exp.open builds a temporary file, filled with the given labels. In the second case, the hide file must be provided by the user. No particular extension is required, but the filename must be written between double quotes if it does not have the form IDF, IDF.hide, or IDF.hid. See the caesar_hide_1 man page for a definition of the hide file format.

The "all but" keywords modify the semantics of the hiding rules: all the labels, except the labels specified in the list of labels, are hidden.

The keywords "total", "partial", and "gate" modify the matching mode, that is the way the hiding rules are interpreted. See the caesar_hide_1 man page. See also Section SYNTAX OF EXP 2.0 above, which explains how the gate of a label is recognized. If no matching mode is specified, then the default is "gate", which implements the LOTOS hiding operator extended with regular expressions denoting gates.

For every hiding with "gate" matching, exp.open checks whether the gates to be hidden have an appropriate syntax and issues a warning if they appear to contain experiment offers (which is a common mistake for novice users). For instance, 

        hide "G !1"
will trigger a warning message because of the occurrence of "!1".

Examples: 

        total hide "G"
hides every label equal to "G", 
        gate hide "G"
hides every label whose gate is G, e.g., "G !1", "G !2", 
        gate hide ".*G.*"
hides every label whose gate contains the character G and 
        partial hide "G"
hides every label whose gate or offers contain the character G.

See the caesar_hide_1 man page for more information on matching mode semantics. regexp man page for information about regular expression syntax.

The semantics of LOTOS "hide" is compatible with that of E-LOTOS, i.e., 

        hide GL in B
is equivalent to 
        gate hide GL in B end hide

Generalized Renaming


  [gate | total | single | multiple] rename 
        L -> L (, L -> L)* in B end rename
| [gate | total | single | multiple] rename 
        using FILE in B end rename
will rename the labels of B using the given renaming rules. These rules can be specified either as a list of items of the form L -> L (first form), or using an external file FILE (second form).

In the first case exp.open builds a temporary file, filled with the given substitution rules. In the second case exp.open uses the given renaming file. No particular extension is required, but the filename must be written between double quotes if it does not have the form IDF, IDF.rename, or IDF.ren. See the caesar_rename_1 man page for a definition of the hide file format.

See also Section SYNTAX OF EXP 2.0 above, which explains how the gate of a label is recognized. The keywords "total", "single", "multiple", and "gate" modify the way the left-hand sides of the renaming rules are interpreted, see the caesar_rename_1 man page. If no matching mode is specified, then the default is "gate".

For every renaming with "gate" matching, exp.open checks whether the gates to be renamed have an appropriate syntax and issues a warning if they appear to contain experiment offers (which is a common mistake for novice users). For instance, 

        rename "G !1" -> "G !2"
will trigger a warning message because of the occurrence of "!1" in the left-hand side. Note however that 
        rename "G" -> "G !1"
is correct.

Examples: 

        total rename "G" -> "H"
renames to "H" every label equal to "G", 
        gate rename "G" -> "H"
renames to "H" every gate equal to "G", e.g., "G !1" is renamed to "H !1", 
        gate rename ".*G.*" -> "H"
renames to "H" every gate that contains a G character, 
        single rename "G" -> "H"
replaces the first occurrence of "G" by "H" in every label whose gate or offers contain a G character, 
        multiple rename "G" -> "H"
replaces every occurrence of "G" by "H" in every label whose gate or offers contain a G character, and 
        total rename "\([a-zA-Z0-9]*\) \(!.*\)" -> "\1 !1 \2"
inserts "!1" between every gate (sequence of letters and digits) and its offers (prefixed with !).

See the caesar_rename_1 man page for more information on matching mode semantics. See also the regexp man page for more information on regular expressions.

Generalized Cut


  [gate | total | partial] cut [all but] LL in B end cut
| [gate | total | partial] cut using FILE in B end cut
is a generalization of mCRL encapsulation, on the same principles as the generalized "hide" operator. Instead of being converted into silent transitions as does the "hide" operator, transitions whose label matches the given regular expressions are simply cut off.

Cut files have the following syntax: 

AXIOM ::= <blanks> cut <blanks> \n LABELS
       |  <blanks> cut all but <blanks> \n LABELS
LABELS ::= (<blanks> L <blanks> \n)*
where L is a label, and <blanks> is any sequence of spaces, tabulations, carriage returns, newlines, vertical tabulation, or form feeds; these characters are those recognized by the POSIX function isspace(); they are always skipped and ignored.

Generalized Priority


  [gate | total | partial] prio 
      ([all but] LL (> [all but] LL)+)+
  in B end prio
sets priorities between the transitions of B. In each state of B, a transition may be executed only if all transitions of higher priority are not ready for execution.

Priorities between transitions (or equivalently, between labels) are defined by a set of priority rules X1 > ... Xn, where each Xi has the form [all but] LLi and LL1, ..., LLn are lists of regular expressions denoting gates or labels. The "all but" keywords that may precede some LLi means all gates or labels but those matching LLi.

Such priority rules define a transitive relation ">>" on labels as follows:

L >> L' means that any transition labeled L has priority over any transition labeled L' or, equivalently, any transition labeled L' yields priority to any transition labeled L.

The relation ">>" must be a strict partial order: B must not contain any label L such that L >> L. If ">>" is not a strict partial order, exp.open will issue an error message and exit.

Beware that the rules X > X' and X' > X'' (which are equivalent to X > X' > X'') imply X > X'' if and only if some label of B matches X'. Therefore, to avoid tricky errors, exp.open checks that every individual regular expression L in LL1, ..., LLn matches some label of B. If not, then exp.open will issue a warning.

The optional "gate", "total", and "partial" keywords define the matching mode, in the same way as for the "hide" and "cut" operators. The matching mode by default is "gate".

Examples:

Note: Strong bisimulation is a congruence for all exp.open operators, including "prio". However, branching, observational, and safety equivalences are congruences for all exp.open hiding, cutting, renaming, and parallel composition operators, but not for "prio". It should also be noted that tau*.a equivalence is not a congruence for parallel composition.

Generalized Parallel


  [gate | label] par (all | S) in B ("||" B)+ end par
| [gate | label] par (all | S) in 
      LL -> B ("||" LL -> B)+ end par
are extensions of the E-LOTOS generalized parallel operators presented in [Garavel-Sighireanu-99]. They denote the concurrent execution of behaviours following synchronisation rules expressed using the construct "all" or the synchronisation list "S", and the label lists preceding the "->" symbols, called synchronisation interfaces.

The first form is equivalent to the second form in which all synchronisation interfaces are empty.

The semantics of synchronisation rules is as follows:

Transition synchronisation is a generalization of LOTOS rendezvous: the transition resulting from the synchronisation of transitions labelled with L is also labelled with L. Transitions whose label does not match any synchronisation rule perform asynchronously.

Note that behaviours always synchronize on labels whose gate is the termination gate and never synchronize on hidden events. Note also that "rate" is a keyword used for stochastic transitions (see the bcg_min manual page for details about stochastic transitions) and therefore "rate" should not be used as a gate name. Behaviours never synchronize on stochastic transitions.

Before generating the graph module, exp.open checks that generalized parallel operators are well-formed, i.e.:

These checks can be discarded by using the -nocheck option. This is not recommended because syntactic errors lead to unpredictable behaviours.

Example: 

gate par G#2 in
   G4, G2 -> "f1.bcg"
|| G1, G3 -> "f2.bcg"
|| G2, G4 -> "f3.bcg"
|| G3, G1 -> "f4.bcg"
end par

represents an automaton such that:

Parallel with Synchronisation Vectors


  [gate | label] par SV (, SV)* in B ("||" B)* end par
is parallel composition with synchronisation vectors. It denotes the concurrent execution of behaviours following synchronisation rules, expressed using vectors of gates (in "gate" mode) or labels (in "label" mode).

A synchronisation vector SV has the form "E1 * ... * En -> L" where each Ei (i = 1..n) is either a visible gate without offers (in "gate" mode), a visible label, i.e., visible gate with offers (in "label" mode), or the special symbol "_" (in both modes). Note that gates and labels must not be defined using regular expressions. If it is not specified, the mode by default is "gate". See Section SYNTAX OF EXP 2.0 above, which explains how the gate of a label is recognized.

The left-hand side (left of the arrow) of each synchronisation vector must have as many gates (or labels) and "_" symbols as there are behaviours B in parallel. A gate (or label) G as nth component of a vector left-hand side means that the nth behaviour in the parallel composition can perform a transition whose gate is G only if all behaviours can perform simultaneously as specified by the same vector, possibly on different gates, but with same offers (in "gate" mode). "_" means that no transition is required for the corresponding behaviour. The resulting transition is labelled with the right-hand side of the vector (in "label" mode) or with the right-hand side of the vector, followed by the offers, if any (in "gate" mode). The hidden string is forbidden in the left-hand side of a synchronisation vector.

Transitions that do not fit any vector are blocked, except hidden transitions, which always perform asynchronously. In particular, if one wants to let visible transitions perform asynchronously, it is necessary to define vectors whose left-hand side contain only "_" but one visible gate.

Example: 

gate par 
  G1 * _ * G3 -> G13,
  G1 * G2 * _ -> G12,
  G1 * _ * _ -> G1
  H * _ * _ -> H
in
  "f1.bcg" || "f2.bcg" || "f3.bcg"
end par

represents the automaton defined as follows:

  1. if "f1.bcg" can perform a transition whose gate is G1, possibly followed with experiment offers (written O1...On), then a transition labelled "G1 O1...On" is created in the resulting automaton due to the vector "G1 * _ * _ -> G1"

  2. if, additionally to 1), "f3.bcg" can perform a transition labelled "G3 O1...On", then a transition labelled "G13 O1...On" is created in the resulting automaton due to the vector "G1 * _ * G3 -> G13"

  3. if, additionally to 1), "f2.bcg" can perform a transition labelled "G2 O1...On", then a transition labelled "G12 O1...On" is created in the resulting automaton due to the vector "G1 * G2 * _ -> G12"

  4. if "f1.bcg" can perform a transition whose gate is H, then the same transition is created in the resulting automaton, due to the vector "H * _ * _ -> H"

  5. all other transitions of "f1.bcg", "f2.bcg" and "f3.bcg" do not create any transition in the resulting automaton.

Lotos Parallel


  B "||" B
| B "|||" B
| B "|[" GL "]|" B
have the same semantics as, respectively: 
gate par all in B "||" B end par

gate par in B "||" B end par

gate par GL in B "||" B end par
Note that in mCRL mode, "||" has a different semantics (see MCRL PARALLEL). Note also that the "|||" operator of CSP has the same semantics as in LOTOS.

Ccs Parallel


  B "|" B
is the parallel composition operator of CCS.

Transitions of both behaviours may either perform asynchronously, or may synchronize, resulting in a hidden event.

Synchronisation is possible only if the corresponding transition labels are co-actions, i.e., they have the same gate and offers, but one of the gates is prefixed with the co-action prefix. The co-action prefix by default is "'" but can be modified using the -coaction option. Note that (1) the co-action prefix should not contain !, ?, (, space, and tabulation characters, which are used to delimit a gate from its offer, and (2) there should not be any space or tabulation between the co-action prefix and the gate identifier (see Section SYNTAX OF EXP 2.0 above, which explains how the gate of a label is recognized).

For instance, transitions labelled "G" and "'G" may synchronize, as well as transitions labelled "G O" and "'G O". In both cases, the resulting label after synchronisation is the hidden label.

Note that hidden transitions perform asynchronously and that there is no termination label in CCS.

Csp Parallel


  B "|||" B
| B "[|" "{" GL "}" "|]" B
| B "[" "{" GL "}" "||" "{" GL "}" "]" B
denote parallel composition in CSP.

Mcrl Parallel


  B "||" B
denotes parallel composition in mCRL.

In "B1 || B2", transitions may either perform asynchronously, or they may synchronize following communication rules, that must be defined in the preamble of the EXP file ("comm" keyword). A communication rule has the form "G1 | G2 = G3", where G1, G2, and G3 are gates. Communication rules are commutative, i.e., there is no difference between "G1 | G2 = G3" and "G2 | G1 = G3". Such a rule means that if an operand (B1 or B2) may perform a transition whose gate is G1 and the other operand may perform a transition whose gate is G2, and both transitions carry the same experiment offers O, then a synchronisation is possible and results in a transition labelled "G3 O". See Section SYNTAX OF EXP 2.0 above, which explains how the gate of a label is recognized.

Note that hidden transitions must perform asynchronously, and that there must be at most one communication rule for each pair of gates occurring in the left-hand side of the "=" symbol. For instance, the following is not allowed: 

comm G1 | G2 = G3, G2 | G1 = G4 end comm

Note that the reference language must be mCRL in order for the "||" operator to have mCRL semantics instead of LOTOS semantics. If the reference language is different from mCRL, then any "comm" definition is useless and irrelevant.

Ccs Restriction


  B \ "{" L (, L)* "}"
| B \ L
denotes the CCS restriction operator, except when the language option is set to CSP (see Section CSP HIDING below). In the first form, the behaviour B is restricted with respect to several labels, whereas in the second form it is restricted with respect to a single label.

CCS restriction is similar to cut (in gate matching mode), except that co-action labels are also affected by the restriction whenever the corresponding action label is affected.

For instance, in "B \ G", transitions of B labelled "G", "'G" (where "'" stands for the co-action prefix), "G O" (where O denotes any communication offer), and "'G O" are cut off. See Section SYNTAX OF EXP 2.0 above, which explains how the gate of a label is recognized.

Note that labels in the restriction set can be regular expressions denoting gates, but should not have offers and should not start with the co-action prefix.

Csp Hiding


  B \ "{" L (, L)* "}"
| B \ L
denotes the CSP hiding operator when the language option is set to CSP (otherwise it denotes the CCS restriction operator, see Section CCS RESTRICTION above). Both forms are equivalent to 
gate hide L (, L)* in B end hide
gate hide L in B end hide
respectively.

Ccs Relabeling


  B "[" L / L (, L / L)* "]"
denotes the CCS relabeling operator. It is similar to the renaming operator (in gate matching mode) except that the co-action prefix is preserved by renaming.

For instance, in "B [G1/G2]", the labels "G2", "'G2" (where "'" stands for the co-action prefix), "G2 O" (where O denotes any communication offer), and "'G2 O" are renamed respectively into "G1", "'G1", "G1 O", and "'G1 O". See Section SYNTAX OF EXP 2.0 above, which explains how the gate of a label is recognized.

Note that labels can be regular expressions denoting gates, but should not have offers and should not start with the co-action prefix.

Csp Relabeling


  B "[[" L <- L (, L <- L)* "]]"
denotes the CSP relabeling operator.

The behaviour 

B [[ G1 <- G2, ..., G2n+1 <- G2n+2 ]]
is equivalent to 
gate rename G1 -> G2, ..., G2n+1 -> G2n+2 in B

(Note the opposite direction of the arrows.)

Note that, as a consequence, labels can be regular expressions denoting gates, but should not have offers.

Language Parameters

There are two means to select a reference language:

If the EXP file header and the command line option specify different reference languages, then a warning is issued. It is not allowed to specify more than one language option on the command line.

The following table summarizes the default parameter values according to reference languages. Note that these values (in particular lines labelled none and LOTOS) are compatible with exp.open version 1.0. 

+----------+--------+--------+-------------+------+-------+
| language | hidden | termin.|    case     | sem. | sem.  |
|          | event  |  gate  | sensitivity | of \ | of || |
+----------+--------+--------+-------------+------+-------+
| none     |   "i"  | "exit" |  sensitive  | CCS  | LOTOS |
+----------+--------+--------+-------------+------+-------+
| LOTOS    |   "i"  | "exit" | insensitive | CCS  | LOTOS |
+----------+--------+--------+-------------+------+-------+
| E-LOTOS* |   "i"  | "exit" |  sensitive  | CCS  | LOTOS |
+----------+--------+--------+-------------+------+-------+
| CCS      |   "t"  |  N/A   | insensitive | CCS  | LOTOS |
+----------+--------+--------+-------------+------+-------+
| CSP      |   "t"  | "delta"| insensitive | CSP  | LOTOS | 
+----------+--------+--------+-------------+------+-------+
| mCRL     |  "tau" |  N/A   |  sensitive  | CCS  | mCRL  |
+----------+--------+--------+-------------+------+-------+
where N/A stands for Not Applicable.

* The parameters associated to E-LOTOS are subject to modifications in the future, depending on implementation choices still to be made.

Note that the hidden string (written either "i", "t", "tau", or anything else) should not be followed by communication offers, whereas the termination string may.

Exit Status

Exit status is 0 if everything is all right, > 0 otherwise.

References

[Berthomieu-Ribet-Vernadat-04]
B. 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-Grahlmann-98]
Eike Best and Bernd Grahlmann. "PEP Documentation and User Guide." http://parsys.informatik.uni-oldenburg.de/~pep/paper.html. 1998."

[Bouali-Ressouche-Roy-deSimone-96]
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, 1996.

[Brookes-Hoare-Roscoe-84]
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.

[Garavel-Sighireanu-99]
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.

[Groote-Ponse-90]
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.

[ISO-89]
ISO/IEC. "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-01]
ISO/IEC. "Enhancements to LOTOS (E-LOTOS)." International Organization for Standardization --- Information Technology. International Standard number 15437:2001. Geneva, September 2001.

[Lang-05]
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.

[Lang-06]
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.

[Milner-89]
Robin Milner. "Communication and Concurrency." Prentice-Hall, 1989.

[Pace-Lang-Mateescu-03]
Gordon 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.

Authors

Versions 1.*: Marius Bozga, Jean-Claude Fernandez, and Laurent Mounier.

Versions 2.*: Frederic Lang and Hubert Garavel.

Operands

filename.exp
network of communicating automata (input)

filename.c
graph module for filename.exp (output)

filename.fc2
FC2 network (output, with -network fc2 option)

filename.ll_net
low level PEP Petri net (output, with -network pep option)

filename.tpn
TINA Petri net (output, with -network tina option)

user.a      
exploration module (archive, input)

user.c      
exploration module (source, input)

user.o      
exploration module (object code, input)

user      
executable program (output)

Files

$CADP/com/exp.open
``exp.open'' shell script

$CADP/bin.`arch`/libexp_open.a
``exp.open'' static library

$CADP/bin.`arch`/exp2c
``exp.open'' graph module generator

$CADP/incl/caesar_*.h
OPEN/CAESAR interfaces

$CADP/bin.`arch`/libcaesar.a
OPEN/CAESAR library

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

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

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

See Also

aldebaran , bcg_io , caesar_hide_1 , caesar_rename_1 , caesar.open , exp2fc2 , projector , regexp , svl

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.

Bugs

Please report bugs to cadp@inria.fr

Table of Contents