Search code examples
verificationalloyformal-verification

A predicate which holds for at most 2

I want to write a predicate which holds for at most two items.

I tried doing one x,y: Object | However this did not give the desired result

I then tried one x,y: Object | x != y However this gave no instances

I was thinking of something along the lines of

some .. { one.. }

Any help would be appreciated

Solution

  • one forces there to be only one atom, but x, y is two. One way to do this would be some disj x, y: Object | no z: Object - x - y | ...