Domanda

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?

È stato utile?

Soluzione

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
}
Autorizzato sotto: CC-BY-SA insieme a attribuzione
Non affiliato a StackOverflow
scroll top