alloy - 合金の推移閉包

Question

ここで誰かが、マトリックスの観点から、Alloyで推移閉包演算子がどのように機能するかを説明できますか？つまり、閉包作用素を実際の行列演算に変換するための変換規則は何ですか。

Answer 1

推移閉包を計算するために、Kodkodは反復二乗を使用します。

一言で言えば、二項関係r（2次元ブール行列に直接変換される）がある場合、の推移閉包は次のrように反復的に計算できます。

• r ₁ = rまたは（r。r）
• r ₂ = r ₁または（_{r1。r1 ）}
• r ₃ = r ₁または_（r2。r2）
• ..。
• ^ r = r _n = r n _-1または（rn _{- 1。rn-1}）

問題は、いつ停止するか、つまり何をすべきかというnことです。すべてが制限されているため、Kodkodは静的に最大行数を認識します。がその行数に設定されている場合、アルゴリズムは意味的に正しい変換を生成することをr直感的に理解する必要があります。nただし、n/2Kodkodが実際に使用する数である（毎回行列を2乗しているため）でも十分です。