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

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 MUST be installed! It is provided in dep/ folder.
(see guppy-0.1.9.tar.gz)

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

Please install Guppy 0.1.9 before our ATAO Solver. All informations available into
dep/guppy-0.1.9.tar.gz

Installer not yet available. Source code only.

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

In the main directory this command executes the full test suite:
		run test
(the bash script runexample do the same thing and clean the log file. Also
runexample_debug add debug informations to the log)

If you need profiling informations try:
		run test profile

All informations are stored in the log file placed in the main directory.
For debug informations use the option "debug":
		run test debug
		
If you need to pipe the output try
		run test noprogress
		
Combined options: 
		run test debug noprogress profile
	
Benchmarks are available:
		run stresstest1
		run 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.

run is a wrapper for the full command:
	python -O ./EmptinessATA.py

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

Please see doc/tutorial.

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

MTL module is not full working and needs performance improvements.

(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.2 beta
RELEASED: april 2010

NEXT RELEASE: 1.2.5 RC1
DUE FOR: may 2010

# 1.2 beta: First public beta of the project
	+ more operations for automata (intersection, union, negation)
	+ added support for MTL (and conversion to ATAO. To be finished by next release)
	+ a lot of bugfixing
	+ added run command
	+ unified test cases
	+ many optimizations
	+ better logging
	+ tutorial

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