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

Make Couvreur/FM the default translation.

Browse source 
* src/tgbatest/ltl2tgba.cc (syntax, main): Do it.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2010-01-30 11:20:27 +01:00
parent 369e4c419b
commit 55b693e123
4 changed files with 15 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

8
ChangeLog
View file

@ -1,3 +1,11 @@
2010-01-30 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Make Couvreur/FM the default translation.
* src/tgbatest/ltl2tgba.cc (syntax, main): Do it.
* NEWS: Mention it.
* src/tgbatest/emptchk.test: Add missing -l.
2010-01-30 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2010-01-30 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Overhaul LaCIM's ELTL options. Overhaul LaCIM's ELTL options.

2
NEWS
View file

@ -33,7 +33,7 @@ New in spot 0.5 (2010-01-31):
step will produce a generalized automaton in the end. step will produce a generalized automaton in the end.
* ltl2tgba has gained several options and the help text has been * ltl2tgba has gained several options and the help text has been
reorganized. Please run src/tgbatest/ltl2tgba without arguments reorganized. Please run src/tgbatest/ltl2tgba without arguments
for details. for details. Couvreur/FM is now the default translation.
* Automata using BDD-encoded transitions relation can now be pruned * Automata using BDD-encoded transitions relation can now be pruned
for useless states symbolically using the delete_unaccepting_scc() for useless states symbolically using the delete_unaccepting_scc()
function. This is ltl2tgba's -R3b option. function. This is ltl2tgba's -R3b option.

8
src/tgbatest/emptchk.test
View file

@ -54,8 +54,8 @@ expect_ce()
run 0 ../ltl2tgba -eTau03_opt -f "$1" run 0 ../ltl2tgba -eTau03_opt -f "$1"
run 0 ../ltl2tgba -eGV04 -f "$1" run 0 ../ltl2tgba -eGV04 -f "$1"
# Expect multiple accepting runs # Expect multiple accepting runs
test `../ltl2tgba -e'CVWY90(repeated)' "$1" | grep Prefix: | wc -l` -ge $2 test `../ltl2tgba -e'CVWY90(repeated)' -l "$1" | grep Prefix: | wc -l` -ge $2
test `../ltl2tgba -e'SE05(repeated)' "$1" | grep Prefix: | wc -l` -ge $2 test `../ltl2tgba -e'SE05(repeated)' -l "$1" | grep Prefix: | wc -l` -ge $2
} }
expect_no() expect_no()
@ -78,9 +78,9 @@ expect_no()
run 0 ../ltl2tgba -E'SE05(bsh=10M)' -f "$1" run 0 ../ltl2tgba -E'SE05(bsh=10M)' -f "$1"
run 0 ../ltl2tgba -ETau03_opt -f "$1" run 0 ../ltl2tgba -ETau03_opt -f "$1"
run 0 ../ltl2tgba -EGV04 -f "$1" run 0 ../ltl2tgba -EGV04 -f "$1"
test `../ltl2tgba -e'CVWY90(repeated)' "!($1)" | test `../ltl2tgba -e'CVWY90(repeated)' -l "!($1)" |
grep Prefix: | wc -l` -ge $2 grep Prefix: | wc -l` -ge $2
test `../ltl2tgba -e'SE05(repeated)' "!($1)" | test `../ltl2tgba -e'SE05(repeated)' -l "!($1)" |
grep Prefix: | wc -l` -ge $2 grep Prefix: | wc -l` -ge $2
} }

4
src/tgbatest/ltl2tgba.cc
View file

@ -110,9 +110,9 @@ syntax(char* prog)
<< "Translation algorithm:" << std::endl << "Translation algorithm:" << std::endl
<< " -f use Couvreur's FM algorithm for LTL" << " -f use Couvreur's FM algorithm for LTL"
<< "(default)"
<< std::endl << std::endl
<< " -l use Couvreur's LaCIM algorithm for LTL " << " -l use Couvreur's LaCIM algorithm for LTL "
<< "(default)"
<< std::endl << std::endl
<< " -le use Couvreur's LaCIM algorithm for ELTL" << " -le use Couvreur's LaCIM algorithm for ELTL"
<< std::endl << std::endl
@ -268,7 +268,7 @@ main(int argc, char** argv)
enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen; enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
enum { TransitionLabeled, StateLabeled } labeling_opt = TransitionLabeled; enum { TransitionLabeled, StateLabeled } labeling_opt = TransitionLabeled;
enum { TransFM, TransLaCIM, TransLaCIM_ELTL, TransLaCIM_ELTL_ops, TransTAA } enum { TransFM, TransLaCIM, TransLaCIM_ELTL, TransLaCIM_ELTL_ops, TransTAA }
translation = TransLaCIM; translation = TransFM;
int fm_red = spot::ltl::Reduce_None; int fm_red = spot::ltl::Reduce_None;
bool fm_exprop_opt = false; bool fm_exprop_opt = false;
bool fm_symb_merge_opt = true; bool fm_symb_merge_opt = true;