From 019bdef8ff703d0537a46bd438d0e62f54d6da1b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 9 Jul 2004 12:54:08 +0000 Subject: [PATCH] * src/tgbatest/ltl2baw.pl: Do not use -T anymore. Fix comments. --- ChangeLog | 4 ++++ src/tgbatest/ltl2baw.pl | 19 +++++++------------ 2 files changed, 11 insertions(+), 12 deletions(-) diff --git a/ChangeLog b/ChangeLog index e10f41b99..9acfaa51a 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,7 @@ +2004-07-09 Alexandre Duret-Lutz + + * src/tgbatest/ltl2baw.pl: Do not use -T anymore. Fix comments. + 2004-07-08 Alexandre Duret-Lutz lbtt 1.1.0 supports TGBAs, use that and remove old workarounds. diff --git a/src/tgbatest/ltl2baw.pl b/src/tgbatest/ltl2baw.pl index 774da9e36..ae2d4be98 100755 --- a/src/tgbatest/ltl2baw.pl +++ b/src/tgbatest/ltl2baw.pl @@ -27,9 +27,9 @@ # This script converts the intermediate generalized automata computed # by ltl2ba into a form usable by lbtt. This is useful for statistics. # -# It can also be used to simplify a formula using lbtt, and then hand -# the simplified formula over to spot. (At the time of writing, Spot -# is not yet able to simplify formulae.) +# It can also be used to simplify a formula using ltl2ba, and then hand +# the simplified formula over to spot. (This can be used to compare +# Spot's formulae simplification and ltl2ba's.) # # ltl2baw.pl --ltl2ba='options-A' options-B # run `ltl2ba options-B', extract the optimized generalized automata, @@ -39,17 +39,12 @@ # a form readable by lbtt. # # ltl2baw.pl options-B -# this is a shorthand for `ltl2baw.pl --ltl2ba=-T options-B', -# i.e., this creates an lbtt automata whose size is the same as -# the size of the one produced by ltl2ba (module the initial -# state, see below), whose product with the system will have -# the same size, but without acceptance conditions. I.e., the -# only use of this automata is making statistics. +# this is a shorthand for `ltl2baw.pl --ltl2ba=-t options-B', # e.g., ltl2baw.pl -f 'a U b' # # ltl2baw.pl --spot='options-A' options-B -# run `ltl2ba options-B', extract the optimized generalized automata, -# and pass this automata to `ltl2tgba options-A'. +# run `ltl2ba options-B', extract the simplified formula +# and pass this formula to `ltl2tgba options-A'. # e.g., ltl2baw.pl ---spot=-f -f '(a U b) <-> true' # will use the Couvreur/FM algorithm to translate the formula # simplified by ltl2ba @@ -93,7 +88,7 @@ elsif ($arg =~ '--spot=(.*)$') } else { - open(LTL2TGBA, "| ./ltl2tgba -T -X -"); + open(LTL2TGBA, "| ./ltl2tgba -t -X -"); } END {