// This is a very simple example of ATPG for a digital combinational circuit using Alloy
// CC-BY Samuel A. Kirk, http://www.samkirk.com, v0.1

open util/boolean

abstract sig Fault { }
one sig NF, SA0, SA1 extends Fault { }  // no fault, stuck at 0, stuck at 1

abstract sig Node { v: Bool }
one sig O1, I1, I2, X1 extends Node { }	  // The pristine (unfaulted) version of the circuit
one sig O1', I1', I2', X1' extends Node { }  // The faulted version of the circuit.
    // O = Output, I = Input, X = internal (non-observable) node

fun Connect [input: Bool, f: Fault] : Bool {
// Connect -  passes along the value from its input if there's no fault (NF).  Otherwise,
// it passes along True 
//    if the fault injected is stuck at one (SA1), or False if stuck at zero (SA0)
// input is the value it receives
// the "returned" value is the value the Connector "outputs"
    ( f = NF) => input else
    ( f = SA1 ) => True else 
    ( f = SA0 ) => False else
    none
    }

pred Network [ f: Fault, o1, i1, i2, x1: Node ] { 
// Network - predicate defining the structure of the circuit using Boolean functions and Connect.
// The inputs are given as parameters and are used but not "assigned" or otherwise defined.
// This predicate is invoked for both the faulted and the non-faulted circuit in a single run by
// the caller.

    o1.v = And [ i1.v, x1.v ]
    x1.v = Connect [ i2.v, f ]
    }

pred Compare( ) {
// Is there a single set of inputs, I1 and I2, for the faulted and unfaulted circuit such that 
// the output, O1, differs when there's no fault (NF) 
// as compared to when there is a fault (SA1 or SA0) ?

    // faulted inputs = non-faulted inputs.
    I1.v = I1'.v
    I2.v = I2'.v

    // faulted outputs != non-faulted outputs
    O1.v != O1'.v

    Network[ NF, O1, I1, I2, X1 ]
    Network[ SA1, O1', I1', I2', X1' ]
    }

run Compare for 3