Commit 75a24111 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent ae03bc67
2010-11-30 Alexandre Duret-Lutz <adl@lrde.epita.fr>
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 <adl@lrde.epita.fr>
Fix a GCC 4.6 warning.
......
......@@ -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
}
......
......@@ -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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment