Aldebaran file format

From MCRL2

The Aldebaran file format is a simple format for storing labelled transition systems (LTS's) explicitly.

Files in this format usually have the extension '.aut'.

Syntax

The syntax of an Aldebaran file consists of a number of lines, where the first line is aut_header and the remaining lines are aut_edges.

aut_header is defined as follows:

aut_header ::= "des (" first_state "," nr_of_transitions "," nr_of_states ")"

Here:

• first_state is a number representing the first state, which should always be 0
• nr_of_transitions is a number representing the number of transitions
• nr_of_states is a number representing the number of states

An aut_edge is defined as follows:

 aut_edge ::= "(" start_state "," label "," end_state ")"

Here:

• start_state is a number representing the start state of the edge;
• label is a string enclosed in double quotes representing the label of the edge;
• end_state is a number representing the end state of the edge.

Example

The following example shows a simple labelled transition system of the dining philosophers problem for two philosophers, visualised using ltsgraph:

This transition system is represented by the following Aldebaran file:

des (0,12,10)
(0,"lock(p2, f2)",1)
(0,"lock(p1, f1)",2)
(1,"lock(p1, f1)",3)
(1,"lock(p2, f1)",4)
(2,"lock(p2, f2)",3)
(2,"lock(p1, f2)",5)
(4,"eat(p2)",6)
(5,"eat(p1)",7)
(6,"free(p2, f2)",8)
(7,"free(p1, f1)",9)
(8,"free(p2, f1)",0)
(9,"free(p1, f2)",0)

Acknowledgements

The Aldebaran format is originally used in the CADP toolset. To be fully compatible with the original syntax definition, the labels of the edges should consist of at most 5000 characters.