Alloy - 1 oder 2 Variablen deklarieren

Question

Ich möchte in der Lage sein, eine oder zwei Variablen des gleichen Typs aus einer Gruppe namens group zu deklarieren. Ich weiß, dass one und lone verwendet werden können, um jeweils eine oder null/eine Variablen zu deklarieren. Mein bisheriger Versuch ist:

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

Dies scheint jedoch nicht zu funktionieren. Mein Ziel ist es, entweder eine oder zwei Variablen zu haben, die ich dann im folgenden Ausdruck verwenden kann.

Answer 1

Es könnte hier Verwirrung geben. Wenn Sie one x:group| expr schreiben, bedeutet dies, dass es genau ein x in der Gruppe geben sollte, so dass der Ausdruck expr gilt.

Wissen, wenn Sie diese Art von Einschränkung ausdrücken möchten, könnten Sie etwas wie diese schreiben: z. vorausgesetzt, es gibt ein Feld size beschreibt eine Beziehung group-Int, Ausdruck, dass mindestens ein und höchstens zwei Gruppen haben eine Größe von 5 wie folgt in diesem Beispiel genannt ist

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

getan werden kann, x+y werden Je nachdem, ob x=y oder nicht, ergeben sich ein oder zwei Gruppenelemente.