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