alloy - 如何更新合金模型的设定尺寸在一定范围内？

Question

如果我有以下格式的合金模型

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

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

}

如果我想制定一个规则，让每个玩家可以有 1 到 3 个位置。有没有办法创建这样的预测或事实来做到这一点？

谢谢，

Answer 1

您可以将附加事实添加到playersig 以指定该约束。基数运算符 ( #) 可用于表示“集合大小”，例如，

one sig player {
    name: String,
    spot: set  position
} {
    #position <= 1 && position >= 3
}