alloy - 合金中的传递闭合

Question

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

Answer 1

为了计算传递闭包，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 使用的实际数字。