DES2AUT manual page
Table of Contents

Name

des2aut - compositional generation of a Labelled Transition System from a composition expression represented by a ".des" file.

Important Notice

The des2aut tool is now obsolete and no longer maintained. It has been replaced by the svl tool. It is advised to migrate to svl as des2aut might be removed from future versions of CADP.

Synopsis

des2aut -Rmin filename.des [options]

Description


Taking as input the composition expression contained in filename.des, des2aut performs a compositional generation to produce the Labelled Transition System filename.aut, wich represents the quotient with respect to relation R of the behaviour defined by this composition expression.

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.

Notes:

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

Syntax of the Composition Expressions

A .des file describes a composition expression. Its format is similar to the one used to describe networks of communicating LTSs (see the .exp format description in the 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> ']|?'

Note: <gate> is case-sensitive.

Informal Semantics of the Composition Expressions

The <behaviour> semantics is the following:

<lts> denotes the behaviour defined:

hide <gate-list> in <behaviour>
has the same semantics as the hiding operator in LOTOS. Note that the hide operator is distributed through <behaviour> (with respect to the distributivity property of this operator) before the compositional generation is performed.

<behaviour> <parallel-operator> <behaviour>
has the same semantics as the parallel composition in LOTOS.

<behaviour> <semi-composition-operator> <behaviour>
denotes the semi-composition of the left-hand side behaviour with respect to the right-hand side behaviour (the interface), using a synchronization set specified by a <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:

'-|[' <gate-list> ']|', when the interface is assumed to be correct,

'-|[' <gate-list> ']|?', when the interface is a "user-given" one, and its validity has to be checked.

Options


-output filedest[.aut]
Store the result LTS in the file filedest[.aut]. By default this LTS is stored in the file filename[.aut].

-script
Do not perform the compositional generation but produce only the corresponding shell-script in the file Script/filename.

-english
Print messages in English. By default messages are printed in French.

Exit Status

Exit status is 0 if everything is alright, 1 otherwise.

Diagnostics

When "user-given" interfaces are used their validity is checked and a result message is displayed.

Authors

Jean-Pierre Krimm, Laurent Mounier (VERIMAG)

Operands

filename.des
composition expression (input)

filename.aut
result LTS (output)

Script/filename
compositional generation shell-script (output)

See Also

aldebaran , caesar , caesar.open , exp.open , 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 Laurent.Mounier@imag.fr


Table of Contents