Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

transitive closure in alloy

Tags:

alloy

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.

like image 313
user1197891 Avatar asked Feb 18 '23 18:02

user1197891


1 Answers

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

  • r1 = r or (r . r)
  • r2 = r1 or (r1 . r1)
  • r3 = r1 or (r2 . r2)
  • ...
  • ^r = rn = rn-1 or (rn-1 . rn-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.

like image 53
Aleksandar Milicevic Avatar answered May 16 '23 06:05

Aleksandar Milicevic