diff --git a/ChangeLog b/ChangeLog index a125f28f5..ebdb9002a 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2010-11-25 Alexandre Duret-Lutz + + "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 Fix bugs in minimize(). diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index f87fe2552..3b4be7523 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -921,8 +921,15 @@ main(int argc, char** argv) } else // We don't know if A is a safety automaton. { - // Let's make sure that a recognize the same language - // as minimized. + if (!f) + { + 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::unop::instance(spot::ltl::unop::Not, f->clone()); spot::tgba* n = spot::ltl_to_tgba_fm(neg, dict, fm_exprop_opt,