Simple example of alloy synthesis

readme.md

I made this as a fun demo five years ago. Uses Alloy. It's not particularly good Alloy code.

circuit.als

enum Val {On, Off}

sig P {} //"Permutation"
abstract sig Input {
  val: Val one -> P
}

sig Source extends Input {}

abstract sig Gate extends Input {
  input: set Input,
} {
  some input
}

sig And extends Gate {}
sig Or extends Gate {}
sig Not extends Gate {}
sig Xor extends Gate {}
fact AndGates {
  all g: And | all p: P |
    #g.input = 2 and
    g.input.val.p = On implies g.val.p = On else g.val.p = Off
}S

fact OrGates {
  all g: Or | all p: P |
    #g.input = 2 and
    On in g.input.val.p implies g.val.p = On else g.val.p = Off
}

fact NotGates {
  all g: Not | {
    one g.input
    all p: P |
    g.input.val.p = Off implies g.val.p = On else g.val.p = Off
  }
}

fact XorGates {
  all g: Xor | all p: P | {
    #g.input = 2
    g.input.val.p = On + Off implies g.val.p = On else g.val.p = Off
  }
}

fun transitive_outputs(i: Input): set Input {
  i.^input //might be backwards, still valid
}

fun End: set Input {
  Input - Input.input
}

fact NoCycles {
  all g: Gate |
    no g.transitive_outputs & g
}

pred HalfAdder {
  some disj A, B: Source |
    some disj S, C: Gate |
      some p1, p2, p3, p4: P |  {  
        A + B = Source
        S + C = End
        A->Off + B->Off + C->Off + S->Off in val.p1
        A->On + B->Off + C->Off + S->On in val.p2
        A->Off + B->On + C->Off + S->On in val.p3
        A->On + B->On + C->On + S->Off in val.p4

      }
}

run {HalfAdder} for 4 Input, 4 P