矢印演算子を使用して作成された関係のAlloy Visualizerの表示の理解

Question

矢印（製品）演算子を理解するために、私はWhitePagesのモデルを作成しました。各白いページには名前からアドレスへのマッピングがあります（この名前/アドレスマッピングは矢印演算子を使用します）。私は、白いページの名前/アドレスマッピングを示す述語を作成しましたw。私が指定した述語では、名前/アドレスの関連付けの数は3です。以下のモデルを参照してください。

矢印演算子の定義によれば、Name-> Address関係には名前とアドレスのすべての組み合わせが含まれます。

のように見えていないこと：

驚くべきことに、その代わりに、ビジュアライザーはこれを与えた：私はそれを見るように、唯一の可能なインスタンスがあります私には有効なインスタンスです。名前/住所のマッピングはどこですか？

sig WhitePages { 
    address: Name->Address 
} 

sig Name {} 

sig Address {} 

pred Show (w: WhitePages) {#w.address = 3} 

run Show 

Answer 1

アドレスに投影したので、各アドレスごとに1つのスナップショットが作成されます。下部にUIコントロールが表示され、アドレスを選択できるようになります。制約によって、名前とアドレスの関係に3つのペアがあることがわかるため、異なるアドレスに分散させることができます。