alloy :Declaration do
  enum StateSpace(S1, S2, S3, S4, S5, S6)
  enum Labels(Alpha, Beta, Gamma)
end