Hi Sergio On Mon, May 23, 2016 at 11:46 AM, Sergio Hernández <shernandez@unizar.es> wrote:
Hi,
i would like to ask you about the most efficient way of completing an automaton using bdd operations.
we are working with huge automata and we want to improve the automaton creation process. For that, one of the bottlenecks is generating the logical formulas corresponding to the automaton transitions as bdds.
For example, let us consider we have the following automaton:
State 0 | | a & b | v State 1 | | a & c | v State 2
Then, the alphabet is {a,b,c,d,e}. Thus, we need to add (!c & !d & !e) to the first transition and (!b & !d & !e) to the second one in order to make queries such as "F(e)".
Currently, we are implementing this manually using a loop where for each transition we add the negation of every condition that is not present in the transition. But it is not fast enough.
Is there any bdd operation to implement this in an efficient way?
I was a bit confused by these last two paragraphs, so I hope my answer will make sense to you. Each transition stores its label as a BDD. If you want to modify all labels, you have to loop over all transitions, probably using something like for (auto& t: aut->edges()) t.cond = some_function(t.cond); There is no BDD operation that would get rid of this loop, but there are multiple ways to implement some_function() using BDD operations. Let's assume that t.cond is always a conjunction (like a&c in your example), and that there exists a variable ALL = a&b&c&d&e that is the conjunct of all propositions. Then one possible implementation is t.cond = bdd_satoneset(t.cond, ALL, bddfalse) because bdd_satoneset will return one assignement satisfying t.cond using all variables of ALL, using negated variables whenever there is a choice. Note however that bdd_satoneset() does not implement any cache, so if your automaton has several duplicate labels, it is probably worthwhile to cache it. An alternative approach would be to append to labels all negated atomic propositions that are not in the label. For this, prepare an ALLNEG variable that always contains !a&!b&!c&!d&!e and do t.cond &= bdd_exists(ALLNEG, t.cond) These two operations (exists and &) both use a cache, but it might still be worthwhile to add one in your function. I don't know which one would be faster (but if you do the benchmark, I'm curious to know). If you are creating this automaton from scratch, you should also consider creating "complete" labels directly using a function such as bdd_buildcube() or bdd_ibuildcube(). I believe that using one of these two functions behind a cache would be the most efficient way to create these labels. Hope this helps -- Alexandre Duret-Lutz