diff --git a/bench/ltl2tgba/tools b/bench/ltl2tgba/tools
index b00ff73fa..5448b3a33 100644
--- a/bench/ltl2tgba/tools
+++ b/bench/ltl2tgba/tools
@@ -1,5 +1,5 @@
## -*- coding: utf-8; mode: sh -*-
-## Copyright (C) 2013 Laboratoire de Recherche et Développement de
+## Copyright (C) 2013, 2015 Laboratoire de Recherche et Développement de
## l'Epita (LRDE).
##
## This file is part of Spot, a model checking library.
@@ -27,10 +27,10 @@ set dummy
# Add third-party tools if they are available.
test -n "$SPIN" && set "$@" "{spin} $SPIN -f %s >%N"
test -n "$LTL2BA" && set "$@" "{ltl2ba} $LTL2BA -f %s >%N"
-test -n "$LTL3BA" && set "$@" "{ltl3ba} $LTL3BA -f %s >%N" \
- "{ltl3ba-M} $LTL3BA -M -f %s >%N" \
- "{ltl3ba-S} $LTL3BA -S -f %s >%N" \
- "{ltl3ba-SM} $LTL3BA -S -M -f %s >%N"
+test -n "$LTL3BA" && set "$@" "{ltl3ba-LS0} $LTL3BA -L -S0 -f %s >%N" \
+ "{ltl3ba-MS0} $LTL3BA -M -S0 -f %s >%N" \
+ "{ltl3ba-LS2} $LTL3BA -L -S2 -f %s >%N" \
+ "{ltl3ba-MS2} $LTL3BA -M -S2 -f %s >%N"
# Use -s to output a neverclaim, like the other tools.
set "$@" \
diff --git a/bench/spin13/README b/bench/spin13/README
index 86a0e6e8a..d85492025 100644
--- a/bench/spin13/README
+++ b/bench/spin13/README
@@ -6,7 +6,7 @@ This contains most of the a benchmark used for the paper
To appear in the proceedings of Spin'13.
-By "most" we means that some lines of the table we actually be missing
+By "most" we means that some lines of the table will actually be missing
because we cannot compute them with the current version of Spot. The
missing lines are those with a small "a", that use the old SCC-based
simplification, and not the new one which is presented in section 4.1
@@ -19,6 +19,9 @@ exactly the same versions (yes, that's a plural), please head over to
Keep in mind that as Spot is evolving, the results from this benchmark
may evolve (hopefully for the best!) with time.
+The benchmark has been updated to use ltl3ba 1.1.0 released on
+2014-01-23 (because the set of optimizations that are now activated
+by default is different).
Running instructions
====================
diff --git a/bench/spin13/run.sh b/bench/spin13/run.sh
index 4cc123186..eef34d598 100755
--- a/bench/spin13/run.sh
+++ b/bench/spin13/run.sh
@@ -1,7 +1,7 @@
#!/bin/sh
# -*- coding: utf-8 -*-
-# Copyright (C) 2013 Laboratoire de Recherche et Développement de
-# l'Epita (LRDE).
+# Copyright (C) 2013, 2015 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@@ -69,8 +69,8 @@ if test $# = 2; then
# Deter
$ba && set "$@" \
- ": LTL3BA NoSim NoSusp Deter; ltl3ba -A -M -f %s >%N" \
- ": LTL3BA Sim NoSusp Deter; ltl3ba -S -A -M -f %s >%N" \
+ ": LTL3BA NoSim NoSusp Deter; ltl3ba -S0 -A -M -f %s >%N" \
+ ": LTL3BA Sim NoSusp Deter; ltl3ba -S2 -A -M -f %s >%N" \
": Cou99 '(Ad)' Deter; $ltl2tgba $opt $nosim --deter -x !degen-reset,!degen-lcache %f"
set "$@" \
": Cou99 '(A${D})' Deter; $ltl2tgba $opt $nosim --deter %f"
@@ -81,8 +81,8 @@ if test $# = 2; then
": Cou99 '(AS${DB})' Deter; $ltl2tgba $opt --deter %f"
$ba && set "$@" \
": Cou99 '(ASdB)' Deter; $ltl2tgba $opt --deter -x !degen-reset,!degen-lcache %f" \
- ": LTL3BA NoSim Susp Deter; ltl3ba -M -f %s >%N" \
- ": LTL3BA Sim Susp Deter; ltl3ba -S -M -f %s >%N"
+ ": LTL3BA NoSim Susp Deter; ltl3ba -S0 -M -f %s >%N" \
+ ": LTL3BA Sim Susp Deter; ltl3ba -S2 -M -f %s >%N"
set "$@" \
": Comp '(A${D})' Deter; $ltl2tgba -x comp-susp,!skel-simul $opt $nosim --deter %f" \
": Comp '(A${D})' Deter Early; $ltl2tgba -x comp-susp,!skel-simul,early-susp $opt $nosim --deter %f"
@@ -96,8 +96,8 @@ if test $# = 2; then
# Small
$ba && set "$@" \
- ": LTL3BA NoSim NoSusp; ltl3ba -A -f %s >%N" \
- ": LTL3BA Sim NoSusp; ltl3ba -S -A -f %s >%N" \
+ ": LTL3BA NoSim NoSusp; ltl3ba -S0 -L -A -f %s >%N" \
+ ": LTL3BA Sim NoSusp; ltl3ba -S2 -L -A -f %s >%N" \
": Cou99 '(Ad)' Small; $ltl2tgba $opt $nosim --small -x !degen-reset,!degen-lcache %f"
set "$@" \
": Cou99 '(A${D})' Small; $ltl2tgba $opt $nosim --small %f"
@@ -108,8 +108,8 @@ if test $# = 2; then
": Cou99 '(AS${DB})' Small; $ltl2tgba $opt --small %f"
$ba && set "$@" \
": Cou99 '(ASdB)' Small; $ltl2tgba $opt --small -x !degen-reset,!degen-lcache %f" \
- ": LTL3BA NoSim Susp; ltl3ba -f %s >%N" \
- ": LTL3BA Sim Susp; ltl3ba -S -f %s >%N"
+ ": LTL3BA NoSim Susp; ltl3ba -S0 -L -f %s >%N" \
+ ": LTL3BA Sim Susp; ltl3ba -S2 -L -f %s >%N"
set "$@" \
": Comp '(A${D})' Small; $ltl2tgba -x comp-susp,!skel-wdba,!skel-simul $opt $nosim --small %f" \
": Comp '(A${D})' Small Early; $ltl2tgba -x comp-susp,!skel-wdba,!skel-simul,early-susp $opt $nosim --small %f"
diff --git a/wrap/python/ajax/README b/wrap/python/ajax/README
index 546cd5af5..7dab377d1 100644
--- a/wrap/python/ajax/README
+++ b/wrap/python/ajax/README
@@ -9,8 +9,8 @@ In both cases you should ensure that the command `dot', from the
GraphViz package, is in the PATH. configure should have picked it up.
The "ltl3ba" tab will only be enabled if ltl3ba is available (as
-checked by ./configure) and supports options -v/-U/-T (checked by the
-CGI script). These option were introduced into ltl3ba version 1.0.2.
+checked by ./configure) and supports options -v/-T/-T3 (checked by the
+CGI script). These option were introduced into ltl3ba version 1.1.0.
Standalone usage
diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html
index 765f5253f..e59c6e34c 100644
--- a/wrap/python/ajax/ltl2tgba.html
+++ b/wrap/python/ajax/ltl2tgba.html
@@ -642,7 +642,7 @@ an identifier: aUb is an atomic proposition, unlike
SCC simplifications