From a4b6faba202089eda568baa2376226a31b2f2741 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 23 Jan 2015 11:38:10 +0100 Subject: [PATCH] ltl2tgba.html: Adjust for ltl3ba 1.1.0 ltl3ba 1.1.0 was released today * wrap/python/ajax/spot.in: Use -T3 instead of -U. * wrap/python/ajax/README: Adjust version. * wrap/python/ajax/ltl2tgba.html: Turn on improved determinism of ltl3ba by default. * bench/ltl2tgba/tools, bench/spin13/run.sh: Adjust options. * bench/spin13/README: Mention the update. --- bench/ltl2tgba/tools | 10 +++++----- bench/spin13/README | 5 ++++- bench/spin13/run.sh | 20 ++++++++++---------- wrap/python/ajax/README | 4 ++-- wrap/python/ajax/ltl2tgba.html | 2 +- wrap/python/ajax/spot.in | 16 +++++++++++----- 6 files changed, 33 insertions(+), 24 deletions(-) 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