is it possible to model a logic gate in alloy

Question

I'm a new Alloy learner. I have a few things in mind I would like to know.

Is it possible to create an element?

How would you model an AND logic gate?

My idea wich is useles is something like

open util/ordering[Time]
sig Time {frame: set gate}


abstract sig gate{}
sig ABinCout extends gate{ 
getA    : A,
getB    : B,
outputsC    : C,
} 


abstract sig Signals {}
sig A extends Signals{}
sig B extends Signals{}
sig C extends Signals{}


fact{first.frame = gate && no gate.getA && no gate.getB && no gate.outputsC } 

pred GateAB [t,t' : set Time,Gate : ABinCout]{
one a : A  | one b : B | {
Gate.getA = Gate.getA + a 
Gate.getB = Gate.getB + b
}}

pred GateABparaC [Gate : set ABinCout]{
one a : Gate.getA | one b : Gate.getB | one c : C{
    Gate.getA = Gate.getA - a
    Gate.getB = Gate.getB - b
    Gate.outputsC = Gate.outputsC + c

}}

pred GateC [Gate : set ABinCout]{
one c : Gate.outputsC | {
    Gate.outputsC =Gate.outputsC - c
}}

fact{
all t : Time, t' : t.next | one cel: ABinCout{
 GateAB[t,t',cel]
}}


run{ }for exactly 2 Time, 1 ABinCout, 3 A, 3 B, 1 C 

I can literally say i know nothing about alloy, but i would like to represent the gate alone... then I spawn 2 inputs... then in another frame it makes an output which is not any of the inputs!

Thanks in advance

If there is something I should read or now to do this task please say it.

Answer 1

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 Ones).

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