alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

"ltl2tgba -Rm -X foo.tgba" would fail.

Browse source 
* src/tgbatest/ltl2tgba.cc (main): Warn if -Rm is used without
knowing the formula whose automaton is minimized.
This commit is contained in:
Alexandre Duret-Lutz 2010-11-25 13:21:34 +01:00
parent 7d8a5310e4
commit a962bb6ddc
2 changed files with 16 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
ChangeLog
View file

@ -1,3 +1,10 @@
2010-11-25 Alexandre Duret-Lutz <adl@lrde.epita.fr>
"ltl2tgba -Rm -X foo.tgba" would fail.
* src/tgbatest/ltl2tgba.cc (main): Warn if -Rm is used without
knowing the formula whose automaton is minimized.
2010-11-25 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2010-11-25 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Fix bugs in minimize(). Fix bugs in minimize().

11
src/tgbatest/ltl2tgba.cc
View file

@ -921,8 +921,15 @@ main(int argc, char** argv)
} }
else // We don't know if A is a safety automaton. else // We don't know if A is a safety automaton.
{ {
// Let's make sure that a recognize the same language if (!f)
// as minimized. {
std::cerr << "Error: Without a formula I cannot make "
<< "sure that the automaton built with -Rm\n"
<< " is correct." << std::endl;
exit(2);
}
// Let's make sure that A recognizes the same language
// as MINIMIZED.
spot::ltl::formula* neg = spot::ltl::formula* neg =
spot::ltl::unop::instance(spot::ltl::unop::Not, f->clone()); spot::ltl::unop::instance(spot::ltl::unop::Not, f->clone());
spot::tgba* n = spot::ltl_to_tgba_fm(neg, dict, fm_exprop_opt, spot::tgba* n = spot::ltl_to_tgba_fm(neg, dict, fm_exprop_opt,