From 44e4beca2eb94eae668257f542f4ab1d0b61dcfc Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 26 Jul 2007 13:51:16 +0000 Subject: [PATCH] * src/tgbatest/ltl2tgba.cc (main): Correctly destroy unobservable events. --- ChangeLog | 5 +++++ src/tgbatest/ltl2tgba.cc | 14 ++++++++++++-- 2 files changed, 17 insertions(+), 2 deletions(-) diff --git a/ChangeLog b/ChangeLog index 57bbec670..56e8dfe69 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,8 @@ +2007-07-26 Alexandre Duret-Lutz + + * src/tgbatest/ltl2tgba.cc (main): Correctly destroy unobservable + events. + 2007-07-23 Alexandre Duret-Lutz * iface/gspn/ltlgspn.cc: New option -L. diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 62239a1e4..ed41e3c9d 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -128,8 +128,10 @@ syntax(char* prog) << " -S convert to explicit automata, and number states " << "in BFS order" << std::endl << " -t display reachable states in LBTT's format" << std::endl - << " -U[PROPS] consider atomic properties PROPS as exclusive " - << "events (implies -f)" << std::endl + << " -U[PROPS] consider atomic properties of the formula as " + << "exclusive events, and" << std::endl + << " PROPS as unobservables events (implies -f)" + << std::endl << " -v display the BDD variables used by the automaton" << std::endl << " -x try to produce a more deterministic automata " @@ -849,6 +851,14 @@ main(int argc, char** argv) exit_code = 1; } + if (unobservables) + { + for (spot::ltl::atomic_prop_set::iterator i = + unobservables->begin(); i != unobservables->end(); ++i) + spot::ltl::destroy(*i); + delete unobservables; + } + assert(spot::ltl::atomic_prop::instance_count() == 0); assert(spot::ltl::unop::instance_count() == 0); assert(spot::ltl::binop::instance_count() == 0);