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产生一个或两个组元素。