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