Last active
April 13, 2019 13:24
-
-
Save ashiato45/b46837f5ff1237fa9c12e64ddaf4711e to your computer and use it in GitHub Desktop.
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
sig Element{} | |
one sig Group{ | |
elements: set Element, | |
unit: one elements, | |
mult: elements -> elements -> one elements, | |
inv: elements -> one elements | |
} | |
fact NoRedundantElements{ | |
all e: Element | e in Group.elements | |
} | |
fact UnitLaw1{ | |
all a: Group.elements | Group.mult [a] [Group.unit] = a | |
} | |
fact UnitLaw2{ | |
all a: Group.elements | | |
Group.mult [Group.unit] [a] = a | |
} | |
fact AssociativeLaw{ | |
all a: Group.elements | all b: Group.elements | all c:Group.elements | | |
Group.mult [Group.mult [a] [b]] [c] = Group.mult [a] [Group.mult [b] [c]] | |
} | |
fact InvLaw1{ | |
all a: Group.elements | Group.mult [Group.inv[a]] [a] = Group.unit | |
} | |
assert InvLaw2 { | |
all a: Group.elements | Group.mult [a] [Group.inv[a]] = Group.unit | |
} | |
//check InvLaw2 | |
//run {} | |
assert Commutativity{ | |
all a: Group.elements | all b: Group.elements | Group.mult [a] [b] = Group.mult [b] [a] | |
} | |
assert Anticommutativity{ | |
some a: Group.elements | some b: Group.elements | Group.mult [a] [b] != Group.mult [b] [a] | |
} | |
//check Commutativity for 5 | |
//check Commutativity for 6 | |
//check Anticommutativity for 6 Element | |
//run {} for exactly 6 Element | |
pred subgroup (g: set Element, h: set Element){ | |
(all a: g | a in h) and | |
(Group.unit in g) and | |
(all a, b: g | Group.mult [a] [b] in g) and | |
(all a: g | Group.inv[a] in g) | |
} | |
pred regularSubgroup(n: set Element, g: set Element){ | |
subgroup [n, g] and | |
(all n0: n, g0: g | Group.mult [Group.mult [g0] [n0]] [Group.inv[g0]] in n) | |
} | |
// run {some g: set Element | regularSubgroup [g] [Group.elements]} | |
pred main(n1: set Element, n2: set Element){ | |
let g = Group.elements | | |
regularSubgroup [n1, g] and | |
(some g0: g | (not g0 in n1)) and | |
regularSubgroup [n2, n1] and | |
(some n10: n1 | (not n10 in n2)) and | |
(not regularSubgroup [n2, g]) | |
} | |
//run main for 7 | |
run main for 8 | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment