alloy - 为什么基数约束在运行命令中起作用但在事实中不起作用？

Question

下面是两个桌面的 Alloy 表示。在 fact 中，我指定第一个桌面包含两个图标 A 和 B，第二个桌面包含一个图标 A。我想指定正好有两个桌面，所以我将事实上:

#Desktop = 2

当我执行run命令时，我收到以下消息:未找到实例。当我从事实中省略这一点并在 run 命令中指定桌面数量时:

run {} but 2 Desktop

然后就生成了所需的实例。为什么？为什么当我在 fact 中限制桌面数量时它不起作用，但当我在 run 命令中限制桌面数量时它却起作用？

open util/ordering[Desktop]

sig Desktop {
     icons: set Icon
} 

abstract sig Icon {}
one sig A extends Icon {}
one sig B extends Icon {}

fact {
    first.icons = A + B
    first.next.icons = A
}

Answer 1

根据page 283 of the Alloy Reference ，如果没有为签名指定显式绑定(bind)并且找不到隐式绑定(bind)，则该签名默认为至多 3 个元素。 run {#Desktop = 3} 默认情况下有效。

您还可以打开 util/ordering[Desktop]。该模块以 module util/ordering[exactly elem] 开头，它将 exactly 约束添加到范围中。这意味着隐式绑定(bind)正好 3 个元素，因此 run {#Desktop = 2} 失败。添加 run {#Desktop = 2} for 2 将隐式绑定(bind)更改为每个签名 2 个元素，因此成功。