bench/stutter: add a "user" benchmark

* bench/stutter/user.sh: New bench.
* bench/stutter/Makefile.am: Add it.
* bench/stutter/README: Mention it.
* bench/stutter/stutter_bench.sh: Run it.

bench/stutter/Makefile.am

@@ -1,5 +1,5 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2014 Laboratoire de Recherche et Développement
+## Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
 ## de l'Epita (LRDE).
 ##
 ## This file is part of Spot, a model checking library.
@@ -30,4 +30,4 @@ bin_PROGRAMS = stutter_invariance_randomgraph \
 stutter_invariance_randomgraph_SOURCES = stutter_invariance_randomgraph.cc
 stutter_invariance_formulas_SOURCES = stutter_invariance_formulas.cc
 
-EXTRA_DIST = stutter_bench.sh stutter.ipynb
+EXTRA_DIST = stutter_bench.sh stutter.ipynb user.sh

bench/stutter/README

@@ -1,20 +1,22 @@
 This benchmark measures the performance of different algorithms to
-check if property (expressed as a formula or as a deterministic TGBA)
+check if a property is stutter-invariant.  When the benchmark is run
-is stutter-invariant.  When the benchmark is run on formulas, the
+on formulas, the translation time is not included in the measured
-translation time is not included in the measured time.
+time.
 
-
+To reproduce the benchmark run
-To reproduce the benchmark is to run
 
   % ./stutter_bench.sh -j8
 
-to create bench_formulas.csv and bench_randgraph.csv.
 (Adjust -j8 to the number of cores you have.)
 
-Then explore these data the provided ipython notebook
+This should create three files:
 
-  % ipython notebook --pylab=inline stutter.ipynb
+  - bench_formulas.csv
-
+      running stutter checks on LTL formulas, but without including
-
+      LTL translation time.
-The time in bench_formulas.csv is reported in microseconds, while the
+  - bench_randgraph.csv
-time in bench_randgraph.csv is in seconds.
+      unning stutter checks on deterministic TGBA, without including
+      complementation time.
+  - ltl-user-bench.csv
+      running stutter checks on LTL formulas, from the user point
+      of view, i.e., timing the whole "ltlfilt" run.

bench/stutter/stutter_bench.sh

@@ -3,6 +3,8 @@
 RANDLTL=../../src/bin/randltl
 LTLFILT=../../src/bin/ltlfilt
 
+echo 'ltl-user-bench.csv:; ./user.sh' > run.mk
+
 pos="pos.states,pos.trans,pos.edges,pos.scc,pos.nondet"
 neg="neg.states,neg.trans,neg.edges,neg.scc,neg.nondet"
 algos="time1,time2,time3,time4,time5,time6,time7,time8"
@@ -17,7 +19,7 @@ for ap in 1 2 3 4; do
 done
 
 echo "$OUTPUTF:$all; (echo 'formula,ap,$pos,$neg,$algos,res'; cat $all) > \$@"
-) > run.mk
+) >> run.mk
 
 OUTPUTG=bench_randgraph.csv
 (
@@ -32,4 +34,9 @@ done
 echo "$OUTPUTG:$all; (echo 'd,ap,seed,$pos,$neg,$algos,res'; cat $all) > \$@"
 ) >> run.mk
 
+
 make "$@" -f run.mk $OUTPUTF $OUTPUTG
+# Do this one separately from the rest, because it will eat the memory
+# and will either die from out-of-memory, or from needing more that 32
+# acceptance sets.
+make "$@" -f run.mk ltl-user-bench.csv

bench/stutter/user.sh

@@ -0,0 +1,23 @@
+#!/bin/sh
+RANDLTL=../../src/bin/randltl
+LTLFILT=../../src/bin/ltlfilt
+LTLDO=../../src/bin/ltldo
+
+set -e -x
+
+(
+must_exit=false
+echo ap,algo,time,matched,exit.status
+for ap in 1 2 3 4; do
+    $RANDLTL $ap --tree-size=..30 -n -1 | $LTLFILT --ap=$ap | $LTLFILT -v --nox -n 500 > formulas
+    for algo in 1 2 3 4 5 6 7 8 0; do
+	es=0
+	SPOT_STUTTER_CHECK=$algo /usr/bin/time -o user-$ap-$algo.csv -f "$ap,$algo,%e" $LTLFILT --stutter-invariant formulas > matched-$ap-$algo.ltl || must_exit=true es=$?
+	matched=`wc -l < matched-$ap-$algo.ltl`
+	csv=`tail -n 1 user-$ap-$algo.csv`
+	echo $csv,$matched,$es
+	rm -f user-$ap-$algo.csv
+	$must_exit && exit 0
+    done
+done
+) > ltl-user-bench.csv