Alternating Timed Automata Solver Files

=================================================================================
				BIG WARNING
	This is an alpa version! The internal code is changing very fast. 
	Please wait the beta release in order to try, test and use our tools.
=================================================================================

#################################################################################
#################################################################################
########	Alternating Timed Automata (with one clock) Solver	#########
#################################################################################
#################################################################################

			this is the version 1.1 alpha

Original project made by Matteo Carini and Nicholas Fiorentini for the 
software engineering degree at Politecnico di Milano (september 2009). 
Project advisors: Paola Spoletini and Carlo Alberto Furia

Current version is due to:
 * Matteo Carini (matteo <dot> carini <at> mail <dot> polimi <dot> it)
 * Nicholas Fiorentini (http://www.lordgordon.com)
 * Paola Spoletini (http://www.dei.polimi.it/personale/docentidettaglio.php?id_docente=229)
 * Carlo Alberto Furia (http://se.ethz.ch/people/furia/)

			The project is released under
		    GNU GENERAL PUBLIC LICENSE v3 License 
		(more at http://www.gnu.org/licenses/gpl.html)
		     See LICENSE.txt for full license text

Official project page: http://sourceforge.net/projects/atao/

Abstract: Our goal is to develop a full working solver for alternating timed automata 
(with one clock) in Python. The algorithm implements the decidability demonstration 
for the emptiness problem over finite words proposed by Lasota and Walukiewicz.

#################################################################################
#################################################################################
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
	0. QUICK START
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

This software need python 2.6 (should still work with 2.5 releases) but not 3.x!
The required module Guppy 0.1.9 is already packed into the library. You don't have
to install it!

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
	1. INSTALLATION
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Not yet available. Source code only.

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
	2. WORKING WITH ATAO SOLVER
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

In the main directory this command executes the full test suite:
		python ataocore/src/EmptinessATA.py test
(the bash script runexample do the same thing)

If you need profiling informations try:
		python ataocore/src/EmptinessATA.py test profile

All informations are stored in the log file placed in the main directory.
For debug informations use the option "debug":
		python ataocore/src/EmptinessATA.py test debug
		
If you need to pipe the output try
		python ataocore/src/EmptinessATA.py test noprogress
		
Combined options: 
	python ataocore/src/EmptinessATA.py test debug noprogress profile
	
Benchmarks are available:
	python ataocore/src/EmptinessATA.py stresstest1
	python ataocore/src/EmptinessATA.py stresstest2
	
With a dual core intel core duo processor (2 GHz and 4 GB RAM) we reached a 
cmax of 61 (in ~500 seconds and 150 MiB) for stresstest1 and cmax of 9 
(in ~8000 seconds and ~1,2 MiB) for stresstest2.

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
	3. HOW TO USE ATAO SOLVER IN YOUR SOFTWARE
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Please see ataocore/src/test/fulltests source for some useful example. A complete 
and detailed tutorial will be available for beta release.

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
	4. IMPORTANT BUG, HACKS AND OTHERS USEFUL INFORMATIONS
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

(For a full list see https://sourceforge.net/apps/trac/atao/)

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
	6. MODULES AND LIBRARY USED IN THIS SOFTWARE
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


	Guppy-PE 0.1.9
Sverker Nilsson <sn@sncs.se> (Homepage: http://sncs.se)
Guppy-PE homepage: http://guppy-pe.sourceforge.net
See README.txt in Guppy directory


	Murmur hashing algorithm 2
This is a python implementation of the common hashing algorithm know as murmur
(version 2). See: http://murmurhash.googlepages.com/
This is an hashing algorithm well balanced for general purpose usage.

Examples and tutorial are directly cited in the source code.

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
	7. CHANGELOG
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

LAST STABLE RELEASE: None, so far!

CURRENT RELEASE: 1.1 alpha
RELEASED: not yet

NEXT RELEASE: 1.2 beta
DUE FOR: feb 2010
Major improvements: operations on automata (intersection), MTL implementation,
		    and much more...

# 1.1 alpha: First public release of the project
	+ extreme performance improvements (time and memory) 
	+ better testing suite
	+ clean code and more documentation
	+ optimized hashing (using murmur hashing 2 algorithm)
	+ LTL precalculus and bugfixing
	+ memory profiling
	+ full debug logging
	- no multiprocessing (postponed for a future version)

# 1.0.0 alpha: This was the first release made for the thesis by Matteo Carini and
	       Nicholas Fiorentini.