Table of Contents
aldebaran - minimization and comparison of labelled transitions
As of July 2008, aldebaran
is a deprecated tool
of CADP. Instead of aldebaran
it is highly recommended to invoke the following
tools of CADP (either directly or indirectly using SVL):
1.0 (January 1990) to version 6.6 (October 2005), aldebaran has been a binary
executable (located in "$CADP/bin.`arch`/aldebaran" and later in "$CADP/bin.`arch`/aldebaran.old").
It performed minimizations and comparisons of labelled transition systems,
using the Paige & Tarjan algorithm, the Fernandez & Mounier on-the-fly algorithm,
the Minimal Model Generation algorithm, and algorithms based on Binary
Decision Diagrams (BDD for short). Because aldebaran was no longer maintained
by its authors and was known to contain bugs (including false verdicts
about equivalence or preorder comparisons), it was marked as deprecated
in CADP 2006. In July 2008, it was eventually removed from CADP because
it would no longer compile using gcc/g++ 3.4.* and no one volunteered to
port it to 64-bit platforms.
Version 7.* of aldebaran is a shell-script (located
in file "$CADP/com/aldebaran") that has been introduced in October 2005.
This shell-script invokes the CADP tools mentioned above and does not rely
on aldebaran 6.6. It provides extensive backward compatibility with previous
versions of aldebaran by supporting all their commands/options but -dequ.
It also removes many limitations that existed in the previous versions
] 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
allows the minimization or comparison
of Labelled Transitions Systems (LTS for short) with respect to various
equivalence and preorder relations. It can be applied:
- either to completely
generated LTSs, which are usually contained in files with the .aut or .bcg
suffix. See the aut
manual pages for a description
of the .aut and .bcg formats. aldebaran also accepts other LTSs formats (such
as .fc2 or .seq files): in such case, the bcg_io tool is used to perform
silently the translation of these other formats into the BCG format.
to networks of communicating LTSs, which are contained in files with the
.exp suffix. See the exp
manual page for a description of this format.
The followings command
s are currently available:
- Print the
set of deadlock states (sinks) for a LTS or a network of communicating
- Determinize a LTS and display the result as a new LTS.
the help file and stop.
- 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
provides more complete structure information on a BCG graph.
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
- -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 seq
(see the DIAGNOSTICS section below).
- 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.
the current version number of the software and stop.
The remaining commands
have the following syntax:
where <relation> is a one-character string, either b, i, o, p, or s:
- `b' :
use the strong bisimulation equivalence [Park-81] or the corresponding preorder
- `i' : use the tau*.a bisimulation [Fernandez-Mounier-90] or the corresponding
preorder (tau is written i in LOTOS)
- `o' : use the observational relation
- `p' : use the branching bisimulation [R.J. Van Glabbeek and W.P. Weijland]
- `s' : use the safety relation [Rodriguez-88] [Bouajjani-Fernandez-Graf-Rodriguez-Sifakis-91]
or the corresponding preorder
and where <action> is a character string, either
min, cla, equ or ord:
- `min' : minimize the LTS contained in filename1.(aut,bcg),
or the network of communicating LTSs represented by filename1.exp, with
respect to <relation> and display the minimized LTS
- `cla' : same as above,
but display the equivalence classes on the standard output (instead of
the reduced LTS)
- `equ' : compare both LTSs contained in filename1.(aut,bcg)
and filename2.(aut,bcg), or the network of communicating LTSs filename1.exp
to the LTS filename2.(aut,bcg), or the network of communicating LTSs filename2.exp
to LTS filename1.(aut,bcg), with respect to <relation>, using algorithm. The
result can be either
TRUE (both LTSs are equivalent) or
FALSE; in the latter
case, aldebaran issues a diagnostic consisting either of a set of discriminating
sequences displayed on standard output (see the DIAGNOSTICS section below),
or of an acyclic BCG graph stored in file aldebaran.bcg (see the -diag options
for details about diagnostics
in the BCG format).
- `ord' : same as equ, but use a preorder relation instead
of the equivalence relation
In version 7.* of aldebaran, the method is selected
automatically as follows:
- As regards tau*.a and safety minimizations (-imin,
-icla, -pmin, and -pcla options), the LTS is first pre-reduced on the fly using
reductor, then minimized modulo strong bisimulation following the standard
method using bcg_min.
- As regards strong and branching minimizations (-bmin,
-bcla, -pmin, -pcla), the LTS is first generated (if needed) using generator
and then minimized following the standard method using bcg_min.
- As regards
comparisons modulo strong, branching, observational, tau*.a, and safety
equivalences (-bequ, -bord, -pequ, -pord, -oequ, -oord, -iequ, -iord, -sequ, and
-sord options), they are performed using bcg_cmp or, if not possible, using
Note: options -iord and -sord are identical, since both compute
the same preorder relation.
The following options
are currently available:
- Print various statistics.
- -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
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
- -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
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
Renaming and hiding patterns are applied in the order in
which they occur on the command line.
to explain why two LTSs are not related (equ
commands). In the general
case, these diagnostics are directed acyclic subgraphs (encoded in the
BCG format) containing all sequences that, when executed simultaneously
in the two LTSs, lead to non-equivalent states. In the particular case where
diagnostics are just a single sequence, aldebaran
displays this sequence
using the seq
format, in the same way as bcg_cmp
When the source is erroneous, error messages are issued. Exit
status is 0 if everything is alright, 1 otherwise.
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).
- LTS in the Aldebaran format (input or output)
- LTS in the BCG
format (input or output)
- network of communicating LTSs (input)
- list of labels to hide (input)
- list of labels
to rename (input)
- license file
- shell-script (version 7.*)
- diagnostic file
Reference Manual, aut
Additional information is available from the CADP Web page located at http://cadp.inria.fr
Directives for installation are given in files $CADP/INSTALLATION_*.
changes and improvements to this software are reported and commented in
Please report any bug to email@example.com
Table of Contents