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?

Thanks in advance,

Sergio Hernández