Download
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
)