From 3ce16272513ab47cfaa85c2b16da3f93864dc342 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 6 Nov 2009 16:45:11 +0100 Subject: [PATCH] Add a benchmark using Kristin Y. Rozier's LTLcounter scripts. * bench/ltlcounter/README, bench/ltlcounter/run, bench/ltlcounter/plot.gnu, bench/ltlcounter/defs.in, bench/ltlcounter/Makefile.am: New files. * bench/Makefile.am (SUBDIRS): Add ltlcounter. * configure.ac (AC_CONFIG_FILES): Adjust. * THANKS: Add her. --- ChangeLog | 13 ++++++++- THANKS | 1 + bench/Makefile.am | 4 +-- bench/ltlcounter/.gitignore | 3 ++ bench/ltlcounter/Makefile.am | 23 +++++++++++++++ bench/ltlcounter/README | 6 ++++ bench/ltlcounter/defs.in | 55 ++++++++++++++++++++++++++++++++++++ bench/ltlcounter/plot.gnu | 25 ++++++++++++++++ bench/ltlcounter/run | 55 ++++++++++++++++++++++++++++++++++++ configure.ac | 2 ++ 10 files changed, 184 insertions(+), 3 deletions(-) create mode 100644 bench/ltlcounter/.gitignore create mode 100644 bench/ltlcounter/Makefile.am create mode 100644 bench/ltlcounter/README create mode 100644 bench/ltlcounter/defs.in create mode 100644 bench/ltlcounter/plot.gnu create mode 100755 bench/ltlcounter/run diff --git a/ChangeLog b/ChangeLog index 73e3af2e2..84e1d5239 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,14 @@ +2009-11-06 Alexandre Duret-Lutz + + Add a benchmark using Kristin Y. Rozier's LTLcounter scripts. + + * bench/ltlcounter/README, bench/ltlcounter/run, + bench/ltlcounter/plot.gnu, bench/ltlcounter/defs.in, + bench/ltlcounter/Makefile.am: New files. + * bench/Makefile.am (SUBDIRS): Add ltlcounter. + * configure.ac (AC_CONFIG_FILES): Adjust. + * THANKS: Add her. + 2009-11-06 Alexandre Duret-Lutz Use a timer to clock the different phases of the translation. @@ -168,7 +179,7 @@ 2009-11-04 Alexandre Duret-Lutz - Fix a longstanding bug reported by Kristin Y. Rozier.. + Fix a longstanding bug reported by Kristin Y. Rozier. * src/ltlast/formula.hh (formula_ptr_less_than::operator()): Fix a typo where `l' was typed as `1'. diff --git a/THANKS b/THANKS index 6f517e9ee..0d8159baf 100644 --- a/THANKS +++ b/THANKS @@ -4,4 +4,5 @@ suggestions. Heikki Tauriainen Jean-Michel Couvreur Jean-Michel Ilié +Kristin Y. Rozier Yann Thierry-Mieg diff --git a/bench/Makefile.am b/bench/Makefile.am index 23e86fa82..33b3a17b8 100644 --- a/bench/Makefile.am +++ b/bench/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2005, 2008 Laboratoire d'Informatique de Paris 6 (LIP6), +## Copyright (C) 2005, 2008, 2009 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. ## @@ -19,4 +19,4 @@ ## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA ## 02111-1307, USA. -SUBDIRS = emptchk gspn-ssp ltl2tgba scc-stats split-product +SUBDIRS = emptchk gspn-ssp ltl2tgba scc-stats split-product ltlcounter diff --git a/bench/ltlcounter/.gitignore b/bench/ltlcounter/.gitignore new file mode 100644 index 000000000..651393aca --- /dev/null +++ b/bench/ltlcounter/.gitignore @@ -0,0 +1,3 @@ +*.eps +results* +defs diff --git a/bench/ltlcounter/Makefile.am b/bench/ltlcounter/Makefile.am new file mode 100644 index 000000000..4efee8761 --- /dev/null +++ b/bench/ltlcounter/Makefile.am @@ -0,0 +1,23 @@ +# Copyright (C) 2009 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 results.lacim results.fm.eps results.lacim.eps diff --git a/bench/ltlcounter/README b/bench/ltlcounter/README new file mode 100644 index 000000000..83cc30f50 --- /dev/null +++ b/bench/ltlcounter/README @@ -0,0 +1,6 @@ +This benchmark uses the ltlcounter scripts of Kristin Y. Rozier (See +src/tgbatest/ltlcounter/) to plot the performance of the ltl2tgba_fm +algorithm. + +Execute "./run" to compute the raw numbers, then execture +"gnuplot plot.gnu" to plot the figures. diff --git a/bench/ltlcounter/defs.in b/bench/ltlcounter/defs.in new file mode 100644 index 000000000..20729104f --- /dev/null +++ b/bench/ltlcounter/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/ltlcounter/plot.gnu b/bench/ltlcounter/plot.gnu new file mode 100644 index 000000000..86a8a9e10 --- /dev/null +++ b/bench/ltlcounter/plot.gnu @@ -0,0 +1,25 @@ +set terminal postscript eps enhanced color +set ytics nomirror +set y2tics auto +set ylabel "states" +set y2label "ticks" +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' \ + with filledcurve x1 title "Translation Time" axes x1y2, \ + 'results.fm' using 1:2 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \ + with lines title "States" + + +set output 'results.lacim.eps' + +plot 'results.lacim' using 1:($4+$5) '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \ + with filledcurve x1 title "Total Time" axes x1y2, \ + 'results.lacim' using 1:4 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \ + with filledcurve x1 title "Translation Time" axes x1y2, \ + 'results.lacim' using 1:2 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \ + with lines title "States" diff --git a/bench/ltlcounter/run b/bench/ltlcounter/run new file mode 100755 index 000000000..19856daa0 --- /dev/null +++ b/bench/ltlcounter/run @@ -0,0 +1,55 @@ +#!/bin/sh + +# Copyright (C) 2009 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 + +lcdir=$srcdir/../../src/tgbatest/ltlcounter + +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 time2, 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 -k -f "`$lcdir/LTLcounterLinear.pl $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.fm + +echo "# Benching ltl2tgba_lacim..." +echo "# the following values are also saved to file 'results.lacim'" +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; do + $LTL2TGBA -T -k "`$lcdir/LTLcounterLinear.pl $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.lacim + +echo "# now run 'gnuplot plot.gnu'" diff --git a/configure.ac b/configure.ac index feca4f438..20db33393 100644 --- a/configure.ac +++ b/configure.ac @@ -75,6 +75,8 @@ AC_CONFIG_FILES([ bench/emptchk/defs bench/gspn-ssp/Makefile bench/gspn-ssp/defs + bench/ltlcounter/Makefile + bench/ltlcounter/defs bench/ltl2tgba/Makefile bench/ltl2tgba/defs bench/scc-stats/Makefile