transitive closure in alloy

Question

Can any one here explains how the transitive closure operator works in Alloy in terms of the matrix. I mean what's translation rule for translating closure operator into actual matrix operation.

Answer 1

To compute transitive closure, Kodkod uses iterative squaring.

In a nutshell, if you have a binary relation r (which directly translates to a 2-dimensional boolean matrix), transitive closure of r can be computed iteratively as

• r₁ = r or (r . r)
• r₂ = r₁ or (r₁ . r₁)
• r₃ = r₁ or (r₂ . r₂)
• ...
• ^r = r_n = r_n-1 or (r_n-1 . r_n-1)

The question is when do we stop, i.e., what should n be. Since everything is bounded, Kodkod statically knows the maximum number of rows in r, and it should be intuitively clear that if n is set to be that number of rows, the algorithm will produce a semantically correct translation. However, even n/2 is enough (since we are squaring the matrix every time), which is the actual number Kodkod uses.