KodKod 中的传递闭包

Question

我在使用关系方法 closure() 时遇到问题。如果有人可以解释传递闭包在 KodKod 中是如何工作的。

举个例子：

Relation r1 = Relation.nary("r1",4);
Relation r2 = Relation.binary("r2");
Relation i = Relation.unary("i");
Relation j = Relation.unary("j");
Formula f = r.in(r2.product(i).product(j));

我想知道怎么说：变量 k Oneof(j) 不在关系 r1

的传递闭包中

Answer 1

你的例子中的关系 r1 的元数是 4，传递闭包只能应用于二元关系。

假设 r1 是二元的，类似于 k.in(r1.closure()).not()，其中 k 是计算为二元关系的任何表达式，应该有效。

KodKod 中的传递闭包

Transitive closure in KodKod

alloy