alloy - 合金 - 移除对象时获取空集

Question

考虑合金中的以下规范：

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

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

假设我们有一个实例 $univ = {Books$0, Books$1, Books$2}$。用 $Books$0$ 评估函数 f 会产生空集而不是 ${Books$1, Books$2}$：

f[Books$0]
{}

任何想法为什么？

Answer 1

这是因为集合理解的工作方式。

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

这个表达式提供了所有等于的单例子集。但是是一个二元集。所以没有单例集等于它，整体结果是.BooksBooks - bBooks - b{}

您可能只是想要：

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