ALDEBARAN manual page
Table of Contents

Name

aldebaran - minimization and comparison of labelled transitions systems

Important Notice

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):

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"). 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 of aldebaran.

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

Description

aldebaran allows the minimization or comparison of Labelled Transitions Systems (LTS for short) with respect to various equivalence and preorder relations. It 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.

-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 format (see the DIAGNOSTICS 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:

-<relation><action>

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

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

In version 7.* of aldebaran, the method is selected automatically as follows:

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

Options

The following options are currently available:
-stat      
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 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.

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

Renaming and hiding patterns are applied in the order in which they occur on the command line.

Diagnostics

aldebaran produces diagnostics to explain why two LTSs are not related (equ or ord 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 and bisimulator do.

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, aut , bcg , bcg_cmp , bcg_info , bcg_io , bcg_labels , bcg_min , bcg_open , bisimulator , caesar_hide_1 , caesar_rename_1 , evaluator , exp , exp.open , exhibitor , generator , reductor , seq

Additional information is available from the CADP Web page located at http://cadp.inria.fr

Directives for installation are given in files $CADP/INSTALLATION_*.

Recent changes and improvements to this software are reported and commented in file $CADP/HISTORY.

Bugs

Please report any bug to [email protected]

Table of Contents