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.
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
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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With