alloy - 合金中的传递闭合

这里的任何人都可以解释传递闭包运算符如何根据矩阵在 Alloy 中工作。我的意思是将闭包运算符转换为实际矩阵运算的转换规则是什么。

最佳答案

为了计算传递闭包，Kodkod 使用迭代平方。

简而言之，如果你有一个二元关系 r(它直接转换为一个二维 bool 矩阵)，那么 r 的传递闭包可以迭代计算为

r1 = r 或 (r . r)

r2 = r1 或 (r1 . r1)

r3 = r1 或 (r2 . r2)

...

^r = rn = rn-1 或 (rn-1 . rn-1)

问题是我们什么时候停止，即 n 应该是什么。由于一切都是有界的，Kodkod 静态地知道 r 中的最大行数，并且直观上应该很清楚，如果 n 设置为该行数，算法将产生语义正确的翻译。然而，即使是 n/2 也足够了(因为我们每次都对矩阵进行平方)，这是 Kodkod 使用的实际数字。

关于alloy - 合金中的传递闭合，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/14483418/