half-adder

half-adder-jackson.als

//This is the one that Daniel Jackson wrote

 abstract sig Node {inputs: set Node}

 sig Source extends Node {} {no inputs}
 sig Sink extends Node {} {one inputs}

 abstract sig Gate extends Node {}
 sig And, Or, Xor extends Gate {} {#inputs = 2}
 sig Not extends Gate {}  {one inputs}

 sig State {
 	high: set Node
 	} {
 	all g: Gate {
 		g in And implies (g in high iff g.inputs in high)
 		g in Or implies (g in high iff some g.inputs & high)
 		g in Xor implies (g in high iff one g.inputs & high)
 		g in Not implies (g in high iff no g.inputs & high)
 		}
 	all n: Sink | n in high iff n.inputs in high	
 }

 fact Acyclic {
 	no ^inputs & iden
 	}

 fact CanonicalStates {
 	no disj s, s': State | s.high & Source = s'.high & Source
 	}

 fact HalfAdder {	
 	some disj A, B, S, C: Node | all s: State {
 		A + B = Source and S + C = Sink
 		C in s.high iff A+B in s.high
 		S in s.high iff one (A+B) & s.high
 		}
 	#State = 4
 	}

 run {} for 6

half-adder.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