23 May
2016
23 May
'16
2:21 p.m.
Hi Sergio
On Mon, May 23, 2016 at 11:46 AM, Sergio Hernández <shernandez(a)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