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

* src/tgbatest/ltl2tgba.cc (main): Correctly destroy unobservable

Browse source 
events.
This commit is contained in:
Alexandre Duret-Lutz 2007-07-26 13:51:16 +00:00
parent b8fd421232
commit 44e4beca2e
2 changed files with 17 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
ChangeLog
View file

@ -1,3 +1,8 @@
2007-07-26 Alexandre Duret-Lutz <adl@gnu.org>
* src/tgbatest/ltl2tgba.cc (main): Correctly destroy unobservable
events.
2007-07-23 Alexandre Duret-Lutz <adl@src.lip6.fr> 2007-07-23 Alexandre Duret-Lutz <adl@src.lip6.fr>
* iface/gspn/ltlgspn.cc: New option -L. * iface/gspn/ltlgspn.cc: New option -L.

14
src/tgbatest/ltl2tgba.cc
View file

@ -128,8 +128,10 @@ syntax(char* prog)
<< " -S convert to explicit automata, and number states " << " -S convert to explicit automata, and number states "
<< "in BFS order" << std::endl << "in BFS order" << std::endl
<< " -t display reachable states in LBTT's format" << std::endl << " -t display reachable states in LBTT's format" << std::endl
<< " -U[PROPS] consider atomic properties PROPS as exclusive " << " -U[PROPS] consider atomic properties of the formula as "
<< "events (implies -f)" << std::endl << "exclusive events, and" << std::endl
<< " PROPS as unobservables events (implies -f)"
<< std::endl
<< " -v display the BDD variables used by the automaton" << " -v display the BDD variables used by the automaton"
<< std::endl << std::endl
<< " -x try to produce a more deterministic automata " << " -x try to produce a more deterministic automata "
@ -849,6 +851,14 @@ main(int argc, char** argv)
exit_code = 1; 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::atomic_prop::instance_count() == 0);
assert(spot::ltl::unop::instance_count() == 0); assert(spot::ltl::unop::instance_count() == 0);
assert(spot::ltl::binop::instance_count() == 0); assert(spot::ltl::binop::instance_count() == 0);