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