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/benchs/ATVA-2014/spot-1.2.1a.tar.gz

   (b) :  the full archive of models and formulas
     http://pagesperso-systeme.lip6.fr/Etienne.Renault/benchs/ATVA-2014/benchmark.tar.gz

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

   (d) : the full logs (for the algorithm of LTSmin (cndfs) we add a
         CSV export to ease the log processing
   http://pagesperso-systeme.lip6.fr/Etienne.Renault/benchs/ATVA-2014/logs.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) cndfs_1 : the wall time execution for cndfs with 1 thread

    (3) cndfs_2 : the wall time execution for cndfs with 2 threads

    (4) cndfs_4 : the wall time execution for cndfs with 4 threads

    (5) cndfs_6 : the wall time execution for cndfs with 6 threads

    (6) cndfs_8 : the wall time execution for cndfs with 8 threads

    (7) dijkstra_1 : the wall time execution for dijkstra with 1 thread

    (8) dijkstra_2 : the wall time execution for dijkstra with 2 threads

    (9) dijkstra_4 : the wall time execution for dijkstra with 4 threads

    (10) dijkstra_6 : the wall time execution for dijkstra with 6 threads

    (11) dijkstra_8 : the wall time execution for dijkstra with 8 threads

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

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

    (14) mixed_6 : the wall time execution for mixed with 6 threads

    (15) mixed_8 : the wall time execution for mixed with 8 threads

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

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

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

    (19) tarjan_6 : the wall time execution for tarjan with 6 threads

    (20) tarjan_8 : the wall time execution for tarjan with 8 threads

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

    (22) model : the model form this formula

Note that in this CSV you can find some values equals to -1 for CNDFS
algorithm; we denote by this value results that are incorrect with the
LTSmin tool. We report this bug to the team of LTSmin!

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