This is the README file for , a prototype to check universality of Buechi automata.
Installation
============
1) Compilation:
Run the script file :
sh ./COMPILE
This creates an executable named
2) Execution:
Run the executable with or without argument:
./mh
or
./mh univ.txt
Usage
=====
A. The typical usage is ./mh
The file contains a text description of the automaton to check.
The first number is the number of states of the automaton. States are numbered 1,2,...,n. (in the source code however, states are numbered 0,1,...,n-1)
Then comes the list of accepting states. The list is terminated by a dash.
Then comes the list of transitions. A transition is a triple (start_state, letter, target_state)
where is either 0 (coding an 'a') or 1 (coding a 'b').
Each of these lists is given in no particular order.
The initial state is always State 1.
Here is an example:
3 /* The automaton has 3 states. States are numbered 1,2,3 */
3 /* The automaton has one accepting state, namely State 3 */
- /* separator */
1 /* The first transition is (1,0,2): from State 1, read 'a', goto State 2
0
2
1 /* The second transition is (1,0,3): from State 1, read 'a', goto State 3
0
3
1 /* The third transition is (1,1,3): from State 1, read 'b', goto State 3
1
3
3 /* etc. */
0
3
3
1
3
B. There is an alternative usage, with no argument: ./mh
This runs on a randomly generated automaton of 50 states, with branching degree r=2
and density of accepting states f=0.5
The generated automaton is written in the file
Output
======
The output is either 'Universal' or 'Not Universal'
and an upper bound of the duration of the computation.
Examples
========
Three examples are provided: , and
Documentation
=============
There is no other documentation available.
The program is based on the following paper:
Laurent Doyen and Jean-François Raskin. Improved algorithms for the automata
based approach to model-checking. Proceedings of TACAS 2007, LNCS 4424,
Springer-Verlag, Braga, 2007
Contact
=======
For more help or info, please contact Laurent Doyen.
http://mtc.epfl.ch/%7Edoyen/antichains/antichains.html
Upgrade
=======
The file , courtesy of Seth Fogarty,
contains an upgraded version that essentially fixes
memory leaks.