Как обновить установленный размер модели сплава, чтобы он находился в определенном диапазоне?

Если у меня есть модель Alloy в следующем формате

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

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

}

Если я хочу иметь определенное правило, чтобы каждый игрок мог иметь от 1 до 3 позиций. Есть ли способ создать такой прогноз или факт, чтобы сделать это?

Спасибо,


person user2744486    schedule 01.10.2013    source источник


Ответы (1)


Вы можете добавить добавленный факт к player sig, чтобы указать это ограничение. Оператор кардинальности (#) может использоваться для выражения «установленного размера», например,

one sig player {
    name: String,
    spot: set  position
} {
    #position <= 1 && position >= 3
}
person Aleksandar Milicevic    schedule 01.10.2013
comment
Спасибо. Как указать, что позиции одного игрока отличаются друг от друга. Например, если у одного игрока две позиции. Атака одной позиции True. тогда другая позиция не может иметь атаку, чтобы быть Истинной. - person user2744486; 02.10.2013
comment
Могу ли я использовать следующее пред: все n: shippingServiceOptions, m: shippingServiceOptions - n { n.expeditedService не в m.expeditedService } - person user2744486; 02.10.2013
comment
@user2744486 user2744486, возможно, вы захотите задать эти вопросы как новые вопросы; они действительно не являются комментариями к предложенному решению проблемы, которую вы изложили выше. - person C. M. Sperberg-McQueen; 02.10.2013