10 Jan
2016
10 Jan
'16
10:41 p.m.
On Sun, Jan 10, 2016 at 5:14 PM, Miriam Blank <miriampo(a)gmail.com> wrote:
Thank you, it solved the problem.
... and it won't be necessary in 1.99.7, as I just added this call to
twa::~twa().
I am trying to implement on-the-fly model checking. To
do this, I extended
spot::state, spot::kripke_succ_iterator and spot::kripke and implemented the
required methods.
As a starting point, I want to implement a simple kripke structure that has
only one state (labeled "s0"), in which one atomic proposition is true (p).
This state has a self-loop.
Good plan.
There must be something that I implemented wrong,
because I get segmentation
faults in four (separate) cases in my code (attached).
Can you please look at it and try to explain where is my mistake?
Sure
There are some memory management issues with the on-the-fly interface:
1) The iterator returned by succ_iter() should be a new instance. The
caller of succ_iter() can do two things when it has finished with the
iterator: either "delete" it or (preferred) call release_iter() to give the
iterator back to the automaton.
So as a first step, just make sure that the return value of succ_iter()
is a new object that can be deleted.
Later you may decide to optimize a bit and recycle iterators, as
described below, but that is entirely optional.
Most algorithms do something like
for (auto i: aut->succ(s))
{
// use i->dst(), i->cond(), i->acc()
}
which is just syntactic sugar for
twa_succ_iterator* i = aut->succ_iter(s);
if (i->first())
do
{
// use i->dst(), i->cond(), i->acc()
}
while (i->next());
aut->release_iter(i);
and twa::release_iter() has a very straightforward
implementation: it has a one slot memory for
released iterators (called twa::iter_cache_) and will
call delete on any passed iterator if that slot is full.
To recycle iterator, you would modify your succ_iter()
method such that if iter_cache_ is not nullptr, then
you can take that iterator, update it for the current
request, and return it without allocating anything
(but do not forger to clear iter_cache_).
2) the memory management of states is slightly
different. state* returned by methods like
twa_succ_iterator::dst(), twa::get_init_state()
or state::clone() are always destroyed by
calling the state::destroy() method of the state.
(delete is NEVER called directly for states.)
By default state::destroy() calls delete, which means
that all the above methods should return a fresh
state instance. In that situation the state::compare()
and state::hash() methods are super important
has they can be used to decide whether two different
state* objects refer to the same automaton state.
In Kripke structures, even computed on the fly,
it's more efficient to keep a unicity table such that
the pointer returned by dst() or get_init_state() will
be unique for a given state, and clone() can be
implemented as an identity function, saving a lot
of memory allocations. In that case destroy()
should be overloaded, and implemented as an
empty function
So in your case where you have a single,
pre-allocated state, I would override destroy()
to do nothing, and fix clone() to simply "return this".
(modulo the const issue: I'm not sure why clone()
returns a non-const state*; that's probably another
thing I should fix before 2.0)
Then there is a small issue with the twa_succ_iterator
interface:
3) The methods first(), next(), done(), are meant to be
used as in
for (i->first(); !i->done(); i->next())
{
// use i->dst(), i->cond(), i->acc()
}
or more efficiently:
if (i->first())
do
{
// use i->dst(), i->cond(), i->acc()
}
while (i->next());
because that saves all the calls to done() (halving
the number of virtual calls necessary to make the loop).
But in your current implementation of MyIterator, with
next() returning true, and done() returning done, both
loops are infinite...
A couple of more suggestions, but these are not
causing any problems:
4) BuDDy gets initialized automatically when you
create a bdd_dict for the first time, so you can
remove those lines.
5) twa_succ_iterator::current_state() is the old name
of twa_succ_iterator::dst(). You do not need the
former.
I'm attaching a version of your program with all the
above changes. Note that I changed the #include
to match the conventions that will be needed
with Spot 1.99.7 once it is released: replace them
with what you had to compile with 1.99.6.
--
Alexandre Duret-Lutz