15 Jun
2018
15 Jun
'18
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