Commit 042c7a0f authored by Alexandre GBAGUIDI AISSE's avatar Alexandre GBAGUIDI AISSE
Browse files

Update dtgbasat benchmark

* bench/dtgbasat/config.bench: Configuration file sample used by gen.py
* bench/dtgbasat/gen.py: Script that can generate both bench script and
pdf results.
* bench/dtgbasat/stats.sh: Change stat.sh into stat-gen.sh that will be
generated by gen.py script.
* bench/dtgbasat/Makefile.am: Add new files.
* bench/dtgbasat/README: Update README.
* bench/dtgbasat/stat-gen.sh: Add stat script generated by gen.py and
default config.bench file.
parent 823dc56e
......@@ -17,6 +17,6 @@
## along with this program. If not, see <http://www.gnu.org/licenses/>.
EXTRA_DIST = formulas prepare.sh rundbamin.pl stat.sh stats.sh tabl.pl \
tabl1.pl tabl2.pl tabl3.pl tabl4.pl
tabl1.pl tabl2.pl tabl3.pl tabl4.pl gen.py config.bench
......@@ -9,6 +9,9 @@ Note that the encoding used in the SAT-based minimization have evolved
since the paper, so if you want to reproduce exactly the benchmark
from the paper, you should download a copy of Spot 1.2.3.
This benchmark has grown since FORTE'14. Some new SAT-based methods have
been implemented. This benchmark measures all the methods and identifies the
best.
To reproduce, follow these instructions:
......@@ -55,19 +58,32 @@ To reproduce, follow these instructions:
You should set such a limit with "ulimit" if you like. For instance
% ulimit -v 41943040
9) Actually run all experiments
9) Before running the experiment, as Spot has now more SAT-based minimization
methods, you may want to reduce or choose the methods to be benched.
Have a look at the 'config.bench' file. By default, it contains all the
possible methods. Leave it unchanged if you want to compare all methods.
If it is changed, you need to re-generate the stat-gen.sh file by running:
% ./gen.py script --timeout <int> --unit <h|m|s>
% make -j4 -f stat.mk
10) Actually run all experiments
This will build a CSV file called "all.csv".
% make -j4 -f stat.mk
10) You may generate LaTeX code for the tables with the scripts:
- tabl.pl: Full data.
- tabl1.pl, tabl2.pl, tabl3.pl, tabl4.pl: Partial tables as shown
in the paper.
This will build a CSV file called "all.csv".
All these script takes the CSV file all.csv as first argument, and
output LaTeX to their standard output.
11) You may generate LaTeX code for the tables with 'gen.py'. This script is
really helpful as it permits you to generate even partial results. If after
all benchmarks, you want to compare only two methods among the others, just
comment the others in the configuration file 'config.bench' and run this
script.
% ./gen.py results
This scripts read the all.csv file generated at the end of the benchmark
and outputs two PDF documents:
-results.pdf: Which contains all statistics about each formula for each
method.
-resume.pdf which present two tables that count how many times a method
is better than another.
For more instruction about how to use ltl2tgba and dstar2tgba to
......
# This is a comment.
# This file is only used by the gen.py script.
#
# If you need to execute some shell code before a method, just write:
# 'sh "your_shell_code_in_one_line"' before that method.
#
# For each method, here is the syntax:
# "name_of_the_bench":"short_code">"some -x options"
# (see man spot-x for details)"
sh export SPOT_SATSOLVER="glucose -verb=0 -model %I > %O"
Glucose (As before):glu>sat-minimize=4
sh export SPOT_SATSOLVER="picosat %I > %O"
PicoSAT (As before):pic>sat-minimize=4
sh unset SPOT_SATSOLVER
PicoLibrary:libp>sat-minimize=4
Incr Naive:incr1>sat-minimize=3,param=-1
Incr param=1:incr2p1>sat-minimize=3,param=1
Incr param=2:incr2p2>sat-minimize=3,param=2
Incr param=4:incr2p4>sat-minimize=3,param=4
Incr param=8:incr2p8>sat-minimize=3,param=8
Assume param=1:assp1>sat-minimize=2,param=1
Assume param=2:assp2>sat-minimize=2,param=2
Assume param=3:assp2>sat-minimize=2,param=2
Assume param=4:assp4>sat-minimize=2,param=4
Assume param=5:assp5>sat-minimize=2,param=5
Assume param=6:assp6>sat-minimize=2,param=6
Assume param=7:assp7>sat-minimize=2,param=7
Assume param=8:assp8>sat-minimize=2,param=8
Dichotomy:dicho>sat-minimize
This diff is collapsed.
This diff is collapsed.
......@@ -17,15 +17,15 @@ while IFS=, read f type accmax accmin; do
case $type in
*TCONG*)
echo "$n.log:; ./stat.sh $n '$f' $type $accmax >\$@" >> stats.tmp
echo "$n.log:; ./stat-gen.sh $n '$f' $type $accmax >\$@" >> stats.tmp
all="$all $n.log"
n=`expr $n + 1`
echo "$n.log:; ./stat.sh $n '$f' DRA-CONG $accmax >\$@" >> stats.tmp
echo "$n.log:; ./stat-gen.sh $n '$f' DRA-CONG $accmax >\$@" >> stats.tmp
all="$all $n.log"
n=`expr $n + 1`
;;
*)
echo "$n.log:; ./stat.sh $n '$f' $type $accmax >\$@" >> stats.tmp
echo "$n.log:; ./stat-gen.sh $n '$f' $type $accmax >\$@" >> stats.tmp
all="$all $n.log"
n=`expr $n + 1`
;;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment