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