svl tool. It is advised to migrate to svl as des2aut might be removed from future versions of CADP.
Composition expression are built from elementary Labelled Transition Systems (provided either in the ".aut" format, or as networks of communicating LTSs in the ".exp", or by LOTOS programs), that are combined together using the hiding operator and the parallel composition operator of the LOTOS language. Moreover, semi-composition operations can be included to restrict the behaviour of a given sub-expression with respect to its environment (i.e., a composition expression - the interface - and a synchronisation set).
Interfaces can be either ``exact'' interfaces (i.e., parts of the syntactic environment of the sub-expression to be restricted), or ``user-given'' interfaces (i.e., composition expression that are supposed to correctly approximate this environment). In this later case, des2aut generates validation predicates (using the -interfaceuser option of projector and exp.open in order to check the correctness of the result.
The behavioural relation R can be any character `b', `i', `o' or `s' as defined in the aldebaran manual page.
To perform the compositional generation des2aut makes multiple calls to the components of CADP (aldebaran , caesar , exp.open , caesar.open , etc.) through a Unix shell-script, and it generates several intermediate files. All these files are stored in a temporary directory (named Script), which is created if necessary. This directory can therefore be removed after an execution of des2aut.
Full descriptions of the compositional generation process and the des2aut tool are given in $CADP/doc/*/Krimm-Mounier-97.*aldebaran manual page), with the two following extensions:
The grammar of the .des format is the following:
<axiom> ::= <behaviour> <behaviour> ::= <lts> | 'hide' <gate-list> 'in' <behaviour> | <behaviour> <parallel-operator> <behaviour> | <behaviour> <semi-composition-operator> <behaviour> | '('<behaviour>')' <lts> ::= 'Proc' '(' <lotos-filename> ',' <process-call> ')' | <filename> <gate-list> ::= <gate> | <gate> ',' <gate-list> <gate> ::= <any-string-denoting-a-lotos-gate-identifier> <parallel-operator> ::= '||' | '|||' | '||' | '|[' <gate-list> ']|' <semi-composition-operator> ::= '-|[' <gate-list> ']|' | '-|[' <gate-list> ']|?'
<gate> is case-sensitive.
<behaviour>semantics is the following:
<lts> denotes the behaviour defined:
<process-call>of the LOTOS program contained in
<process-call>can be either the empty string '' (and then the whole LOTOS program is considered), or any process instantiation of the form '
P [G1, ..., Gn]' (and then only process
Pis considered, according to the -root option of the caesar tool).
hide <gate-list> in <behaviour>
hideoperator is distributed through
<behaviour>(with respect to the distributivity property of this operator) before the compositional generation is performed.
<behaviour> <parallel-operator> <behaviour>
<behaviour> <semi-composition-operator> <behaviour>
<gate-list>. The interface LTS is previously reduced modulo safety equivalence hiding all labels that not belong to
<gate-list>. Two semi-composition operators are proposed:
]|', when the interface is assumed to
]|?', when the interface is a "user-given" one, and its validity
has to be checked.
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.Laurent.Mounier@imag.fr