【发布时间】：2013-01-07 03:37:20
【问题描述】：
这里的任何人都可以解释传递闭包运算符如何根据矩阵在合金中工作。我的意思是将闭包运算符转换为实际矩阵运算的转换规则。
【问题讨论】：
标签： alloy
【发布时间】：2013-01-07 03:37:20
【问题描述】：
为了计算传递闭包，Kodkod 使用迭代平方。
简而言之，如果你有一个二元关系r（直接转换为二维布尔矩阵），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 使用的实际数字。
【讨论】：
-
还有一个问题，如果我有 c^.contents，计算传递闭包的输入矩阵是什么？假设 c 是签名 C 的一种类型，那么输入矩阵是什么？
-
我的意思是，如果我在 c^.contents 中说 c，那么如何确保 c 出现在传递闭包矩阵中？
-
c在计算contents的传递闭包时无关紧要。要求contents是二元关系，然后^contents像我之前描述的那样计算，最后计算c和^contents之间的简单连接。 -
其实连
ceiling(log_2(n))的界限就够了。