1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 | language Essence 1.3 $ Problem Diagnosis $ $ Problem details available at http://www.csplib.org/Problems/prob042/ $ $ Essence model by Andrew Martin $ $ Licenced under CC-BY-4.0 : http://creativecommons.org/licenses/by/4.0/ given numGates : int (1..) letting dGates be domain int (1..numGates) letting dGatesZero be domain int (0..numGates) $ each gate maps to a function converting (bool, bool) to bool given gateFuncs : function ( total ) dGates --> ( function matrix indexed by [ int (1..2)] of bool --> bool ) given gateInpts : function ( total ) dGates --> matrix indexed by [ int (1..2)] of int (-1..numGates) given finalOutputs : function dGates --> bool $ false for stuck off, true for stuck on, if there is no mapping for a gate, that gate is not faulty find faultyGates : function dGates --> bool minimising |faultyGates| such that exists gateOutput : function ( total ) int (-1..numGates) --> bool . $ define external inputs gateOutput(-1) = false /\ gateOutput(0) = true /\ $ ensure that all gates either - ( forAll gate : dGates . $ meet expected outputs based on their function ( gateOutput(gate) = gateFuncs(gate)([gateOutput(gateInpts(gate)[1]), gateOutput(gateInpts(gate)[2])]) \/ $ are broken in the correct way (either stuck on or off) gateOutput(gate) = faultyGates(gate) ) ) /\ $ ensure output equals given output ( forAll (gateLinkedtoOutput, expectedOutput) in finalOutputs . gateOutput(gateLinkedtoOutput) = expectedOutput ) |