diff --git a/ChangeLog b/ChangeLog index 5155907e8..d043e9d13 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2005-01-28 Denis Poitrenaud + + * src/tgbatest/dfs.test, src/tgbatest/emptchk.test, + src/tgbatest/emptchke.test, src/tgbatest/ltl2tgba.cc, + src/tgbatest/randtgba.cc, src/tgbatest/tba_samples_from_spin.test: + Adjust names of emptiness check algorithms. + 2005-01-27 Denis Poitrenaud * src/tgbaalgos/gtec/gtec.cc: Adjust statistics count to match diff --git a/src/tgbatest/dfs.test b/src/tgbatest/dfs.test index e3cf62d41..e6897add1 100755 --- a/src/tgbatest/dfs.test +++ b/src/tgbatest/dfs.test @@ -77,8 +77,8 @@ s9, s8,,; s9, s9,,; EOF -run 0 ./ltl2tgba -emagic_search -X blue_counter -run 0 ./ltl2tgba -ese05_search -X blue_counter +run 0 ./ltl2tgba -eSE05 -X blue_counter +run 0 ./ltl2tgba -eTau03_opt -X blue_counter # s1->s2->s3->(large composant from s4 to s9) # ^ || @@ -129,8 +129,8 @@ s9, s8,,; s9, s9,,; EOF -run 0 ./ltl2tgba -emagic_search -X blue_last -run 0 ./ltl2tgba -ese05_search -X blue_last +run 0 ./ltl2tgba -eSE05 -X blue_last +run 0 ./ltl2tgba -eTau03_opt -X blue_last # _______ # | | @@ -185,7 +185,7 @@ s9, s8,,; s9, s9,,; EOF -run 0 ./ltl2tgba -emagic_search -X red -run 0 ./ltl2tgba -ese05_search -X red +run 0 ./ltl2tgba -eSE05 -X red +run 0 ./ltl2tgba -eTau03_opt -X red rm -f red blue_counter blue_last \ No newline at end of file diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test index f2ab1e2a3..a1df1b2e3 100755 --- a/src/tgbatest/emptchk.test +++ b/src/tgbatest/emptchk.test @@ -37,23 +37,23 @@ expect_ce() expect_ce_do -e -D "$1" expect_ce_do -e -f "$1" expect_ce_do -e -f -D "$1" - expect_ce_do -ecouvreur99_shy "$1" - expect_ce_do -ecouvreur99_shy -D "$1" - expect_ce_do -ecouvreur99_shy -f "$1" - expect_ce_do -ecouvreur99_shy -f -D "$1" - expect_ce_do -emagic_search "$1" - expect_ce_do -emagic_search -f "$1" - run 0 ./ltl2tgba -ebsh_magic_search "$1" - run 0 ./ltl2tgba -ebsh_magic_search -f "$1" - run 0 ./ltl2tgba -ese05_search "$1" - run 0 ./ltl2tgba -ese05_search -f "$1" - run 0 ./ltl2tgba -ebsh_se05_search "$1" - run 0 ./ltl2tgba -ebsh_se05_search -f "$1" - run 0 ./ltl2tgba -etau03_opt_search -f "$1" - run 0 ./ltl2tgba -egv04 -f "$1" + expect_ce_do -eCou99_shy "$1" + expect_ce_do -eCou99_shy -D "$1" + expect_ce_do -eCou99_shy -f "$1" + expect_ce_do -eCou99_shy -f -D "$1" + expect_ce_do -eCVWY90 "$1" + expect_ce_do -eCVWY90 -f "$1" + run 0 ./ltl2tgba -eCVWY90_bsh "$1" + run 0 ./ltl2tgba -eCVWY90_bsh -f "$1" + run 0 ./ltl2tgba -eSE05 "$1" + run 0 ./ltl2tgba -eSE05 -f "$1" + run 0 ./ltl2tgba -eSE05_bsh "$1" + run 0 ./ltl2tgba -eSE05_bsh -f "$1" + run 0 ./ltl2tgba -eTau03_opt -f "$1" + run 0 ./ltl2tgba -eGV04 -f "$1" # Expect multiple accepting runs - test `./ltl2tgba -emagic_search_repeated "$1" | grep Prefix: | wc -l` -ge $2 - test `./ltl2tgba -ese05_search_repeated "$1" | grep Prefix: | wc -l` -ge $2 + test `./ltl2tgba -eCVWY90_repeated "$1" | grep Prefix: | wc -l` -ge $2 + test `./ltl2tgba -eSE05_repeated "$1" | grep Prefix: | wc -l` -ge $2 } expect_no() @@ -62,23 +62,23 @@ expect_no() run 0 ./ltl2tgba -E -D "$1" run 0 ./ltl2tgba -E -f "$1" run 0 ./ltl2tgba -E -f -D "$1" - run 0 ./ltl2tgba -Ecouvreur99_shy "$1" - run 0 ./ltl2tgba -Ecouvreur99_shy -D "$1" - run 0 ./ltl2tgba -Ecouvreur99_shy -f "$1" - run 0 ./ltl2tgba -Ecouvreur99_shy -f -D "$1" - run 0 ./ltl2tgba -Emagic_search "$1" - run 0 ./ltl2tgba -Emagic_search -f "$1" - run 0 ./ltl2tgba -Ebsh_magic_search "$1" - run 0 ./ltl2tgba -Ebsh_magic_search -f "$1" - run 0 ./ltl2tgba -Ese05_search "$1" - run 0 ./ltl2tgba -Ese05_search -f "$1" - run 0 ./ltl2tgba -Ebsh_se05_search "$1" - run 0 ./ltl2tgba -Ebsh_se05_search -f "$1" - run 0 ./ltl2tgba -Etau03_opt_search -f "$1" - run 0 ./ltl2tgba -Egv04 -f "$1" - test `./ltl2tgba -emagic_search_repeated "!($1)" | + run 0 ./ltl2tgba -ECou99_shy "$1" + run 0 ./ltl2tgba -ECou99_shy -D "$1" + run 0 ./ltl2tgba -ECou99_shy -f "$1" + run 0 ./ltl2tgba -ECou99_shy -f -D "$1" + run 0 ./ltl2tgba -ECVWY90 "$1" + run 0 ./ltl2tgba -ECVWY90 -f "$1" + run 0 ./ltl2tgba -ECVWY90_bsh "$1" + run 0 ./ltl2tgba -ECVWY90_bsh -f "$1" + run 0 ./ltl2tgba -ESE05 "$1" + run 0 ./ltl2tgba -ESE05 -f "$1" + run 0 ./ltl2tgba -ESE05_bsh "$1" + run 0 ./ltl2tgba -ESE05_bsh -f "$1" + run 0 ./ltl2tgba -ETau03_opt -f "$1" + run 0 ./ltl2tgba -EGV04 -f "$1" + test `./ltl2tgba -eCVWY90_repeated "!($1)" | grep Prefix: | wc -l` -ge $2 - test `./ltl2tgba -ese05_search_repeated "!($1)" | + test `./ltl2tgba -eSE05_repeated "!($1)" | grep Prefix: | wc -l` -ge $2 } diff --git a/src/tgbatest/emptchke.test b/src/tgbatest/emptchke.test index 7eb3fe8cb..5503e6b59 100755 --- a/src/tgbatest/emptchke.test +++ b/src/tgbatest/emptchke.test @@ -29,9 +29,9 @@ expect_ce() { run 0 ./ltl2tgba -e -X "$1" run 0 ./ltl2tgba -e -D -X "$1" - run 0 ./ltl2tgba -ecouvreur99_shy -X "$1" - run 0 ./ltl2tgba -ecouvreur99_shy -D -X "$1" - run 0 ./ltl2tgba -emagic_search -X "$1" + run 0 ./ltl2tgba -eCou99_shy -X "$1" + run 0 ./ltl2tgba -eCou99_shy -D -X "$1" + run 0 ./ltl2tgba -eCVWY90 -X "$1" } cat >input <<'EOF' diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index e22e1d01b..cf6854e71 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -133,24 +133,24 @@ syntax(char* prog) << "(implies -f)" << std::endl << std::endl << "Where ALGO should be one of:" << std::endl - << " couvreur99 (the default)" << std::endl - << " couvreur99_shy-" << std::endl - << " couvreur99_shy" << std::endl - << " magic_search" << std::endl - << " magic_search_repeated" << std::endl - << " bsh_magic_search[(heap size in Mo - 10Mo by default)]" + << " Cou99 (the default)" << std::endl + << " Cou99_shy-" << std::endl + << " Cou99_shy" << std::endl + << " CVWY90" << std::endl + << " CVWY90_repeated" << std::endl + << " CVWY90_bsh[(heap size in Mo - 10Mo by default)]" << std::endl - << " bsh_magic_search_repeated[(heap size in MB - 10MB" + << " CVWY90_bsh_repeated[(heap size in MB - 10MB" << " by default)]" << std::endl - << " gv04" << std::endl - << " se05_search" << std::endl - << " se05_search_repeated" << std::endl - << " bsh_se05_search[(heap size in MB - 10MB by default)]" + << " GV04" << std::endl + << " SE05" << std::endl + << " SE05_repeated" << std::endl + << " SE05_bsh[(heap size in MB - 10MB by default)]" << std::endl - << " bsh_se05_search_repeated[(heap size in MB - 10MB" + << " SE05_bsh_repeated[(heap size in MB - 10MB" << " by default)]" << std::endl - << " tau03_search" << std::endl - << " tau03_opt_search" << std::endl; + << " Tau03" << std::endl + << " Tau03_opt" << std::endl; exit(2); } @@ -241,7 +241,7 @@ main(int argc, char** argv) echeck_algo = argv[formula_index] + 2; } else - echeck_algo = "couvreur99"; + echeck_algo = "Cou99"; expect_counter_example = true; output = -1; } @@ -255,7 +255,7 @@ main(int argc, char** argv) echeck_algo = argv[formula_index] + 2; } else - echeck_algo = "couvreur99"; + echeck_algo = "Cou99"; expect_counter_example = false; output = -1; } @@ -412,77 +412,77 @@ main(int argc, char** argv) if (echeck_algo != "") { - if (echeck_algo == "couvreur99") + if (echeck_algo == "Cou99") { echeck = Couvreur; } - else if (echeck_algo == "couvreur99_shy") + else if (echeck_algo == "Cou99_shy") { echeck = Couvreur2; couv_group = true; } - else if (echeck_algo == "couvreur99_shy-") + else if (echeck_algo == "Cou99_shy-") { echeck = Couvreur2; couv_group = false; } - else if (echeck_algo == "magic_search") + else if (echeck_algo == "CVWY90") { echeck = MagicSearch; degeneralize_maybe = true; } - else if (echeck_algo == "magic_search_repeated") + else if (echeck_algo == "CVWY90_repeated") { echeck = MagicSearch; degeneralize_maybe = true; search_many = true; } - else if (echeck_algo == "bsh_magic_search") + else if (echeck_algo == "CVWY90_bsh") { echeck = MagicSearch; degeneralize_maybe = true; bit_state_hashing = true; } - else if (echeck_algo == "bsh_magic_search_repeated") + else if (echeck_algo == "CVWY90_bsh_repeated") { echeck = MagicSearch; degeneralize_maybe = true; bit_state_hashing = true; search_many = true; } - else if (echeck_algo == "se05_search") + else if (echeck_algo == "SE05") { echeck = Se05Search; degeneralize_maybe = true; } - else if (echeck_algo == "se05_search_repeated") + else if (echeck_algo == "SE05_repeated") { echeck = Se05Search; degeneralize_maybe = true; search_many = true; } - else if (echeck_algo == "bsh_se05_search") + else if (echeck_algo == "SE05_bsh") { echeck = Se05Search; degeneralize_maybe = true; bit_state_hashing = true; } - else if (echeck_algo == "bsh_se05_search_repeated") + else if (echeck_algo == "SE05_bsh_repeated") { echeck = Se05Search; degeneralize_maybe = true; bit_state_hashing = true; search_many = true; } - else if (echeck_algo == "tau03_search") + else if (echeck_algo == "Tau03") { echeck = Tau03Search; } - else if (echeck_algo == "tau03_opt_search") + else if (echeck_algo == "Tau03_opt") { echeck = Tau03OptSearch; } - else if (echeck_algo == "gv04") + else if (echeck_algo == "GV04") { echeck = Gv04; degeneralize_maybe = true; @@ -753,7 +753,7 @@ main(int argc, char** argv) if (a->number_of_acceptance_conditions() == 0) { if (!paper_opt) - std::cout << "To apply tau03_search, the automaton must have at" + std::cout << "To apply Tau03, the automaton must have at" << " least one accepting condition. Try with another" << " algorithm." << std::endl; else diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 2874c1038..0a6748069 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -103,16 +103,16 @@ struct ec_algo ec_algo ec_algos[] = { - { "couvreur99", couvreur99_cons, 0, -1U, true }, - { "couvreur99_shy-", couvreur99_shy_minus_cons, 0, -1U, true }, - { "couvreur99_shy", couvreur99_shy_cons, 0, -1U, true }, - { "explicit_magic_search", spot::explicit_magic_search, 0, 1, true }, - { "bsh_magic_search", bsh_ms_cons, 0, 1, false }, - { "explicit_se05", spot::explicit_se05_search, 0, 1, true }, - { "bsh_se05", bsh_se05_cons, 0, 1, false }, - { "explicit_gv04", spot::explicit_gv04_check, 0, 1, true }, - { "explicit_tau03", spot::explicit_tau03_search, 1, -1U, true }, - { "explicit_tau03_opt", spot::explicit_tau03_opt_search, 0, -1U, true }, + { "Cou99", couvreur99_cons, 0, -1U, true }, + { "Cou99_shy-", couvreur99_shy_minus_cons, 0, -1U, true }, + { "Cou99_shy", couvreur99_shy_cons, 0, -1U, true }, + { "CVWY90", spot::explicit_magic_search, 0, 1, true }, + { "CVWY90_bsh", bsh_ms_cons, 0, 1, false }, + { "GV04", spot::explicit_gv04_check, 0, 1, true }, + { "SE05", spot::explicit_se05_search, 0, 1, true }, + { "SE05_bsh", bsh_se05_cons, 0, 1, false }, + { "Tau03", spot::explicit_tau03_search, 1, -1U, true }, + { "Tau03_opt", spot::explicit_tau03_opt_search, 0, -1U, true }, }; spot::emptiness_check* diff --git a/src/tgbatest/tba_samples_from_spin.test b/src/tgbatest/tba_samples_from_spin.test index 27c82728c..ccc255925 100755 --- a/src/tgbatest/tba_samples_from_spin.test +++ b/src/tgbatest/tba_samples_from_spin.test @@ -27,25 +27,25 @@ set -e expect_ce() { ./ltl2tgba -X -e "$1" - ./ltl2tgba -X -ecouvreur99_shy "$1" - ./ltl2tgba -X -emagic_search "$1" - ./ltl2tgba -X -ebsh_magic_search "$1" - ./ltl2tgba -X -ese05_search "$1" - ./ltl2tgba -X -ebsh_se05_search "$1" - ./ltl2tgba -X -etau03_search "$1" - ./ltl2tgba -X -etau03_opt_search "$1" + ./ltl2tgba -X -eCou99_shy "$1" + ./ltl2tgba -X -eCVWY90 "$1" + ./ltl2tgba -X -eCVWY90_bsh "$1" + ./ltl2tgba -X -eSE05 "$1" + ./ltl2tgba -X -eSE05_bsh "$1" + ./ltl2tgba -X -eTau03 "$1" + ./ltl2tgba -X -eTau03_opt "$1" } expect_no() { ./ltl2tgba -X -E "$1" - ./ltl2tgba -X -Ecouvreur99_shy "$1" - ./ltl2tgba -X -Emagic_search "$1" - ./ltl2tgba -X -Ebsh_magic_search "$1" - ./ltl2tgba -X -Ese05_search "$1" - ./ltl2tgba -X -Ebsh_se05_search "$1" - ./ltl2tgba -X -Etau03_search "$1" - ./ltl2tgba -X -Etau03_opt_search "$1" + ./ltl2tgba -X -ECou99_shy "$1" + ./ltl2tgba -X -ECVWY90 "$1" + ./ltl2tgba -X -ECVWY90_bsh "$1" + ./ltl2tgba -X -ESE05 "$1" + ./ltl2tgba -X -ESE05_bsh "$1" + ./ltl2tgba -X -ETau03 "$1" + ./ltl2tgba -X -ETau03_opt "$1" } dir=$srcdir/tba_samples_from_spin