Table of Contents
aldebaran - minimization and comparison of labelled transitions
is a deprecated tool of CADP.
Instead of aldebaran
it is highly recommended to use the following tools
As regards the status and history of aldebaran, the following information
can be relevant:
- From version 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"). Because this program 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 because no
one volunteered port it to 64-bit platforms. Therefore, all the remarks about
version 6.6 are no longer relevant.
- Version 7.* of aldebaran is a shell-script
(located in file "$CADP/com/aldebaran") that was introduced in October
2005. This shell-script (1) provides an extensive backward compatibility
with previous versions of aldebaran by supporting all commands/options
but -dequ; (2) removes limitations existing in the previous versions of
aldebaran; and (3) tries to avoid semantic bugs as much as possible by
calling the other tools of CADP mentioned above instead of aldebaran 6.6.
] 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).
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).
can be applied:
- either to completely generated LTSs, which are usually
contained in files with the .aut or .bcg suffix. See below the section entitled
ALDEBARAN FORMAT FOR LTS and BCG FORMAT FOR LTS 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 a format readable by aldebaran.
- or to networks of communicating LTSs, which are contained in files with
the .exp suffix. See the section below entitled FORMAT FOR NETWORKS OF COMMUNICATING
LTS for a description of the .exp format.
The followings command
are currently available:
- Print the set of deadlock states (sinks)
for a LTS or a network of communicating LTSs.
- Determinize a LTS and
display the result as a new LTS.
- Display 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
tool, which provides more complete structure information
on a BCG graph.
- 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
- -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 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 <method> is a three-character
string among std, fly, or bdd, which is only meaningful with version 6.6
- `std' : use the Paige & Tarjan algorithm (except for branching
equivalence) or the Groote & Vaandrager algorithm (for branching equivalence
- `fly' : use the Fernandez & Mounier algorithm
- `bdd' : use the Minimal
Model Generation algorithm or BDD based algorithms
where <relation> is a
one-character string, either b, d, i, o, p, or s:
- `b' : use the strong bisimulation
equivalence [Park-81] or the corresponding preorder
- `d' : use the delay bisimulation
- `i' : use the tau*.a bisimulation [Fernandez-Mounier-90] or the
corresponding preorder (tau is written i in LOTOS)
- `o' : use the observational
- `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 FORMAT section below),
or of an acyclic BCG graph stored in file aldebaran.bcg (see the -diag option
for details about diagnostics in the BCG format).
- `ord' : same as equ, but use a preorder relation instead of the equivalence
In version 6.6 of aldebaran, not all combinations of methods,
relations and actions are implemented, but only the following:
version 7.* of aldebaran, options -fly, -std, and -bdd are meaningless and
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 on the fly using bisimulator.
Note that options -oord and -pord were not implemented in version 6.6 of aldebaran
(see table above).
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). Comparison of LTSs modulo delay equivalence
(-dequ option) is not implemented in version 7.* of aldebaran.
-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:
- If action is
`min' or `cla': -bdd will be the default method if filename1 is a .exp file,
otherwise -std will be the default method.
- If action is `equ' or `ord': -fly will
be the default method if either filename1 or filename2 is a .exp file, otherwise
-std will be the default method.
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.*.
The following options
- 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
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
Note: the full substitution possibilities described in the
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.
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>)
<to-state> are numbers and
<gate-name> is a character string enclosed
in double quotes (with up to 5000 characters).
<gate-name> is case-sensitive.
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
file describes a network of communicating
LTSs. The syntax of .exp
files is described in the exp.open
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-keyword> ::= 'behaviour'
<behaviour> ::= <lts>
| 'hide' <gate-list> 'in' <behaviour>
| <behaviour> <parallel-operator> <behaviour>
| '(' <behaviour> ')'
<lts> ::= '"'<any-string-without-double-quotes>'"'
<gate-list> ::= <gate>
| <gate> "," <gate-list>
<gate> ::= <string-denoting-a-lotos-gate-identifier>
<parallel-operator> ::= '||'
| '|[' <gate-list> ']|'
<string-denoting-a-lts-filename> is a character string starting with a
letter and containing only letters, underscores, and digits; it may also
terminate with a file extension such as .aut or .bcg. This syntax for filenames
is obsolete and kept for backward compatibility purpose: enclosing filenames
between double quotes is now the recommended syntax for .exp files.
is a character string starting with a letter and containing only letters,
underscores, and digits according to LOTOS syntactic rules for gate identifiers.
<behaviour> semantics is defined as follows:
- 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
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.
<lts> is always case-sensitive.
<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.
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
commands). A detailed description
of this format can be found in the manual page for exhibitor
kind of SEQUENCE format (either "simple" or "full") produced by aldebaran
depends on the verification algorithm chosen:
- If the -std method is used
with strong equivalence, of if the -fly method is used, aldebaran will produce
simple SEQUENCE format.
- If the -std method is used with an equivalence different
from (i.e. weaker than) strong equivalence, aldebaran will produce full
SEQUENCE format (the sequence will contain "
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
page for details). This often leads to much more compact diagnostics than
those exhibited by version 6.6 of aldebaran.
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
- LTS in the Aldebaran format (input
- LTS in the BCG format (input or output)
- network of communicating LTSs (input)
- list of labels to hide
- list of labels to rename (input)
- license file
- shell-script (version 7.*)
- diagnostic file
ALDEBARAN Reference Manual, bcg_info
is available from the CADP Web page located at http://cadp.inria.fr
for installation are given in files $CADP/INSTALLATION_*.
and improvements to this software are reported and commented in file $CADP/HISTORY.
Please report any bug to email@example.com
Table of Contents