730 CHAPTER 16 Automated System Verification Result based on the disjunct on all triples of justifications satisfying these additional constraints. As the number of units n and thus the number of bits to encode a justification are big and the power set is exponential in n, we might doubt that this BDD can be constructed, but we explicitly build the BDD for c i = a i b i on every index i and build the conjunct for all i {1, . . . , n}. Let A(a, j a ) be the description of the first input and B(b, j b ) be the description of the second input. Then we have C(c, j c ) = a, j a , b, j b (A(a, j a ) B(b, j b ) F(a, b, c) Result ( j a , j b , j c )). The implementation of the proposed diagnosis system based on BDDs is simple. Any diagnostic variable consists of a marker final, a BDD bdd representing all possible value/justification pairs, and the variable sets for addressing value and just. Diagnostic variables are linked to at least two devices to inform the devices if a change to a BDD has been obtained. There are four cases to terminate the propagation: The output is final: We have full knowledge of the output values. One input BDD is the zero function: We prevent propagation. The output BDD is the zero function: Either the computation on the restricted domain is not possible or one boundary condition to the relation Result is met. . . .