Alloy - Get empty set when removing object

1
votes

Consider the following specification in Alloy:

sig Books {}
fun f[b:Books] : Books {

    {b':Books | b' = Books -b }
}
run show {}

Suppose we have got an instance for which $univ = {Books$0, Books$1, Books$2}$. Evaluating function f with $Books$0$ yields the empty set instead of ${Books$1, Books$2}$:

f[Books$0]
{}

Any ideas why?

1
alloy

1 Answers

3
votes

It is because of the way set comprehension works.

{b':Books | b' = Books - b }

This expression delivers all the singleton subsets of Books which are equal to Books - b. But Books - b is a two-element set. So no singleton set is equal to it and the overall result is {}.

You probably simply want:

fun f[b:Books] : Books {
   Books - b
}