了解合金展示台对使用箭头运算符创建的关系的显示

Question

为了帮助我了解箭头（产品）运算符，我创建了一个WhitePages模型。每个白页都有从名称到地址的映射（该名称/地址映射使用箭头运算符）。我创建了一个谓词来显示白名单的名称/地址映射w。在我指定的谓词中，名称/地址关联的数量为3.请参见下面的模型。

根据箭头运算符的定义，名称 - >地址关系包含名称和地址的所有组合。所以，在我看来，只有一种可能的情况：

出人意料的是，取而代之的是，展示台给这个：

这看起来并不像一个有效的实例给我。名称/地址映射在哪里？

sig WhitePages { 
    address: Name->Address 
} 

sig Name {} 

sig Address {} 

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

run Show 

Answer 1

您将它投影到地址上，因此您现在每个地址都有一个快照。你会在底部看到一个UI控件，让你选择地址。请注意，您的约束表明，名称 - 地址关系中有3对，因此它们可以分布在不同的地址中。