This is the README file for <mh>, a prototype to check universality of Buechi automata.


Installation
============

1) Compilation:
 
  Run the script file <COMPILE>: 

sh ./COMPILE

  This creates an executable named <mh> 


2) Execution:

  Run the executable <mh> with or without argument:

./mh

or

./mh univ.txt


Usage
=====

A. The typical usage is  ./mh <filename>

The file <filename> 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 <letter> 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 <mh> 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 <graph.txt>


Output
======

The output is either 'Universal' or 'Not Universal'
and an upper bound of the duration of the computation.


Examples
========

Three examples are provided: <univ.txt>, <n-univ1.txt> and <n-univ2.txt>


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.
<firstname.lastname@epfl.ch> 
http://mtc.epfl.ch/%7Edoyen/antichains/antichains.html


Upgrade
=======

The file <mh-fogarty.c>, courtesy of Seth Fogarty, 
contains an upgraded version that essentially fixes 
memory leaks.