了解合金基数答案

【问题标题】：Understanding Alloy cardinality了解合金基数
【发布时间】：2015-03-26 20:37:39
【问题描述】：

我无法理解合金基数。我将我的代码简化为这个 Alloy 找不到实例的简单示例：

sig A {}
sig B { s: set A}

fact x { one n: Int  | all b: B | #(b.s) = n }
run {} for 10

也就是说，B.s 的基数对于 B 的所有成员都必须相同。为什么 Alloy 找不到这样的例子？

【问题讨论】：

标签： alloy

【解决方案1】：

如果您将run 命令更改为run {} for 10 but 5 int，您应该会开始看到实例。

这并不是一个真正令人满意的答案（我希望 Alloy 团队的一位成员可以做得更好），但看起来直接的问题是，虽然 Int 是内置的，但它并不总是被实例化。当没有 Int 的实例时，不能满足事实。（注释掉事实，生成一个实例，然后让 Evaluator 评估表达式 Int。当我这样做时，评估器返回 {}。）

我很乐意更好地解释这一点，但我还没有成功地找到或发现决定何时生成 Int 原子以及何时不生成的规则。

【讨论】：

【解决方案2】：

在“选项”中，您可以将消息详细程度设置为“高”。在那里，当您运行命令时，您会看到位宽（决定 Alloy 的最大 Int）为 0。默认情况下，它曾经是 4，我不确定发生了什么。

正如另一个答案所建议的，将 Int 设置为某个值会增加位宽，因此会增加 Alloy 允许的最大 Int。

在 Alloy 中确实不鼓励使用 Int。这是一种编写相同语句的方法，避免使用 Int：

sig A {}
sig B { s: set A}

fact x { all b,b2: B | #(b.s) = #(b2.s) }
run { some B.s and #B>1} for 10

我在 run 语句中添加了一些内容，只是为了查看一些有趣的实例

【讨论】：