alloy - 合金中的传递闭包

Question

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

Answer 1

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

简而言之，如果您有一个二元关系r（直接转换为二维布尔矩阵），则传递闭包r可以迭代计算为

• r ₁ = r 或 (r . r)
• r ₂ = r ₁或 (r ₁ . r ₁ )
• r ₃ = r ₁或 (r ₂ . r ₂ )
• ...
• ^r = r _n = r _n-1或 (r _n-1 . r _n-1 )

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