This file describes how to to launch the benchmark explained in the
paper.


Four archives can be downloaded:
   (a) : the fork of spot used for experiments 
   http://pagesperso-systeme.lip6.fr/Etienne.Renault/phd/data/spot-1.2.1a.tar.gz

   (b) :  the full archive of models and formulas for SPOT
   http://pagesperso-systeme.lip6.fr/Etienne.Renault/phd/data/replay-spot.zip

   (c) :  the full archive of models and formulas for LTSmin
   http://pagesperso-systeme.lip6.fr/Etienne.Renault/phd/data/replay-ltsmin.zip

   (d) :  the full archive of models and formulas for Divine
   http://pagesperso-systeme.lip6.fr/Etienne.Renault/phd/data/replay-divine.zip

   (c) : the CSV of results 
   http://pagesperso-systeme.lip6.fr/Etienne.Renault/benchs/TACAS-2015/full.tacas.csv.tar.gz


How to interpret the CSV of results?
------------------------------------

To understand CSV we denote by :

    (1)  LOG : which is the associated log, logs are numbered from
              r1.log to r3268.log and corresponds to the ith formula
      	       of the benchmark 
    (2)  cndfs1 : the wall time execution for cndfs with 1 thread
	 
    (3)  cndfs2 : the wall time execution for cndfs with 2 threads
	 
    (4)  cndfs4 : the wall time execution for cndfs with 4 threads
	 
    (5)  cndfs8 : the wall time execution for cndfs with 8 threads
	 
    (6)  cndfs12 : the wall time execution for cndfs with 12 threads
	 
    (7)  dijkstra1 : the wall time execution for dijkstra with 1 thread
	 
    (8)  dijkstra2 : the wall time execution for dijkstra with 2 threads
	 
    (9)  dijkstra4 : the wall time execution for dijkstra with 4 threads

    (10) dijkstra8 : the wall time execution for dijkstra with 8 threads

    (11) dijkstra12 : the wall time execution for dijkstra with 12 threads

    (12) mixed2 : the wall time execution for mixed with 2 threads

    (13) mixed4 : the wall time execution for mixed with 4 threads

    (14) mixed8 : the wall time execution for mixed with 8 threads

    (15) mixed12 : the wall time execution for mixed with 12 threads

    (16) tarjan1 : the wall time execution for tarjan with 1 thread

    (17) tarjan2 : the wall time execution for tarjan with 2 threads

    (18) tarjan4 : the wall time execution for tarjan with 4 threads

    (19) tarjan8 : the wall time execution for tarjan with 8 threads

    (20) tarjan12 : the wall time execution for tarjan with 12 threads

    (21) owcty1 : the wall time execution for owcty with 1 thread

    (22) owcty2 : the wall time execution for owcty with 2 threads

    (23) owcty4 : the wall time execution for owcty with 4 threads

    (24) owcty8 : the wall time execution for owcty with 8 threads

    (25) owcty12 : the wall time execution for owcty with 12 threads

    (26) type : describes wether the formula is verified or not

    (27) model : the model form this formula

Note that in this CSV you can find some values equals to 3600000 for CNDFS
algorithm; we denote by this value the fails of the emptiness check
within the time limit.


To relaunch our experiments :

Install SPOT 
------------

   wget   http://pagesperso-systeme.lip6.fr/Etienne.Renault/benchs/ATVA-2014/spot-1.2.1a.tar.gz
   cd spot-1.1.2a   
   autoreconf -vfi
   make
   make install


Install Divine 2.4 patched by LTSmin 
-------------------------------------

   git clone http://fmt.cs.utwente.nl/tools/scm/divine2.git
   cd divine2
   mkdir _build && cd _build
   cmake .. -DGUI=OFF -DRX_PATH= -DCMAKE_INSTALL_PREFIX=... -DMURPHI=OFF
   make
   make install

If you find any troubles doing this step, you can find more
informations at : http://fmt.cs.utwente.nl/tools/ltsmin/


Download and set up the Benchmark
----------------------------------

  wget  http://pagesperso-systeme.lip6.fr/Etienne.Renault/benchs/ATVA-2014/benchmark.tar.gz 
  cd benchmark
  
You then have to edit script/env.sh Note that for configuring the
benchmark you need to provide the path to the dve2check tool; you can
find it in spot/iface/dve2fasttgba/dve2check. Then type:

  bash scripts/makefile_generator.sh
  make



If you have any comments or question you can join me at 
   etienne.renault@lip6.fr
or
   renault@lrde.epita.fr