14 Jun
2018
14 Jun
'18
6:24 p.m.
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
15 Jun
15 Jun
noon
Hi Ayrat
On Thu, Jun 14, 2018 at 6:24 PM, Ayrat Khalimov
<ayrat.khalimov(a)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?
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,
--
Alexandre Duret-Lutz
17 Jun
17 Jun
5:59 a.m.
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(a)lrde.epita.fr>
wrote:
> Hi Ayrat
>
> On Thu, Jun 14, 2018 at 6:24 PM, Ayrat Khalimov
> <ayrat.khalimov(a)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,
> --
> Alexandre Duret-Lutz
>
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
2425
days inactive
2428
days old
3 comments
2 participants
participants (2)
-
Alexandre Duret-Lutz -
Ayrat Khalimov