From 4654da9ab5240793e82c1417072fd9efe823be22 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 29 Oct 2004 13:15:01 +0000 Subject: [PATCH] * src/tgbatest/ltl2tgba.cc: Replace -e, -E, -m, -M, and -n by -eALGO and -EALGO to ease the addition of new algorithms. * src/tgbatest/emptchk.test, src/tgbatest/emptchke.test: Adjust. --- ChangeLog | 4 ++ src/tgbatest/emptchk.test | 29 +++++------ src/tgbatest/emptchke.test | 4 +- src/tgbatest/ltl2tgba.cc | 99 ++++++++++++++++++-------------------- 4 files changed, 68 insertions(+), 68 deletions(-) diff --git a/ChangeLog b/ChangeLog index df8c087de..7b8ecd1e4 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,9 @@ 2004-10-29 Alexandre Duret-Lutz + * src/tgbatest/ltl2tgba.cc: Replace -e, -E, -m, -M, and -n by + -eALGO and -EALGO to ease the addition of new algorithms. + * src/tgbatest/emptchk.test, src/tgbatest/emptchke.test: Adjust. + * src/misc/version.cc: Fix trailing whitespace. * src/sanity/style.test: Diagnose trailing whitespace. diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test index 1f0c38c70..b4136b09f 100755 --- a/src/tgbatest/emptchk.test +++ b/src/tgbatest/emptchk.test @@ -31,12 +31,12 @@ expect_ce() run 0 ./ltl2tgba -e -D "$1" run 0 ./ltl2tgba -e -f "$1" run 0 ./ltl2tgba -e -f -D "$1" - run 0 ./ltl2tgba -e2 "$1" - run 0 ./ltl2tgba -e2 -D "$1" - run 0 ./ltl2tgba -e2 -f "$1" - run 0 ./ltl2tgba -e2 -f -D "$1" - run 0 ./ltl2tgba -m "$1" - run 0 ./ltl2tgba -m -f "$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" } expect_no() @@ -45,12 +45,12 @@ expect_no() run 0 ./ltl2tgba -E -D "$1" run 0 ./ltl2tgba -E -f "$1" run 0 ./ltl2tgba -E -f -D "$1" - run 0 ./ltl2tgba -E2 "$1" - run 0 ./ltl2tgba -E2 -D "$1" - run 0 ./ltl2tgba -E2 -f "$1" - run 0 ./ltl2tgba -E2 -f -D "$1" - run 0 ./ltl2tgba -M "$1" - run 0 ./ltl2tgba -M -f "$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" } expect_ce 'a' @@ -67,5 +67,6 @@ expect_no '!((FF a) <=> (F a))' expect_no 'Xa && (!a U b) && !b && X!b' expect_no '(a U !b) && Gb' -# Expect at least four counter-examples. -test `./ltl2tgba -n 'FFx <=> Fx' | grep Prefix: | wc -l` -ge 4 +# Expect at least four accepting runs +test `./ltl2tgba -emagic_search_repeated 'FFx <=> Fx' | + grep Prefix: | wc -l` -ge 4 diff --git a/src/tgbatest/emptchke.test b/src/tgbatest/emptchke.test index 1aad5fd4c..cde39c2b4 100755 --- a/src/tgbatest/emptchke.test +++ b/src/tgbatest/emptchke.test @@ -33,5 +33,5 @@ s1, "s2", "a & !b", c d; EOF run 0 ./ltl2tgba -e -X input -run 0 ./ltl2tgba -e2 -X input -run 0 ./ltl2tgba -m -X input +run 0 ./ltl2tgba -ecouvreur99_shy -X input +run 0 ./ltl2tgba -emagic_search -X input diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 7952735b4..e4cc0f466 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -58,24 +58,13 @@ syntax(char* prog) << " -A same as -a, but as a set" << std::endl << " -d turn on traces during parsing" << std::endl << " -D degeneralize the automaton" << std::endl - << " -e emptiness-check (Couvreur), expect and compute " - << "a counter-example" << std::endl - << " -e2 emptiness-check (Couvreur variant), expect and compute " - << "a counter-example" << std::endl - << " -E emptiness-check (Couvreur), expect no counter-example " + << " -eALGO emptiness-check, expect and compute an accepting run" << std::endl - << " -E2 emptiness-check (Couvreur variant), expect no " - << "counter-example " << std::endl + << " -EALGO emptiness-check, expect no accepting run" << std::endl << " -f use Couvreur's FM algorithm for translation" << std::endl << " -F read the formula from the file" << std::endl << " -L fair-loop approximation (implies -f)" << std::endl - << " -m magic-search (implies -D), expect a counter-example" - << std::endl - << " -M magic-search (implies -D), expect no counter-example" - << std::endl - << " -n same as -m, but display more counter-examples" - << std::endl << " -N display the never clain for Spin " << "(implies -D)" << std::endl << " -p branching postponement (implies -f)" << std::endl @@ -121,7 +110,14 @@ syntax(char* prog) << " -X do not compute an automaton, read it from a file" << std::endl << " -y do not merge states with same symbolic representation " - << "(implies -f)" << std::endl; + << "(implies -f)" << std::endl + << std::endl + << "Where ALGO should be one of:" << std::endl + << " couvreur99" << std::endl + << " couvreur99_shy" << std::endl + << " magic_search" << std::endl + << " magic_search_repeated" << std::endl + ; exit(2); } @@ -138,6 +134,7 @@ main(int argc, char** argv) bool file_opt = false; int output = 0; int formula_index = 0; + std::string echeck_algo; enum { None, Couvreur, Couvreur2, MagicSearch } echeck = None; enum { NoneDup, BFS, DFS } dupexp = NoneDup; bool magic_many = false; @@ -176,27 +173,21 @@ main(int argc, char** argv) { degeneralize_opt = true; } - else if (!strcmp(argv[formula_index], "-e")) + else if (!strncmp(argv[formula_index], "-e", 2)) { - echeck = Couvreur; + if (argv[formula_index][2] != 0) + echeck_algo = argv[formula_index] + 2; + else + echeck_algo = "couvreur99"; expect_counter_example = true; output = -1; } - else if (!strcmp(argv[formula_index], "-e2")) + else if (!strncmp(argv[formula_index], "-E", 2)) { - echeck = Couvreur2; - expect_counter_example = true; - output = -1; - } - else if (!strcmp(argv[formula_index], "-E")) - { - echeck = Couvreur; - expect_counter_example = false; - output = -1; - } - else if (!strcmp(argv[formula_index], "-E2")) - { - echeck = Couvreur2; + if (argv[formula_index][2] != 0) + echeck_algo = argv[formula_index] + 2; + else + echeck_algo = "couvreur99"; expect_counter_example = false; output = -1; } @@ -213,28 +204,6 @@ main(int argc, char** argv) fair_loop_approx = true; fm_opt = true; } - else if (!strcmp(argv[formula_index], "-m")) - { - echeck = MagicSearch; - degeneralize_opt = true; - expect_counter_example = true; - output = -1; - } - else if (!strcmp(argv[formula_index], "-M")) - { - echeck = MagicSearch; - degeneralize_opt = true; - expect_counter_example = false; - output = -1; - } - else if (!strcmp(argv[formula_index], "-n")) - { - echeck = MagicSearch; - degeneralize_opt = true; - expect_counter_example = true; - output = -1; - magic_many = true; - } else if (!strcmp(argv[formula_index], "-N")) { degeneralize_opt = true; @@ -350,6 +319,32 @@ main(int argc, char** argv) } } + if (echeck_algo == "couvreur99") + { + echeck = Couvreur; + } + else if (echeck_algo == "couvreur99_shy") + { + echeck = Couvreur2; + } + else if (echeck_algo == "magic_search") + { + echeck = MagicSearch; + degeneralize_opt = true; + } + else if (echeck_algo == "magic_search_repeated") + { + echeck = MagicSearch; + degeneralize_opt = true; + magic_many = true; + } + else + { + std::cerr << "unknown emptiness-check: " << echeck_algo << std::endl; + syntax(argv[0]); + } + + std::string input; if (file_opt)