CODEWITHSUNDEEP
variablesexpressionalloy
LEJ
LEJ

Reputation: 1958

Alloy - Declare 1 or 2 variables

I would like to be able to declare one or two variables of the same type from a set called group. I know that one and lone can be used to declare one or zero/one variables respectively. My attempt so far is :

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

However, this doesn't appear to work. My aim is to have either one or two variables that I can then use in the following expression.

Upvotes: 0

Views: 311

Answers (1)

Loïc Gammaitoni
Loïc Gammaitoni

Reputation: 4171

There might be confusion here. If you write one x:group| expr this means that there should be exactly one x in group so that the expression expr holds.

Knowing this, if you want to express that kind of constraint, you could write something like this : e.g. assuming there is a field named size describing a relation from group to Int, Expressing that at least one and at most two groups have a size of 5 can be done as follows

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

In this example, x+y will yield one or two group elements depending on whether x=y or not.

Upvotes: 2

Related Questions