Spot

Download

spot@lrde.epita.fr

June 2018

2 participants
2 discussions

Walking through BDD formula in python
by Ayrat Khalimov 26 May '21

26 May '21

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

2 5

Cloning an automaton
by Ayrat Khalimov 17 Jun '18

17 Jun '18

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

2 3