From 49b871f924de0682aea4b076f1fb0b53f551fa92 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 16 Nov 2004 00:35:18 +0000 Subject: [PATCH] * src/tgbatest/ltl2tgba.cc (main): For non-generalized emptiness check, degeneralize the automaton only if it has too much acceptance conditions. This makes it easier to reproduce runs of randtgba. * src/tgbatest/emptchk.test: Adjust. --- ChangeLog | 8 ++++++++ src/tgbatest/emptchk.test | 8 ++++---- src/tgbatest/ltl2tgba.cc | 41 ++++++++++++++++++--------------------- 3 files changed, 31 insertions(+), 26 deletions(-) diff --git a/ChangeLog b/ChangeLog index a4b751221..1d5ce802a 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,11 @@ +2004-11-15 Alexandre Duret-Lutz + + * src/tgbatest/ltl2tgba.cc (main): For non-generalized emptiness + check, degeneralize the automaton only if it has too much + acceptance conditions. This makes it easier to reproduce runs + of randtgba. + * src/tgbatest/emptchk.test: Adjust. + 2004-11-15 Poitrenaud Denis * src/tgbaalgos/magic.cc: Fix a stupid bug. diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test index 940e6efb1..8efdc65a6 100755 --- a/src/tgbatest/emptchk.test +++ b/src/tgbatest/emptchk.test @@ -72,14 +72,14 @@ expect_no() run 0 ./ltl2tgba -Ese05_search -f "$1" run 0 ./ltl2tgba -Ebsh_se05_search "$1" run 0 ./ltl2tgba -Ebsh_se05_search -f "$1" - test `./ltl2tgba -emagic_search_repeated "!($1)" | + test `./ltl2tgba -emagic_search_repeated "!($1)" | grep Prefix: | wc -l` -ge $2 - test `./ltl2tgba -ese05_search_repeated "!($1)" | + test `./ltl2tgba -ese05_search_repeated "!($1)" | grep Prefix: | wc -l` -ge $2 } expect_ce 'a' 1 -expect_ce 'a U b' 2 +expect_ce 'a U b' 1 expect_ce 'X a' 1 expect_ce 'a & b & c' 1 expect_ce 'a | b | (c U (d & (g U (h ^ i))))' 2 @@ -90,4 +90,4 @@ expect_ce 'Fc & X(a | Xb) & GF(a | Xb) & Gc' 1 expect_ce '!((FF a) <=> (F x))' 3 expect_no '!((FF a) <=> (F a))' 4 expect_no 'Xa && (!a U b) && !b && X!b' 5 -expect_no '(a U !b) && Gb' 4 +expect_no '(a U !b) && Gb' 3 diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index da7fb8cc7..f55993f0b 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -135,6 +135,7 @@ main(int argc, char** argv) bool debug_opt = false; bool degeneralize_opt = false; + bool degeneralize_maybe = false; bool fm_opt = false; bool fm_exprop_opt = false; bool fm_symb_merge_opt = true; @@ -356,48 +357,48 @@ main(int argc, char** argv) else if (echeck_algo == "magic_search") { echeck = MagicSearch; - degeneralize_opt = true; + degeneralize_maybe = true; } else if (echeck_algo == "magic_search_repeated") { echeck = MagicSearch; - degeneralize_opt = true; + degeneralize_maybe = true; magic_many = true; } else if (echeck_algo == "bsh_magic_search") { echeck = MagicSearch; - degeneralize_opt = true; + degeneralize_maybe = true; bit_state_hashing = true; } else if (echeck_algo == "bsh_magic_search_repeated") { echeck = MagicSearch; - degeneralize_opt = true; + degeneralize_maybe = true; bit_state_hashing = true; magic_many = true; } else if (echeck_algo == "se05_search") { echeck = Se05Search; - degeneralize_opt = true; + degeneralize_maybe = true; } else if (echeck_algo == "se05_search_repeated") { echeck = Se05Search; - degeneralize_opt = true; + degeneralize_maybe = true; magic_many = true; } else if (echeck_algo == "bsh_se05_search") { echeck = Se05Search; - degeneralize_opt = true; + degeneralize_maybe = true; bit_state_hashing = true; } else if (echeck_algo == "bsh_se05_search_repeated") { echeck = Se05Search; - degeneralize_opt = true; + degeneralize_maybe = true; bit_state_hashing = true; magic_many = true; } @@ -492,6 +493,9 @@ main(int argc, char** argv) } spot::tgba_tba_proxy* degeneralized = 0; + + if (degeneralize_maybe && a->number_of_acceptance_conditions() > 1) + degeneralize_opt = true; if (degeneralize_opt) a = degeneralized = new spot::tgba_tba_proxy(a); @@ -605,37 +609,31 @@ main(int argc, char** argv) } spot::emptiness_check* ec = 0; - spot::tgba* ec_a = 0; switch (echeck) { case None: break; case Couvreur: - ec_a = a; ec = new spot::couvreur99_check(a); break; case Couvreur2: - ec_a = a; ec = new spot::couvreur99_check_shy(a); break; case MagicSearch: - ec_a = degeneralized; if (bit_state_hashing) - ec = spot::bit_state_hashing_magic_search( - degeneralized, heap_size); + ec = spot::bit_state_hashing_magic_search(a, heap_size); else - ec = spot::explicit_magic_search(degeneralized); + ec = spot::explicit_magic_search(a); break; case Se05Search: - ec_a = degeneralized; if (bit_state_hashing) - ec = spot::bit_state_hashing_se05_search(degeneralized, heap_size); + ec = spot::bit_state_hashing_se05_search(a, heap_size); else - ec = spot::explicit_se05_search(degeneralized); + ec = spot::explicit_se05_search(a); break; } @@ -677,13 +675,12 @@ main(int argc, char** argv) if (graph_run_opt) { spot::tgba_run_dotty_decorator deco(run); - spot::dotty_reachable(std::cout, ec_a, &deco); + spot::dotty_reachable(std::cout, a, &deco); } else { - spot::print_tgba_run(std::cout, ec_a, run); - if (!spot::replay_tgba_run(std::cout, ec_a, run, - true)) + spot::print_tgba_run(std::cout, a, run); + if (!spot::replay_tgba_run(std::cout, a, run, true)) exit_code = 1; } delete run;