Create a gist now

Instantly share code, notes, and snippets.

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