On Wed, Jan 6, 2016 at 7:34 PM, Miriam Blank miriampo@gmail.com wrote:

Thank you, this was very helpful.

Following that, I have another question -

This code prints errors. How can I avoid them?

code: spot::bdd_dict_ptr dict = spot::make_bdd_dict(); spot::kripke_ptr model = std::make_shared<MyKripke>(dict); model->register_ap("p");

errors: some maps are not empty Variable Map: 0 Var[p] x1 { 0xb32fd0 } 1 Free Anonymous lists: [0] Free list: (1, 1) Aborted

This is the bdd_dict telling you that BDD variable #0 is still associated to atomic proposition "p" for the object 0xb32fd0 (which in this case should be your model).

You probably need get_dict()->unregister_all_my_variables(this); in the destructor of MyKripke.

I realize now that since we introduced twa::register_ap() to hide most of the interactions with the bdd_dict, it should probably be cleaner if unregister_all_my_variables() was called in the twa destructor so that it is not necessary to call it in the destructor of every subclass. I'll have a look at that.

On Sun, Jan 10, 2016 at 5:14 PM, Miriam Blank miriampo@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.