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

@@ -1,3 +1,14 @@
+2009-11-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	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  <adl@lrde.epita.fr>
 
 	Use a timer to clock the different phases of the translation.
@@ -168,7 +179,7 @@
 
 2009-11-04  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
-	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'.

THANKS

@@ -4,4 +4,5 @@ suggestions.
 Heikki Tauriainen
 Jean-Michel Couvreur
 Jean-Michel Ilié
+Kristin Y. Rozier
 Yann Thierry-Mieg

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

bench/ltlcounter/.gitignore

@@ -0,0 +1,3 @@
+*.eps
+results*
+defs

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

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.

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

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"

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

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