On Sun, Jun 17, 2018 at 5:59 AM, Ayrat Khalimov <ayrat.khalimov@gmail.com> wrote:
A related question: I try to enumerate all the propositions of the new automaton by calling
for (const spot::formula& ap: new_aut->ap())
but new_aut->ap() is empty (it is not empty for the original automaton). The documentation for `ap()` says that it returns propositions registered by this automaton. I guess, since the new automaton itself does not register any propositions, `ap()` is empty.
Yes, and if the transitions are actually using some propositions, this discrepancy may cause several issues later. (spot::print_hoa(...) has a check for this and should raise an exception if the automaton uses unregistered atomic propositions.) When new_aut is created from scratch, you use new_aut->register_ap(ap1), and work from that. (e.g. https://spot.lrde.epita.fr/tut22.html). If new_aut is built from old_aut, as in your case, you usually want to copy its alphabet with new_aut->copy_ap_of(old_aut); There are sometimes cases where you don't want the alphabet to be the same. After a copy you can still use register_ap()/unregister_ap() to modify the alphabet. In the case that your algorithm may reduce the alphabet, you can also call new_aut->remove_unused_ap() after new_aut has been constructed: this will scan all transitions to detect unused propositions.
Calling `new_aut->register_aps_from_dict();` does not help.
This method should probably not be public. It's mostly an historical artifact. In the past (Spot 1.x and before) we used to register APs directly to the dictionary, because automata did not keep track of their alphabet. This method helps with some lowlevel stuff that still work in this way. -- Alexandre Duret-Lutz