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

【问题标题】：Why does a cardinality constraint work in a run command but not in a fact?为什么基数约束在运行命令中起作用，但实际上不起作用？
【发布时间】：2018-05-27 22:15:20
【问题描述】：

下面是两个桌面的合金表示。在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
}

【问题讨论】：

标签： alloy

【解决方案1】：

根据page 283 of the Alloy Reference，如果没有为签名指定显式绑定并且找不到隐式绑定，则该签名默认为最多 3 个元素。 run {#Desktop = 3} 默认工作。

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

【讨论】：

嗨@Hovercouch。再次感谢。让我看看我是否理解：限制 sig 成员数量的一种方法是在声明 sig 时，例如，一个 sig Foo {}。限制 sig 成员数量的唯一其他方法是在运行命令中，例如，run for 3 but 1 Foo。 sig 的成员数量不能被 pred 或 fact 限制，例如，这是非法的：#Foo = 1。对吗？
您可以限制事实中的数字。例如，您可以使用fact {#Foo = 1}。然后run for 3 将允许最多三个每个 sig，但恰好一个 Foo。这里的问题是ordering 模块会自动将exactly 添加到您传入的任何内容中。
啊！感谢您的解释。因此，冲突在于我声称（在事实段落中）桌面数量为 2 而订购模块声称正好有 3 个桌面。杰出的！谢谢@Hovercouch！