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是任何表达式，评估为二元关系，应该工作。