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

Question

下面是两个桌面的Alloy表示.在fact我指定第一个桌面包含两个图标,A和B,第二个桌面包含一个图标,A.我想指定正好有两个桌面,所以我把它放在以下事实中:

#Desktop = 2

当我完成run命令时,我收到了这条消息:No instance found.当我从而省略fact了该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

根据Alloy Reference的第283页,如果没有为签名指定显式绑定并且找不到隐式绑定,则该签名默认最多为 3个元素.run {#Desktop = 3}默认情况下有效.

你也有open util/ordering[Desktop].该模块以#开头module util/ordering[exactly elem],将exactly约束添加到范围.这意味着隐式绑定恰好是 3个元素,因此run {#Desktop = 2}失败.将run {#Desktop = 2} for 2每个签名的隐式绑定更改为2个元素,因此成功.