I made this as a fun demo five years ago. Uses Alloy. It's not particularly good Alloy code.
Created
February 6, 2023 21:53
-
-
Save hwayne/2fe25993b62b69ddb1901c969f93fed7 to your computer and use it in GitHub Desktop.
Simple example of alloy synthesis
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