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是任何表達式，評估爲二元關係，應該工作。