diff --git a/bench/ltl2tgba/tools b/bench/ltl2tgba/tools index 5448b3a33..6d9a518de 100644 --- a/bench/ltl2tgba/tools +++ b/bench/ltl2tgba/tools @@ -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-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" +test -n "$LTL3BA" && set "$@" "{ltl3ba-M0S0} $LTL3BA -M0 -S0 -f %s >%N" \ + "{ltl3ba-M1S0} $LTL3BA -M1 -S0 -f %s >%N" \ + "{ltl3ba-M0S2} $LTL3BA -M0 -S2 -f %s >%N" \ + "{ltl3ba-M1S2} $LTL3BA -M1 -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 d85492025..47d4fe249 100644 --- a/bench/spin13/README +++ b/bench/spin13/README @@ -19,9 +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). +The benchmark has been updated to use ltl3ba 1.1.1 released on +2014-01-24 (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 eef34d598..13f0870a9 100755 --- a/bench/spin13/run.sh +++ b/bench/spin13/run.sh @@ -69,8 +69,8 @@ if test $# = 2; then # Deter $ba && set "$@" \ - ": LTL3BA NoSim NoSusp Deter; ltl3ba -S0 -A -M -f %s >%N" \ - ": LTL3BA Sim NoSusp Deter; ltl3ba -S2 -A -M -f %s >%N" \ + ": LTL3BA NoSim NoSusp Deter; ltl3ba -S0 -A -M1 -f %s >%N" \ + ": LTL3BA Sim NoSusp Deter; ltl3ba -S2 -A -M1 -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 -S0 -M -f %s >%N" \ - ": LTL3BA Sim Susp Deter; ltl3ba -S2 -M -f %s >%N" + ": LTL3BA NoSim Susp Deter; ltl3ba -S0 -M1 -f %s >%N" \ + ": LTL3BA Sim Susp Deter; ltl3ba -S2 -M1 -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 -S0 -L -A -f %s >%N" \ - ": LTL3BA Sim NoSusp; ltl3ba -S2 -L -A -f %s >%N" \ + ": LTL3BA NoSim NoSusp; ltl3ba -S0 -M0 -A -f %s >%N" \ + ": LTL3BA Sim NoSusp; ltl3ba -S2 -M0 -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 -S0 -L -f %s >%N" \ - ": LTL3BA Sim Susp; ltl3ba -S2 -L -f %s >%N" + ": LTL3BA NoSim Susp; ltl3ba -S0 -M0 -f %s >%N" \ + ": LTL3BA Sim Susp; ltl3ba -S2 -M0 -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/doc/org/ltlcross.org b/doc/org/ltlcross.org index 1442fb36a..9f5fe901d 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -1,3 +1,4 @@ +# -*- coding: utf-8 -*- #+TITLE: =ltlcross= #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html @@ -125,8 +126,8 @@ tools: - '=spin -f %s >%N=' - '=ltl2ba -f %s >%N=' - - '=ltl3ba -S -f %s >%N=' - - '=ltl3ba -S -M -f %s >%N=' (more deterministic output) + - '=ltl3ba -M0 -f %s >%N=' (less deterministic output, can be smaller) + - '=ltl3ba -M1 -f %s >%N=' (more deterministic output) - '=modella -r12 -g -e %L %T=' - '=/path/to/script4lbtt.py %L %T=' (script supplied by [[http://www.ti.informatik.uni-kiel.de/~fritz/][ltl2nba]] for its interface with LBTT) diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in index 303391adc..db493aace 100755 --- a/wrap/python/ajax/spot.in +++ b/wrap/python/ajax/spot.in @@ -364,11 +364,15 @@ if output_type == 'v': if output_type == 'v3': import subprocess try: - # -L is new in 1.1.0, and older versions will complain about it. - l3proc = subprocess.Popen(['@LTL3BA@', '-L', '-v'], - stdout=subprocess.PIPE) + l3proc = subprocess.Popen(['@LTL3BA@', '-v'], stdout=subprocess.PIPE) (ver, err) = l3proc.communicate() - err = l3proc.returncode + # -M[0|1] is new in 1.1.1, and we use it. + l3proc = subprocess.Popen(['@LTL3BA@', '-h'], stdout=subprocess.PIPE) + (out, err) = l3proc.communicate() + if out.find('-M[') < 0: + err = 1 + else: + err = 0 except: err = 1 if err != 0: @@ -542,8 +546,8 @@ elif translator == 'ta': elif translator == 'l3': l3out = '-T' # 1.0.1 had determinization and simulation turned off by default, - # we need -L and -S0 with 1.1.0 for the same effect - l3opt = { '-l', '-P', '-A', '-c', '-C', '-o', '-p', '-L', '-S0' } + # we need -M0 and -S0 with 1.1.1 for the same effect + l3opt = { '-l', '-P', '-A', '-c', '-C', '-o', '-p', '-M0', '-S0' } for lo in form.getfirst('lo', 'T'): if lo == 'U': l3out = '-T3' # was -U in ltl3ba 1.0.1, now -T3 since 1.1.0 @@ -559,8 +563,8 @@ elif translator == 'l3': l3opt.remove('-C') l3opt.remove('-c') elif l3 == 'M': - l3opt.remove('-L') - l3opt.add('-M') + l3opt.remove('-M0') + l3opt.add('-M1') elif l3 == 'S': l3opt.remove('-S0') l3opt.add('-S2') # was -S in 1.0.1