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,

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 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