Alloy - 聲明1或2個變量

Question

我希望能夠從名爲group的集中聲明一個或兩個相同類型的變量。我知道one和lone可以用來分別聲明一個或零個/一個變量。我到目前爲止的嘗試是：

one x : group, lone y : from | {...} 

但是，這似乎並不奏效。我的目標是有一個或兩個變量，然後我可以在下面的表達式中使用。

Answer 1

這裏可能會有困惑。 如果你寫one x:group| expr這意味着組中應該只有一個x，所以表達式expr成立。知道了這一點，如果你想表達這種約束，你可以寫下這樣的文字： 例如，假設有一個名爲size描述到Int從group的關係 一個字段，表達的至少一個和最多兩個基團具有的大小爲5可以如下

one x,y : group | (x + y).size=5 

在這個例子中，x+y將完成根據是否x=y產生一個或兩個組元素。