You can add an appended fact to the player
sig to specify that constraint. The cardinality operator (#
) can be used to express the "set size" e.g.,
one sig player {
name: String,
spot: set position
} {
#position <= 1 && position >= 3
}