Hi Sergio On Mon, May 23, 2016 at 11:46 AM, Sergio Hernández <shernandez(a)unizar.es> wrote: 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