私は次のように少し合金の仕様を持っています：
sig class {parents : set class}
fact f1{all p:class | not p in p.^parents}
run{} for exactly 4 class
最初に、alloyはf1をブール行列に変換し、次にそれに対してクロージャ操作を実行すると思いました。しかし、この種の変換は行わないようです（ブール行列の作成前に何かを実行しているように見えます）。では、このf1はどのように正確に翻訳されるのでしょうか？関係述語を使用していますか？私は合金の翻訳について非常に興味があります。
ブール行列は、Alloyの式を表すために使用されます。したがって、各sigの単項行列、各2項関係の2項行列、各3項関係の3項行列などから始めます。次に、「複雑な」式の変換（たとえば、リレーショナル代数演算子を含む）は、開始した行列を操作（構成）することによって行われます。各Alloy演算子（たとえば、推移閉包（^）、関係結合（。）、in、notなど）には、その演算子のセマンティクスが正しく実装されるように、一連の行列演算を実行する対応するアルゴリズムがあります。
したがって、この例では、all数量詞が最初に展開されます。つまり、pタイプclassの各アトムについて、本体が変換されます（次のようなもの）。
）、そして最後に、これらの本文の翻訳はすべてANDされます。