下面是两个桌面的 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
}
最佳答案
根据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 个元素,因此成功。
关于alloy - 为什么基数约束在运行命令中起作用但在事实中不起作用?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/47802924/