diff --git a/bench/ltlclasses/plot.gnu b/bench/ltlclasses/plot.gnu index f19f93082..1f0032457 100644 --- a/bench/ltlclasses/plot.gnu +++ b/bench/ltlclasses/plot.gnu @@ -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" - diff --git a/bench/ltlclasses/run b/bench/ltlclasses/run index 5843581b4..6e8f83027 100755 --- a/bench/ltlclasses/run +++ b/bench/ltlclasses/run @@ -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 . -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'" diff --git a/bench/ltlcounter/plot.gnu b/bench/ltlcounter/plot.gnu index 09b3a6106..da6f40e7e 100644 --- a/bench/ltlcounter/plot.gnu +++ b/bench/ltlcounter/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" diff --git a/bench/ltlcounter/run b/bench/ltlcounter/run index 195b24689..1a6a865c0 100755 --- a/bench/ltlcounter/run +++ b/bench/ltlcounter/run @@ -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 . -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'"