在 Alloy 中对二元关系使用集合理解

Question

我有以下签名：

sig Id, Grade {}

sig Foo {
    result : Id -> Grade
}

现在我想创建一个接受 foo 变量和 returns 所有关联 Foo -> Grade 关系的函数：

fun results[ id : Id ]: Foo -> Grade {
    //return all Foo->Grade binary relationships such that "id -> grade" in Foo.result
}

即

所以如果 "result" 关系是这样的：

(foo0, id0, grade0)
(foo0, id1, grade0)
(foo0, id2, grade1)
(foo1, id0, grade2)
(foo1, id3, grade3)
(foo2, id0, grade0)

我运行函数 "results[ id0 ]" 我会得到：

(foo0, grade0)
(foo1, grade2)
(foo2, grade0)

现在我想我会使用某种集合推导，但问题是集合推导仅适用于一元集合，不适用于二元集合。

Answer 1

Now i guess I would use some sort of set comprehension, but the issue is that set comprehension only works with unary sets, not binary sets.

第一次正确（是的，使用集合推导），第二次不太正确（集合推导可以很好地处理关系）。请参阅语言参考的 B.8 节，或 Software Abstractions.

的 3.5.5

尝试这样的操作（未选中！）：

fun results[ id : Id ]: Foo -> Grade {
/* return all Foo->Grade binary relationships
   such that "id -> grade" in Foo.result */
   { f : Foo, g : Grade 
     | f -> id -> g in result } 
   /* not Foo.result, that was a slip */
}

可能有一种聪明的方法可以在没有理解的情况下编写所需的集合，只需使用方框连接和点连接，但如果有的话，目前我还不知道。我得到的最接近的是

{ f : Foo, g : Grade | f.result.g = id }

在 Alloy 中对二元关系使用集合理解

Using set comprehension on binary relationships in Alloy

alloy