alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/tgbatest/ltl2baw.pl: Do not use -T anymore. Fix comments.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2004-07-09 12:54:08 +00:00
parent 3b85646638
commit 019bdef8ff
2 changed files with 11 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,3 +1,7 @@
2004-07-09 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbatest/ltl2baw.pl: Do not use -T anymore. Fix comments.
2004-07-08 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-07-08 Alexandre Duret-Lutz <adl@src.lip6.fr>
lbtt 1.1.0 supports TGBAs, use that and remove old workarounds. lbtt 1.1.0 supports TGBAs, use that and remove old workarounds.

19
src/tgbatest/ltl2baw.pl
View file

@ -27,9 +27,9 @@
# This script converts the intermediate generalized automata computed # This script converts the intermediate generalized automata computed
# by ltl2ba into a form usable by lbtt. This is useful for statistics. # 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 # It can also be used to simplify a formula using ltl2ba, and then hand
# the simplified formula over to spot. (At the time of writing, Spot # the simplified formula over to spot. (This can be used to compare
# is not yet able to simplify formulae.) # Spot's formulae simplification and ltl2ba's.)
# #
# ltl2baw.pl --ltl2ba='options-A' options-B # ltl2baw.pl --ltl2ba='options-A' options-B
# run `ltl2ba options-B', extract the optimized generalized automata, # run `ltl2ba options-B', extract the optimized generalized automata,
@ -39,17 +39,12 @@
# a form readable by lbtt. # a form readable by lbtt.
# #
# ltl2baw.pl options-B # ltl2baw.pl options-B
# this is a shorthand for `ltl2baw.pl --ltl2ba=-T 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.
# e.g., ltl2baw.pl -f 'a U b' # e.g., ltl2baw.pl -f 'a U b'
# #
# ltl2baw.pl --spot='options-A' options-B # ltl2baw.pl --spot='options-A' options-B
# run `ltl2ba options-B', extract the optimized generalized automata, # run `ltl2ba options-B', extract the simplified formula
# and pass this automata to `ltl2tgba options-A'. # and pass this formula to `ltl2tgba options-A'.
# e.g., ltl2baw.pl ---spot=-f -f '(a U b) <-> true' # e.g., ltl2baw.pl ---spot=-f -f '(a U b) <-> true'
# will use the Couvreur/FM algorithm to translate the formula # will use the Couvreur/FM algorithm to translate the formula
# simplified by ltl2ba # simplified by ltl2ba
@ -93,7 +88,7 @@ elsif ($arg =~ '--spot=(.*)$')
} }
else else
{ {
open(LTL2TGBA, "| ./ltl2tgba -T -X -"); open(LTL2TGBA, "| ./ltl2tgba -t -X -");
} }
END { END {