diff --git a/ChangeLog b/ChangeLog index f61f26855..14056da86 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,11 @@ +2010-12-04 Alexandre Duret-Lutz + + Preliminary benchmark using genltl, introduced earlier. + + * bench/ltlclasses/: New benchmark. + * bench/Makefile.am: Add it. + * configure.ac: Adjust. + 2010-12-04 Alexandre Duret-Lutz * src/ltlvisit/syntimpl.cc: Reduce the number of dynamic_cast<>s. diff --git a/bench/Makefile.am b/bench/Makefile.am index 6e85fe248..a8b3f2d97 100644 --- a/bench/Makefile.am +++ b/bench/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement +## Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et Développement ## de l'Epita (LRDE). ## Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -21,4 +21,5 @@ ## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA ## 02111-1307, USA. -SUBDIRS = emptchk gspn-ssp ltl2tgba scc-stats split-product ltlcounter +SUBDIRS = emptchk gspn-ssp ltl2tgba scc-stats split-product ltlcounter \ + ltlclasses diff --git a/bench/ltlclasses/.gitignore b/bench/ltlclasses/.gitignore new file mode 100644 index 000000000..5223f5778 --- /dev/null +++ b/bench/ltlclasses/.gitignore @@ -0,0 +1,3 @@ +defs +out +result*.fm diff --git a/bench/ltlclasses/Makefile.am b/bench/ltlclasses/Makefile.am new file mode 100644 index 000000000..4ee518adc --- /dev/null +++ b/bench/ltlclasses/Makefile.am @@ -0,0 +1,23 @@ +# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement de +# l'EPITA (LRDE) +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 2 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + +EXTRA_DIST = run plot.gnu + +CLEANFILES = results*.fm diff --git a/bench/ltlclasses/README b/bench/ltlclasses/README new file mode 100644 index 000000000..9a1cd5e5d --- /dev/null +++ b/bench/ltlclasses/README @@ -0,0 +1,21 @@ +This benchmark plots the performance of the ltl2tgba_fm algorithm +for tanslating some classes of LTL formula. + +Execute "./run" to compute the raw numbers, then execture +"gnuplot plot.gnu" to plot the figures. + +The authors of the following paper defined 5 classes of LTL formulae +to stress the LTL-to-Büchi translators. + +@InProceedings{cichon.09.depcos, + author = {Jacek Cicho{\'n} and Adam Czubak and Andrzej Jasi{\'n}ski}, + title = {Minimal {B\"uchi} Automata for Certain Classes + of {LTL} Formulas}, + booktitle = {Proceedings of the Fourth International + Conference on Dependability of Computer Systems}, + pages = {17--24}, + year = {2009}, + publisher = {IEEE Computer Society}, +} + + diff --git a/bench/ltlclasses/defs.in b/bench/ltlclasses/defs.in new file mode 100644 index 000000000..20729104f --- /dev/null +++ b/bench/ltlclasses/defs.in @@ -0,0 +1,55 @@ +# -*- shell-script -*- +# Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# et Marie Curie. +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 2 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + +# Ensure we are running from the right directory. +test -f ./defs || { + echo "defs: not found in current directory" 1>&2 + exit 1 +} + +srcdir='@srcdir@' + +# Ensure $srcdir is set correctly. +test -f "$srcdir/defs.in" || { + echo "$srcdir/defs.in not found, check \$srcdir" 1>&2 + exit 1 +} + +LBT='@LBT@' +LBTT='@LBTT@' +LBTT_TRANSLATE="@LBTT_TRANSLATE@" +LTL2BA='@LTL2BA@' +LTL2NBA='@LTL2NBA@' +LTL2TGBA='@top_builddir@/src/tgbatest/ltl2tgba@EXEEXT@' +ELTL2TGBA='@top_builddir@/src/tgbatest/eltl2tgba@EXEEXT@' +MODELLA='@MODELLA@' +SPIN='@SPIN@' +WRING2LBTT='@WRING2LBTT@' + +for var in LBT LTL2BA LTL2NBA MODELLA SPIN WRING2LBTT +do + if eval 'test -z "$'$var'"'; then + eval HAVE_$var=no + else + eval HAVE_$var=yes + fi +done diff --git a/bench/ltlclasses/plot.gnu b/bench/ltlclasses/plot.gnu new file mode 100644 index 000000000..f19f93082 --- /dev/null +++ b/bench/ltlclasses/plot.gnu @@ -0,0 +1,52 @@ +set terminal postscript eps enhanced color +set ytics nomirror +set y2tics auto +set ylabel "states" +set y2label "ticks" +set key left top + +set output 'results1.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' \ + with filledcurve x1 title "Translation Time" axes x1y2, \ + 'results1.fm' using 1:2 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \ + with lines title "States" + +set output 'results2.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' \ + with filledcurve x1 title "Translation Time" axes x1y2, \ + 'results2.fm' using 1:2 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \ + with lines title "States" + +set output 'results3.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' \ + with filledcurve x1 title "Translation Time" axes x1y2, \ + 'results3.fm' using 1:2 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \ + with lines title "States" + +set output 'results4.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' \ + with filledcurve x1 title "Translation Time" axes x1y2, \ + 'results4.fm' using 1:2 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \ + with lines title "States" + +set output 'results5.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' \ + with filledcurve x1 title "Translation Time" axes x1y2, \ + 'results5.fm' using 1:2 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \ + with lines title "States" + diff --git a/bench/ltlclasses/run b/bench/ltlclasses/run new file mode 100755 index 000000000..351ef3f05 --- /dev/null +++ b/bench/ltlclasses/run @@ -0,0 +1,43 @@ +#!/bin/sh + +# Copyright (C) 2010 Laboratoire de Recherche et Développement de +# l'EPITA (LRDE) +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 2 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + +. ./defs + +gen="$srcdir/../../src/ltltest/genltl" + +for F in 1 2 3 4 5; do + echo "# Benching ltl2tgba_fm for family F=$F" + echo "# e.g. `$gen $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 time2, user time1, system time2, wall time2" + for n in 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15; do + $LTL2TGBA -T -r1 -DS -k -f "`"$gen" $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 + done | tee results$F.fm +done +echo "# now run 'gnuplot plot.gnu'" diff --git a/configure.ac b/configure.ac index 3027097f2..f80aba023 100644 --- a/configure.ac +++ b/configure.ac @@ -83,6 +83,8 @@ AC_CONFIG_FILES([ bench/gspn-ssp/defs bench/ltlcounter/Makefile bench/ltlcounter/defs + bench/ltlclasses/Makefile + bench/ltlclasses/defs bench/ltl2tgba/Makefile bench/ltl2tgba/defs bench/scc-stats/Makefile