Question

If I have an Alloy model in the following format

one sig player {
    name: String,
    spot: set  position
}

sig position {
    Attack: Bool,
    accuracy: int,
    strength: int,

}

If I want to have a cetain rule such that each player can have 1 to 3 positions. Is there a way to create such a prediction or fact to do this?

Thanks,

Was it helpful?

Solution

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
}
Licensed under: CC-BY-SA with attribution
Not affiliated with StackOverflow
scroll top