Z

zaama

constrained monotonic abstraction for counter machines

*******************************************************************
INSTALLING ZAAMA
*******************************************************************
REQUIRED:

*install gcc,g++ and cmake:

	sudo apt-get update 
	sudo apt-get install gcc
	sudo apt-get install g++
	sudo apt-get install cmake

*install boost:
	sudo apt-get install libboost-all-dev

*install gmp:
	sudo apt-get install libgmp3-dev

*install z3:
download z3,unzip it, then do

   cd /path/to/z3/folder
   python scripts/mk_make.py
   cd build
   make
   sudo make install

*install mathsat:
download mathsat,unzip, copy include/* and lib/* to /usr/include and /usr/lib

*install cplex:
download the binary file and execute it in root mode

********************************************************************
COMPILING ZAAMA
********************************************************************

	cd zaama
	mkdir build; cd build

-->You can run zaama in different modes. Here is the discreption:
BACKWARD = ON/OFF 	run the analysis in backward/forward

LAZY = ON/OFF		use lazy/eager refinement

UPWARD = ON/OFF		do/don't use order-based lazy

WIDEN = ON/OFF 		do/don't use descendents-based lazy

Allowed combinations of above parameters are as follows:
( BACKWARD can be used in both ON/OFF in all combinations)
-DBACKWARD=OFF -DLAZY=OFF -DUPWARD = OFF -DWIDEN = OFF	#eager refinement
-DBACKWARD=OFF -DLAZY=ON -DUPWARD = OFF -DWIDEN = OFF	#point-based lazy refinement
-DBACKWARD=OFF -DLAZY=ON -DUPWARD = ON -DWIDEN = OFF	#order-based lazy refinement
-DBACKWARD=OFF -DLAZY=ON -DUPWARD = OFF -DWIDEN = ON	#descendents-based lazy refinement
-DBACKWARD=OFF -DLAZY=ON -DUPWARD = ON -DWIDEN = ON	#order-based and descendents-based lazy refinement



You should pass the parameters to CMAKE as follows:
	cmake ../src -DBACKWARD=OFF -DLAZY=ON -DUPWARD = OFF -DWIDEN = OFF
You can check and change parameters you set in build/config.h. Then do make
********************************************************************
TESTING ZAAMA
********************************************************************
You can either run the tests individually or use the test script.
Run an individual test: 
	./zaama /path/to/test/file
There are several test files available in zaama/examples/ .

Run the test script:
	cd test/
	python test_zaama.py 

You will be prompted for selecting the analysis mode and number of tests to run.
The test results will be written to test/forward_tests or/and test/backward_test depending on the mode you choose for running the tests.
In each directory you can see the execution time of tests in the file execution_times.
All execution times will be extracted to results-forward and/or results-backward.


---------------
PS: for eclipse in debug mode, use: 

cmake -G"Eclipse CDT4 - Unix Makefiles" -D CMAKE_BUILD_TYPE=Debug
../src

instead of cmake ../src
---------------