Created
February 1, 2019 18:37
-
-
Save hwayne/736e98e415c01ce82d2bddf549126e9e to your computer and use it in GitHub Desktop.
half-adder
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
//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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment