Preliminary benchmark using genltl, introduced earlier.

* bench/ltlclasses/: New benchmark.
* bench/Makefile.am: Add it.
* configure.ac: Adjust.

ChangeLog

+2010-12-04  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Preliminary benchmark using genltl, introduced earlier.
+
+	* bench/ltlclasses/: New benchmark.
+	* bench/Makefile.am: Add it.
+	* configure.ac: Adjust.
+
 2010-12-04  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	* src/ltlvisit/syntimpl.cc: Reduce the number of dynamic_cast<>s.

bench/Makefile.am

-## 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

bench/ltlclasses/.gitignore

+defs
+out
+result*.fm

bench/ltlclasses/Makefile.am

+# 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

bench/ltlclasses/README

+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},
+}
+
+

bench/ltlclasses/defs.in

+# -*- shell-script -*-
+# Copyright (C) 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
+# dpartement Systmes Rpartis Coopratifs (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

bench/ltlclasses/plot.gnu

+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"
+

bench/ltlclasses/run

+#!/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'"

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