ALDEBARAN manual page
Table of Contents

Name

aldebaran - minimization and comparison of labelled transitions systems

Important Notice (july 2008)

aldebaran is a deprecated tool of CADP. Instead of aldebaran it is highly recommended to use the following tools directly:

As regards the status and history of aldebaran, the following information can be relevant:

Synopsis

aldebaran command [options]
aldebaran command [options] filename1
aldebaran command [options] filename1 filename2

where filename can be either a file in Aldebaran format (with suffix .aut), a file in BCG format (with suffix .bcg), or a file describing a system of communicating automata (with suffix .exp) (see the FORMATS section).

Description

aldebaran allows the minimization or comparison of Labelled Transitions Systems (LTS for short) with respect to various equivalence and preorder relations. Minimizations and comparisons are based either on the Paige & Tarjan algorithm, or the Fernandez & Mounier ``on the fly'' algorithm, the Minimal Model Generation algorithm, or (in version 6.6 only) algorithms using Binary Decision Diagrams (BDD for short).

aldebaran can be applied:

Commands

The followings commands are currently available:
-dead      
Print the set of deadlock states (sinks) for a LTS or a network of communicating LTSs.

-det      
Determinize a LTS and display the result as a new LTS.

-help      
Display the help file and stop.

-info      
Print various graph structure information for the LTS contained in filename1.(aut,bcg) or the network of communicating LTSs contained in filename1.exp. See also the bcg_info tool, which provides more complete structure information on a BCG graph.

-live      
Check whether there are livelock states (tau circuits) in the LTS or network of communicating LTSs stored in filename1.(aut,bcg,exp). If so, generate in file aldebaran.bcg a diagnostic, which is a subgraph of filename1 that exhibits both a livelock and a path to the livelock, starting from the initial state.

-old command
This command is no longer supported since version 7.4 of aldebaran.

-output filename[.aut|.bcg]
Specify the name (either filename.aut or filename.bcg) and the format (either ALDEBARAN format or BCG format) of the output file in which aldebaran will display its results (for those aldebaran commands that produce an LTS). By default, if no -output command is given, the result is printed on the standard output in ALDEBARAN format.

-path nb
Compute in a LTS a path from the initial state to the state nb. Display the result on the standard output as an LTS encoded in the SEQUENCE format (see the FORMAT section below).

-sort      
Sort the LTS. Sorting is done with the source state of transitions as primary key, and the label as secondary key. The LTS descriptor remains at the beginning of the file.

-version
Display the current version number of the software and stop.

The remaining commands have the following syntax:

[-<method>] -<relation><action>

where <method> is a three-character string among std, fly, or bdd, which is only meaningful with version 6.6 of aldebaran:

where <relation> is a one-character string, either b, d, i, o, p, or s:

and where <action> is a character string, either min, cla, equ or ord:

In version 6.6 of aldebaran, not all combinations of methods, relations and actions are implemented, but only the following:

-bmin:-stdor-bdd
-imin:-stdor-bdd
-pmin:-stdor-bdd
-omin:-std
-smin:-std
-bequ:-stdor-fly
-iequ:-stdor-fly
-oequ:-std
-sequ:-stdor-fly
-dequ:-fly
-pequ:-stdor-fly
-bcla:-std
-icla:-std
-ocla:-std
-pcla:-std
-scla:-std
-bord:-fly
-iord:-fly
-sord:-fly

Note: version 7.* of aldebaran calls version 6.6 to minimize LTSs modulo observational equivalence (-omin and -ocla options) and to compare LTSs modulo delay equivalence (-dequ option). In all other cases, options -fly, -std, and -bdd are meaningless and the method is selected automatically as follows:

Note: minimization modulo delay equivalence (-dmin and -dcla options) is not implemented, neither in version 6.6 nor in version 7.* of aldebaran (see table above).

Note: options -iord and -sord are identical, since both compute the same preorder relation.

Note (version 6.6 only): only ``on the fly'' and BDD methods can be applied to .exp files.

Note (version 6.6 only): if no method is specified, aldebaran will use the following rules to select a method by default:

Note (version 6.6 only): ``on the fly'' verification is often faster than standard verification and gives more accurate diagnostics. BDD methods often allow to deal with systems too large to be efficiently handled by other methods.

Note (version 6.6 only): when using option `-pequ -fly', one of filename1 or filename2 must be a completely generated LTS that does not contain any invisible (i.e., "tau") transition.

Note (version 6.6 only): version 6.6 and in particular the -bdd option have many bugs. It is recommended to use version 7.*.

Options

The following options are currently available:
-stat      
Print various statistics. -bddsize n This option was used to allocate n megabytes of memory for the Minimal Model Generation algorithm based on Binary Decision Diagrams. By default, n = 64. This option has been meaningless since version 7.* of aldebaran and is no longer supported since version 7.4 of aldebaran.

-hide filename
Use the hiding rules defined in filename to hide the labels contained in files filename1.(aut,bcg,exp) and possibly filename2.(aut,bcg,exp). See the caesar_hide_1 manual page for a detailed description of the appropriate format for filename. There is no required extension for filename; however, extensions ".hid" or ".hide" are recommended for using the SVL compiler and the EUCALYPTUS graphical user-interface. -labels n This option was used to fix the number n of maximum distinct labels of an LTS (or an LTS composition). By default, n = 4000. This option has been meaningless since version 7.* of aldebaran (because all the CADP tools but aldebaran 6.6 accept LTSs with any number of labels) and is no longer supported since version 7.4 of aldebaran.

-rename filename
Use the renaming rules defined in filename to rename the labels contained in files filename1.(aut,bcg,exp) and possibly filename2.(aut,bcg,exp). See the caesar_rename_1 manual page for a description of the appropriate format for filename. There is no required extension for filename; however, extensions ".ren" or ".rename" are recommended for using the SVL compiler and the EUCALYPTUS graphical user-interface.

Note: the full substitution possibilities described in the caesar_rename_1 manual page (especially the operators \(...\), \1, \2, etc.) may not be available in version 6.6 of aldebaran.

Note: in version 6.6, renaming patterns are applied before hiding patterns, whereas in version 7.*, renaming and hiding patterns are applied in the same order in which they occur on the command line.

Aldebaran Format for LTS

A .aut file describes a LTS in the Aldebaran format. Each state is represented by a natural number. The first line of filename.aut, called descriptor has the following structure:
des (<first-state>, <number-of-transitions>, <number-of-states>)
The first state is always equal to 0. Each remaining line of the file represents an edge; these lines have the following structure:

(<from-state>, <gate-name>, <to-state>)
where <from-state> and <to-state> are numbers and <gate-name> is a character string enclosed in double quotes (with up to 5000 characters).
Note: <gate-name> is case-sensitive.

BCG Format for LTS

A .bcg file describes a LTS in the BCG format. The BCG (Binary Coded Graph) format uses a binary representation of the LTS together with an ad-hoc compression algorihm, leading to very compact LTS files. See the bcg manual page.

Format for Networks of Communicating LTS

A .exp file describes a network of communicating LTSs. The syntax of .exp files is described in the exp.open manual page.

However, in version 6.6 of aldebaran, the syntax of .exp files is restricted to the language of the following context-free grammar. Terminals elements are enclosed in simple quotes, even when several characters long. 

     <axiom> ::= <behaviour-keyword> <behaviour>
              |  <behaviour>
     <behaviour-keyword> ::= 'behaviour'
                         |   'behavior'
     <behaviour> ::= <lts>
                  |  'hide' <gate-list> 'in' <behaviour>
                  |  <behaviour> <parallel-operator> <behaviour>
                  |  '(' <behaviour> ')'
     <lts> ::= '"'<any-string-without-double-quotes>'"'
            | <string-denoting-a-lts-filename>
     <gate-list> ::= <gate>
                   |  <gate> "," <gate-list>
     <gate> ::= <string-denoting-a-lotos-gate-identifier>
     <parallel-operator> ::= '||'
                          |  '|||'
                          |  '|[]|'
                          |  '|[' <gate-list> ']|'
where

The <behaviour> semantics is defined as follows:

<lts>      
is the name of a file containing an LTS. If a file named <lts> is present in the current directory, then this file will be read, possibly using the bcg_io tool to perform the appropriate conversions (file <lts> should have a format accepted as input of bcg_io . If no file named <lts> is found, then attempt will be made to read file <lts>.aut, and if this fails, a final attempt will be made to read <lts>.bcg.

hide <gate-list> in <behaviour>
has the same semantics as the hiding operator in LOTOS.

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

Note: <lts> is always case-sensitive.

Note: <gate> and <offer> are case-sensitive, unless <behaviour-keyword> is present, in which case they are case-unsensitive (same as in LOTOS).

Note: the hiding operator gives precedence to parallel operators (same as in LOTOS). For instance, the composition expression: 

    hide G in "f1.bcg" ||| "f2.bcg"
is parsed as: 
    hide G in ("f1.bcg" ||| "f2.bcg")

Note: parallel operators associate to the right (same as in LOTOS). For instance, the composition expression: 

    "f1.bcg" ||| "f2.bcg" |[G]| "f3.bcg"
is parsed as: 
    "f1.bcg" ||| ("f2.bcg" |[G]| "f3.bcg")

Note: as regards .exp files, version 6.6 of aldebaran accepts only a subset of the syntax described above: hiding is allowed only at top-level of the composition expression. Any .exp file containing the hide operator anywhere but at the root of the composition expression is syntactically rejected.

Sequence Format for Diagnostic Sequences

The SEQUENCE format is used (especially by version 6.6 of aldebaran for displaying diagnostic sequences in the case where two LTSs are not related (equ or ord commands). A detailed description of this format can be found in the manual page for exhibitor . The kind of SEQUENCE format (either "simple" or "full") produced by aldebaran depends on the verification algorithm chosen:

Note: in version 7.* of aldebaran, diagnostics are produced in the form of directed acyclic subgraphs containing all sequences which, executed simultaneously in the two LTSs, lead to non-equivalent states (see the bisimulator manual page for details). This often leads to much more compact diagnostics than those exhibited by version 6.6 of aldebaran.

Exit Status

When the source is erroneous, error messages are issued. Exit status is 0 if everything is alright, 1 otherwise.

Authors

Versions up to 6.6 of aldebaran have been developed by Jean-Claude Fernandez, Laurent Mounier, Alain Kerbrat, and Aline Senart (IMAG), with various bug fixes by Marc Herbert, Hubert Garavel, and Frederic Lang (INRIA Rhone-Alpes). Version 7.* of aldebaran was developed by Frederic Lang (INRIA Rhone-Alpes).

Operands

filename.aut
LTS in the Aldebaran format (input or output)

filename.bcg
LTS in the BCG format (input or output)

filename.exp
network of communicating LTSs (input)

filename.hide
list of labels to hide (input)

filename.rename
list of labels to rename (input)

Files

$CADP/LICENSE
license file

$CADP/com/aldebaran
shell-script (version 7.*)

aldebaran.bcg
diagnostic file

See Also

ALDEBARAN Reference Manual, bcg_info , bcg_io , bcg_labels , bcg_min , bcg_open , bisimulator , caesar_hide_1 , caesar_rename_1 , evaluator , exp.open , exhibitor , generator , reductor

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 any bug to cadp@inria.fr

Table of Contents