Thank you, it solved the problem.

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.

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?

Thank you very much for all your help,
Miriam


On Thu, Jan 7, 2016 at 9:38 AM Alexandre Duret-Lutz <adl@lrde.epita.fr> wrote:
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.
--
Alexandre Duret-Lutz