17 Jun
2018
17 Jun
'18
1:28 p.m.
On Sun, Jun 17, 2018 at 5:59 AM, Ayrat Khalimov
<ayrat.khalimov(a)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