Hello!
Given a co-Buchi automaton and some number K, my function [1] creates another automaton ("co-Reachability") that bounds by K the maximal number of visits to co-Buchi accepting states.
I currently create the new automaton like this:
auto new_aut = make_twa_graph(aut->get_dict())
but this BDD-dictionary sharing between the new and the original automaton looks suspicious: once the original automaton dies and kills its dictionary (?), the new automaton will no longer be able to use it. Right?
I guess the correct way is to create a new dictionary for the new automaton:
auto new_d = spot::make_bdd_dict();
But then: what will be the natural way to copy edges of the original automaton into the new automaton? I currently simply iterate over edges of `aut` and do smth like:
for (auto &t: aut->out(state)) k_aut->new_edge(src_state, dst_state, t.cond);
where `t.cond` refers to a BDD of `aut`. So, I will need to create `cond` that uses new BDD dict, right? Which functions will be useful for doing that?
Thanks!
A minor point: If you use CUDD library and SPOT in the same project, then you will get compilation errors, because: CUDD does not use namespaces and has type `BDD`, and and Buddy in SPOT does not use namespaces and has `BDD`. To overcome the clash, the simple trick below works, but... maybe put Buddy into separate namespace? (minor feature request:) (I apologize for not providing the patch!) My current workaround is: whenever including SPOT headers, include them like this:
#define BDD spotBDD #include <spot/twa/twagraph.hh> #include <spot/twaalgos/sccinfo.hh> #undef BDD
best wishes, Ayrat Khalimov
[1] https://github.com/5nizza/sdf-hoa/blob/master/src/k_reduce.cpp#L69
Hi Ayrat
On Thu, Jun 14, 2018 at 6:24 PM, Ayrat Khalimov ayrat.khalimov@gmail.com wrote:
Hello!
Given a co-Buchi automaton and some number K, my function [1] creates another automaton ("co-Reachability") that bounds by K the maximal number of visits to co-Buchi accepting states.
I currently create the new automaton like this:
auto new_aut = make_twa_graph(aut->get_dict())but this BDD-dictionary sharing between the new and the original automaton looks suspicious: once the original automaton dies and kills its dictionary (?), the new automaton will no longer be able to use it.
This is safe and the correct thing to do in your case. Dictionaries are reference-counted, so they will only be killed once they are not used anywhere.
Usually you want to use the same dictionary everywhere. The only use-case for different dictionaries is if you build automata that are completely unrelated, so they do not need to agree on the BDD representation of their letters. For instance when doing a web servers that translate LTL formulas into automata, we need to
A minor point: If you use CUDD library and SPOT in the same project, then you will get compilation errors, because: CUDD does not use namespaces and has type `BDD`, and and Buddy in SPOT does not use namespaces and has `BDD`. To overcome the clash, the simple trick below works, but... maybe put Buddy into separate namespace? (minor feature request:) (I apologize for not providing the patch!) My current workaround is: whenever including SPOT headers, include them like this:
#define BDD spotBDD #include <spot/twa/twagraph.hh> #include <spot/twaalgos/sccinfo.hh> #undef BDD
Hmm... I'm not sure if we can introduce a namespace for BuDDy without breaking all existing user code. BDD is not supposed to be used by users of the C++ interface, so maybe we could arrange things so that the BDD typedef is only used when compiling in C?
[1] https://github.com/5nizza/sdf-hoa/blob/master/src/k_reduce.cpp#L69
Some minor suggestions:
1) Get rid of spot::trivial:: using
L70 aut->is_sba().is_true() L126 k_aut->prop_terminal(true); L127 k_aut->prop_state_acc(true);
2) You can refactor L113-L118 by only doing a single call to kstate_by_state_k.find(dst_k_pair) instead of two.
3) I think the only time you need to insert a state into kstates_to_process is immediately right after you have created to corresponding state in the result automaton k_aut->new_state(). If you do so, you never need the processed_kstates set, and kstates_to_process does not need to be implemented as a set anymore (a vector is enough). Additionally, if this vector of kstate_to_process stores pairs (kstate, state), instead of just kstate, they you should be able to get rid of the state_by_kstate map and associated lookup.
Best regards,
hi Alexandre,
Dictionaries are reference-counted, so they will only be killed once they are not used anywhere.
Oh, I missed that `get_aut()` returns a shared pointer, thanks!
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. Calling `new_aut->register_aps_from_dict();` does not help. Does this mean that the correct way to get the set of atomic propositions used by the new automaton would be to iterate over its edges and collect them?
Thanks for your suggestions regarding the code: your point (3) has a nice insight that simplifies and (should) speed up the code, I have implemented every bit of it!
As for Buddy/Cudd clash, I am not knowledgeable about intricacies of C/C++ compilation, but I am happy with the current workaround!
Many thanks for your help, a On Fri, Jun 15, 2018 at 1:00 PM, Alexandre Duret-Lutz adl@lrde.epita.fr wrote:
Hi Ayrat
On Thu, Jun 14, 2018 at 6:24 PM, Ayrat Khalimov ayrat.khalimov@gmail.com wrote:
Hello!
Given a co-Buchi automaton and some number K, my function [1] creates another automaton ("co-Reachability") that bounds by K the maximal number of visits to co-Buchi accepting
states.
I currently create the new automaton like this:
auto new_aut = make_twa_graph(aut->get_dict())but this BDD-dictionary sharing between the new and the original
automaton
looks suspicious: once the original automaton dies and kills its dictionary (?), the new automaton will no longer be able to use it.
This is safe and the correct thing to do in your case. Dictionaries are reference-counted, so they will only be killed once they are not used anywhere.
Usually you want to use the same dictionary everywhere. The only use-case for different dictionaries is if you build automata that are completely unrelated, so they do not need to agree on the BDD representation of their letters. For instance when doing a web servers that translate LTL formulas into automata, we need to
A minor point: If you use CUDD library and SPOT in the same project, then you will get compilation errors, because: CUDD does not use namespaces and has type `BDD`, and and Buddy in SPOT does not use namespaces and has `BDD`. To overcome the clash, the simple trick below works, but... maybe put Buddy into separate namespace? (minor feature request:) (I apologize for not providing the patch!) My current workaround is: whenever including SPOT headers, include them
like
this:
#define BDD spotBDD #include <spot/twa/twagraph.hh> #include <spot/twaalgos/sccinfo.hh> #undef BDDHmm... I'm not sure if we can introduce a namespace for BuDDy without breaking all existing user code. BDD is not supposed to be used by users of the C++ interface, so maybe we could arrange things so that the BDD typedef is only used when compiling in C?
[1] https://github.com/5nizza/sdf-hoa/blob/master/src/k_reduce.cpp#L69
Some minor suggestions:
- Get rid of spot::trivial:: using
L70 aut->is_sba().is_true() L126 k_aut->prop_terminal(true); L127 k_aut->prop_state_acc(true);
- You can refactor L113-L118 by only doing a single call to
kstate_by_state_k.find(dst_k_pair) instead of two.
- I think the only time you need to insert a state into
kstates_to_process is immediately right after you have created to corresponding state in the result automaton k_aut->new_state(). If you do so, you never need the processed_kstates set, and kstates_to_process does not need to be implemented as a set anymore (a vector is enough). Additionally, if this vector of kstate_to_process stores pairs (kstate, state), instead of just kstate, they you should be able to get rid of the state_by_kstate map and associated lookup.
Best regards,
Alexandre Duret-Lutz
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 -
Ayrat Khalimov