It is not clear what exactly you're trying to achieve with your gates. Hopefully my example below will clarify certain things about Alloy and help you design whatever gates you want.
In this simple example, there is an abstract sig representing signals, and exactly two different concrete kinds of signals: One
and Zero
. Next, an abstract gate is modelled to have a set of signals on its input (the ins
field) and exactly one signal on its output (out
field). Finally, I defined 3 concrete sigs modelling the standard AND, OR, and NOT gates; for each of those sigs I added an appended fact to establish the relationship that must hold between the signals found on the input and the output (e.g., the output of an AND
gate is One
if and only if all of its inputs are One
s).
Then I thought it would be useful to show how you can model more complex gates composed of several simple ones. I defined the xorgate
predicate which asserts that the given input signals (a
, b
) and gates (and1
, and2
, not1
, not2
, or1
) are together forming a XOR gate ("connected" as in the picture below)
Now, the best part about Alloy is that you can have a run
command that will simulate this XOR gate by finding instances satisfying this predicate. You can also also have a check
command that checks that for all possible inputs on this XOR gate, its output is One
if and only if the inputs are different (which is how the XOR gate should work). Executing this check in Alloy finds no counterexample.
abstract sig Signal {}
one sig One extends Signal {}
one sig Zero extends Signal {}
abstract sig Gate {
ins: set Signal,
out: one Signal
}
sig AND extends Gate {}{ out = One iff ins in One }
sig OR extends Gate {}{ out = Zero iff ins in Zero }
sig NOT extends Gate {}{ #ins = 1 and out = Signal - ins }
pred xorgate[a, b: Signal, and1, and2: AND, not1, not2: NOT, o1: OR] {
not1.ins = a
and1.ins = b + not1.out
not2.ins = b
and2.ins = a + not2.out
or1.ins = and1.out + and2.out
}
run xorgate for 5
check {
all in1, in2: Signal |
all a1, a2: AND, n1, n2: NOT, o1: OR {
xorgate[in1, in2, a1, a2, n1, n2, o1] implies (o1.out = One iff in1 != in2)
}
} for 5