// The Alloy specification used to identify all groups of order 8

sig Element {}

sig Group {
	elements: set Element,
	unit: elements,
	mult: elements -> elements ->one  elements,
	inv: elements -> elements
} { all a,b,c : elements | c.((b.(a.mult)).mult)=(c.(b.mult)).(a.mult)
all a: elements | a = unit.(a.mult) && a = a.(unit.mult)
all a: elements | unit = a.((a.inv).mult) && (a.inv).(a.mult) = unit

// all a: elements | unit = (a.(a.mult)) . ((a.(a.mult)).mult)

}

pred AGroup [G: Group] {
	# G.elements = 8
} run AGroup for 8 but 1 Group, 5 int