bench: make ltlcross and ltlclass work again
They were not updated since we moved binaries around in Spot 2.0. Let them use ltl2tgba directly. * bench/ltlclasses/plot.gnu, bench/ltlclasses/run, bench/ltlcounter/plot.gnu, bench/ltlcounter/run: Adjust.
This commit is contained in:
Alexandre Duret-Lutz
parent
7e7c257597
commit
98e7e4e49a
4 changed files with 43 additions and 78 deletions
|
|
@ -2,51 +2,40 @@ set terminal postscript eps enhanced color
|
|||
set ytics nomirror
|
||||
set y2tics auto
|
||||
set ylabel "states"
|
||||
set y2label "ticks"
|
||||
set y2label "seconds"
|
||||
set key left top
|
||||
|
||||
set output 'results1.fm.eps'
|
||||
set output 'resultsalpha.fm.eps'
|
||||
|
||||
plot 'results1.fm' using 1:($4+$5) '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \
|
||||
with filledcurve x1 title "Total Time" axes x1y2, \
|
||||
'results1.fm' using 1:4 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \
|
||||
plot 'resultsalpha.fm' using 1:4 '%lf,%lf,%lf,%lf' \
|
||||
with filledcurve x1 title "Translation Time" axes x1y2, \
|
||||
'results1.fm' using 1:2 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \
|
||||
'resultsalpha.fm' using 1:2 '%lf,%lf,%lf,%lf' \
|
||||
with lines title "States"
|
||||
|
||||
set output 'results2.fm.eps'
|
||||
set output 'resultsbeta.fm.eps'
|
||||
|
||||
plot 'results2.fm' using 1:($4+$5) '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \
|
||||
with filledcurve x1 title "Total Time" axes x1y2, \
|
||||
'results2.fm' using 1:4 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \
|
||||
plot 'resultsbeta.fm' using 1:4 '%lf,%lf,%lf,%lf' \
|
||||
with filledcurve x1 title "Translation Time" axes x1y2, \
|
||||
'results2.fm' using 1:2 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \
|
||||
'resultsbeta.fm' using 1:2 '%lf,%lf,%lf,%lf' \
|
||||
with lines title "States"
|
||||
|
||||
set output 'results3.fm.eps'
|
||||
set output 'resultsbeta-prime.fm.eps'
|
||||
|
||||
plot 'results3.fm' using 1:($4+$5) '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \
|
||||
with filledcurve x1 title "Total Time" axes x1y2, \
|
||||
'results3.fm' using 1:4 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \
|
||||
plot 'resultsbeta-prime.fm' using 1:4 '%lf,%lf,%lf,%lf' \
|
||||
with filledcurve x1 title "Translation Time" axes x1y2, \
|
||||
'results3.fm' using 1:2 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \
|
||||
'resultsbeta-prime.fm' using 1:2 '%lf,%lf,%lf,%lf' \
|
||||
with lines title "States"
|
||||
|
||||
set output 'results4.fm.eps'
|
||||
set output 'resultsphi.fm.eps'
|
||||
|
||||
plot 'results4.fm' using 1:($4+$5) '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \
|
||||
with filledcurve x1 title "Total Time" axes x1y2, \
|
||||
'results4.fm' using 1:4 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \
|
||||
plot 'resultsphi.fm' using 1:4 '%lf,%lf,%lf,%lf' \
|
||||
with filledcurve x1 title "Translation Time" axes x1y2, \
|
||||
'results4.fm' using 1:2 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \
|
||||
'resultsphi.fm' using 1:2 '%lf,%lf,%lf,%lf' \
|
||||
with lines title "States"
|
||||
|
||||
set output 'results5.fm.eps'
|
||||
set output 'resultsxi.fm.eps'
|
||||
|
||||
plot 'results5.fm' using 1:($4+$5) '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \
|
||||
with filledcurve x1 title "Total Time" axes x1y2, \
|
||||
'results5.fm' using 1:4 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \
|
||||
plot 'resultsxi.fm' using 1:4 '%lf,%lf,%lf,%lf' \
|
||||
with filledcurve x1 title "Translation Time" axes x1y2, \
|
||||
'results5.fm' using 1:2 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \
|
||||
'resultsxi.fm' using 1:2 '%lf,%lf,%lf,%lf' \
|
||||
with lines title "States"
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
#!/bin/sh
|
||||
|
||||
# Copyright (C) 2010, 2012, 2013 Laboratoire de Recherche et
|
||||
# Copyright (C) 2010, 2012, 2013, 2017 Laboratoire de Recherche et
|
||||
# Développement de l'EPITA (LRDE)
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
|
|
@ -18,23 +18,17 @@
|
|||
# You should have received a copy of the GNU General Public License
|
||||
# along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
gen=../../src/bin/genltl
|
||||
LTL2TGBA=../../src/tests/ikwiad
|
||||
gen=../../bin/genltl
|
||||
LTL2TGBA=../../bin/ltl2tgba
|
||||
|
||||
for F in alpha beta beta-prime phi xi; do
|
||||
echo "# Benching ltl2tgba_fm for family ccj-$F"
|
||||
echo "# e.g. `$gen --ccj-$F 3`"
|
||||
echo "# the following values are also saved to file 'results$F.fm'"
|
||||
echo "# time1 = translation time"
|
||||
echo "# time2 = exploration time"
|
||||
echo "# n, states, transitions, user time1, system time1, wall time1, user time2, system time2, wall time2"
|
||||
echo "# time = translation time"
|
||||
echo "# n, states, edges, time"
|
||||
for n in 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20; do
|
||||
$LTL2TGBA -T -r1 -DS -ks -f "`"$gen" --ccj-$F $n`" >out 2>&1
|
||||
states=`sed -n 's/^states: \([0-9]*\)$/\1/p' out`
|
||||
transitions=`sed -n 's/^transitions: \([0-9]*\)$/\1/p' out`
|
||||
time=`sed -n 's/ *translating formula *| *\([0-9]*\) .*| *\([0-9]*\) .*| *\([0-9]*\) .*|.*/\1,\2,\3/p' out`
|
||||
time2=`sed -n 's/ *producing output *| *\([0-9]*\) .*| *\([0-9]*\) .*| *\([0-9]*\) .*|.*/\1,\2,\3/p' out`
|
||||
echo $n,$states,$transitions,$time,$time2
|
||||
$LTL2TGBA --any --low -B "`"$gen" --ccj-$F $n`" --stats="$n,%s,%e,%r"
|
||||
done | tee results$F.fm
|
||||
done
|
||||
echo "# now run 'gnuplot plot.gnu'"
|
||||
|
|
|
|||
|
|
@ -2,24 +2,20 @@ set terminal postscript eps enhanced color
|
|||
set ytics nomirror
|
||||
set y2tics auto
|
||||
set ylabel "states"
|
||||
set y2label "ticks"
|
||||
set y2label "seconds"
|
||||
set key left top
|
||||
|
||||
set output 'results.fm.eps'
|
||||
|
||||
plot 'results.fm' using 1:($4+$5) '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \
|
||||
with filledcurve x1 title "Total Time" axes x1y2, \
|
||||
'results.fm' using 1:4 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \
|
||||
plot 'results.fm' using 1:4 '%lf,%lf,%lf,%lf' \
|
||||
with filledcurve x1 title "Translation Time" axes x1y2, \
|
||||
'results.fm' using 1:2 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \
|
||||
'results.fm' using 1:2 '%lf,%lf,%lf,%lf' \
|
||||
with lines title "States"
|
||||
|
||||
|
||||
set output 'results.taa.eps'
|
||||
|
||||
plot 'results.taa' using 1:($4+$5) '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \
|
||||
with filledcurve x1 title "Total Time" axes x1y2, \
|
||||
'results.taa' using 1:4 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \
|
||||
with filledcurve x1 title "Translation Time" axes x1y2, \
|
||||
'results.taa' using 1:2 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \
|
||||
with lines title "States"
|
||||
# set output 'results.taa.eps'
|
||||
#
|
||||
# plot 'results.taa' using 1:4 '%lf,%lf,%lf,%lf' \
|
||||
# with filledcurve x1 title "Translation Time" axes x1y2, \
|
||||
# 'results.taa' using 1:2 '%lf,%lf,%lf,%lf' \
|
||||
# with lines title "States"
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
|
||||
# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2017 Laboratoire de
|
||||
# Recherche et Développement de l'EPITA (LRDE)
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
|
|
@ -18,35 +18,21 @@
|
|||
# You should have received a copy of the GNU General Public License
|
||||
# along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
gen=../../src/bin/genltl
|
||||
LTL2TGBA=../../src/tests/ikwiad
|
||||
gen=../../bin/genltl
|
||||
LTL2TGBA=../../bin/ltl2tgba
|
||||
|
||||
echo "# Benching ltl2tgba_fm..."
|
||||
echo "# the following values are also saved to file 'results.fm'"
|
||||
echo "# time1 = translation time"
|
||||
echo "# time2 = exploration time"
|
||||
echo "# n, states, transitions, user time1, system time1, wall time1, user time1, system time2, wall time2"
|
||||
for n in 1 2 3 4 5 6 7 8 9 10 11 12 13; do
|
||||
$LTL2TGBA -T -ks -f "`$gen --rv-counter-linear $n`" >out 2>&1
|
||||
states=`sed -n 's/^states: \([0-9]*\)$/\1/p' out`
|
||||
transitions=`sed -n 's/^transitions: \([0-9]*\)$/\1/p' out`
|
||||
time=`sed -n 's/ *translating formula *| *\([0-9]*\) .*| *\([0-9]*\) .*| *\([0-9]*\) .*|.*/\1,\2,\3/p' out`
|
||||
time2=`sed -n 's/ *producing output *| *\([0-9]*\) .*| *\([0-9]*\) .*| *\([0-9]*\) .*|.*/\1,\2,\3/p' out`
|
||||
echo $n,$states,$transitions,$time,$time2
|
||||
echo "# n, states, edge, time"
|
||||
for n in 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15; do
|
||||
$LTL2TGBA --any --low "`"$gen" --rv-counter-linear $n`" --stats="$n,%s,%e,%r"
|
||||
done | tee results.fm
|
||||
|
||||
echo "# Benching ltl2taa..."
|
||||
echo "# the following values are also saved to file 'results.taa'"
|
||||
echo "# time1 = translation time"
|
||||
echo "# time2 = exploration time"
|
||||
echo "# n, states, transitions, user time1, system time1, wall time1, user time1, system time2, wall time2"
|
||||
for n in 1 2 3 4 5 6 7; do
|
||||
$LTL2TGBA -T -ks -taa "`$gen --rv-counter-linear $n`" >out 2>&1
|
||||
states=`sed -n 's/^states: \([0-9]*\)$/\1/p' out`
|
||||
transitions=`sed -n 's/^transitions: \([0-9]*\)$/\1/p' out`
|
||||
time=`sed -n 's/ *translating formula *| *\([0-9]*\) .*| *\([0-9]*\) .*| *\([0-9]*\) .*|.*/\1,\2,\3/p' out`
|
||||
time2=`sed -n 's/ *producing output *| *\([0-9]*\) .*| *\([0-9]*\) .*| *\([0-9]*\) .*|.*/\1,\2,\3/p' out`
|
||||
echo $n,$states,$transitions,$time,$time2
|
||||
done | tee results.taa
|
||||
# echo "# Benching ltl2taa..."
|
||||
# echo "# the following values are also saved to file 'results.taa'"
|
||||
# echo "# n, states, transitions, time"
|
||||
# for n in 1 2 3 4 5 6 7; do
|
||||
# $LTL2TGBA --any --low "`"$gen" --rv-counter-linear $n`" --stats="$n,%s,%e,%r"
|
||||
# done | tee results.taa
|
||||
|
||||
echo "# now run 'gnuplot plot.gnu'"
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue