Alloy4.2 -二元关系的三元关系

Question

因此，我试图编写一个函数，它接受一组三元关系和一个中间元素，它返回元素匹配的一组关系，但不包含它自己。(我们已经知道它是什么了)

所以就像这样：

// addr gives us: {Book -> Name -> Addr}
fun [n:Name] : Set Book -> Addr {
    //return {b->a} where {b->n->a}
}

使用联接和域限制，我只能设法获得二进制关系：{Book -> Name}和{Name -> Addr}。我不知道如何将这些拼接在一起，因为名字是不变的，所以你不能区分。

是否可以用一个函数来完成这个任务，或者我还需要其他的东西呢？

我完全是这方面的初学者，在一种正常的过程语言中，这似乎相当简单。但是，我找不到很好的文档，在我看来，在函数如何工作的问题上，我完全搞错了。

Answer 1

或者更简单地说：

fun [n:Name]: Book -> Addr {
   {b:Book,a:Addr | b->n->a in addr}
}

然而，您在函数声明中使用的术语“关系集”和关键字"set“使我怀疑您的意思是否不同。请注意，此函数返回一组元组，而不是一组关系。

Answer 2

您可能可以通过理解来计算这个定义：

fun [n:Name]: Book -> Addr {
   {b:Book,a:Addr | b in (addr.a).n }
}