The tool PACMAN derives counting invariants for parameterized concurrent programs and incrementally predicate abstract them leveragin on a nested constrained monotonic abstraction cegar loop implemented by the sister project zaama.


*Download ZAAMA
In order to use PACMAN, you need the tool ZAAMA.
Download the source of ZAAMA from https://gitlab.ida.liu.se/apv/zaama,
put it besides pacman/ and follow the instructions in README for installation of required packages and compilation.

*install flex, bison, 
	sudo apt-get install flex
	sudo apt-get install bison

*install ppl 
Download ppl source, unzip and do
	sudo make install

Then find the ppl.hh header file (e.g.  in /usr/local/include/ppl.hh or /usr/include/x86_64-linux-gnu/ppl.hh)
change the following line:
typedef typeof(__mpz_struct()._mp_size) mp_size_field_t;

to this:
typedef decltype(__mpz_struct()._mp_size) mp_size_field_t;

*install antlr:
download antlr for cpp target. unzip it and copy the contents of include/ to /usr/include/


	cd pacman
	mkdir build; cd build
	cmake ../src 
to run a pacman test: 
	./pacman path/to/test/file
There are several test programs available in pacman/examples/

Remark: for eclipse in debug mode, use: 

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

instead of cmake ../src