diff --git a/ChangeLog b/ChangeLog index 88305f6ac..7e22af67d 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2010-11-30 Alexandre Duret-Lutz + + Rationalize options for counter-example output. + + * src/tgbatest/ltl2tgba.cc (main): Either replay the accepting + run or print it, but do not do both. + * src/tgbatest/emptchk.test: Adjust. I.e. use -C instead of -CR + when we expect the run to be displayed. + 2010-11-30 Alexandre Duret-Lutz Fix a GCC 4.6 warning. diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test index 17b221d09..7630fa528 100755 --- a/src/tgbatest/emptchk.test +++ b/src/tgbatest/emptchk.test @@ -54,10 +54,10 @@ expect_ce() run 0 ../ltl2tgba -CR -eTau03_opt -f "$1" run 0 ../ltl2tgba -CR -eGV04 -f "$1" # Expect multiple accepting runs - test `../ltl2tgba -CR -e'CVWY90(repeated)' -l "$1" | - grep Prefix: | wc -l` -ge $2 - test `../ltl2tgba -CR -e'SE05(repeated)' -l "$1" | - grep Prefix: | wc -l` -ge $2 + test `../ltl2tgba -C -e'CVWY90(repeated)' -l "$1" | + grep Prefix: | wc -l` -ge $2 + test `../ltl2tgba -C -e'SE05(repeated)' -l "$1" | + grep Prefix: | wc -l` -ge $2 } expect_no() @@ -80,9 +80,9 @@ expect_no() run 0 ../ltl2tgba -CR -E'SE05(bsh=10M)' -f "$1" run 0 ../ltl2tgba -CR -ETau03_opt -f "$1" run 0 ../ltl2tgba -CR -EGV04 -f "$1" - test `../ltl2tgba -CR -e'CVWY90(repeated)' -l "!($1)" | + test `../ltl2tgba -C -e'CVWY90(repeated)' -l "!($1)" | grep Prefix: | wc -l` -ge $2 - test `../ltl2tgba -CR -e'SE05(repeated)' -l "!($1)" | + test `../ltl2tgba -C -e'SE05(repeated)' -l "!($1)" | grep Prefix: | wc -l` -ge $2 } diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 6bf58a5ca..cbc2f015c 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1161,28 +1161,36 @@ main(int argc, char** argv) delete run; run = redrun; } - tm.start("printing accepting run"); - if (graph_run_opt) - { - spot::tgba_run_dotty_decorator deco(run); - spot::dotty_reachable(std::cout, a, &deco); - } - else if (graph_run_tgba_opt) - { - spot::tgba* ar = spot::tgba_run_to_tgba(a, run); - spot::dotty_reachable(std::cout, ar); - delete ar; - } - else - { - spot::print_tgba_run(std::cout, a, run); - if (accepting_run_replay - && !spot::replay_tgba_run(std::cout, a, run, - true)) + if (accepting_run_replay) + { + tm.start("replaying acc. run"); + if (!spot::replay_tgba_run(std::cout, a, + run, true)) exit_code = 1; - } - delete run; - tm.stop("printing accepting run"); + tm.stop("replaying acc. run"); + } + else + { + tm.start("printing accepting run"); + if (graph_run_opt) + { + spot::tgba_run_dotty_decorator deco(run); + spot::dotty_reachable(std::cout, a, &deco); + } + else if (graph_run_tgba_opt) + { + spot::tgba* ar = + spot::tgba_run_to_tgba(a, run); + spot::dotty_reachable(std::cout, ar); + delete ar; + } + else + { + spot::print_tgba_run(std::cout, a, run); + } + delete run; + tm.stop("printing accepting run"); + } } } else