hi!
With the aid of SPOT I am developing a counter-example guided synthesizer
in python. See [1] if interested for details.
My question is:
I am trying to parse twa_run in python,
namely, parse the labels of the each step (`spot.impl.step`).
Is there a python way to walk through BDD?
(The label is a simple cube expressed in BDD, and I need to convert it into
my internal structure)
(yes, this is rather a question about python interface for buddy)
(no, that is not feature request:) if not possible, I will simply print the
label and parse the string, that is not crucial)
[1]
The idea is
- guess the model,
- then model check it and get a counter-example
- then encode the counter-example into the "guesser" (which uses an SMT
solver)
thanks,
Ayrat
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
