formal-methods - 合金 4.2 语义变化对合金书练习 A.1.6 的影响？

Question

根据release notes对于 Alloy 4.2，存在与整数相关的语义变化。这些更改似乎对合金书的练习 A.1.6 有影响。

在本练习中，给出了以下代码作为基础(我在最后添加了“Int”以显示我的问题)。运行“show”谓词时，可视化工具会显示一个实例，但该实例除了包含整数外，还包含另外两个原子“Univ0”和“Univ1”。

module exercises/spanning

pred isTree(r: univ->univ) {}
pred spans(r1, r2: univ->univ) {}

pred show(r, t1, t2: univ->univ) {
    spans[t1,r] and isTree[t1]
    spans[t2,r] and isTree[t2]
    t1 != t2
}
run show for 3 Int

“Univ0”和“Univ1”这两个原子是什么意思？他们为什么在那里？它们不会出现在 Alloy 4.1.10 上执行的相同代码。

Answer 1

当没有用户定义的 sig 时，Alloy 会自动合成一个名为“Univ”的新 sig。这是一个方便的功能，因为它允许您在整个宇宙中编写公式而无需引入任何信号。

当你显式地给 Int 一个作用域时，那么宇宙一定会包含给定作用域内的所有 Int 原子。如果另外没有用户定义的 sig，您最终也会得到合成的 Univ sig。当显式使用 Int 的范围时，合成 Univ sig 是否有意义是值得商榷的。

要解决您的问题，您有多种选择:

1. 如果您不关心图形节点的类型(即，您不明确希望节点是 Ints)，那么您只需将运行命令更改为 say

   run show for 3 而不是 run show for 3 Int。

   如果这样做，您将没有 Int 原子，只有 Univ 原子。如果您不喜欢 Univ sig，只需引入一个新的 sig，例如 sig Node {}，在这种情况下，所有原子的类型都是 Node。

2. 如果您真的希望您的图表仅包含 Ints，您可以将所有谓词中的 univ->univ 更改为 Int->Int。

3. 如果你真的希望你的宇宙只包含 Int 原子(在这种情况下你可以在你的谓词中保留 univ->univ)，你可以引入一个虚拟签名并添加一个事实确保其基数为零。

   sig Dummy {}
   fact { no Dummy }
   

   这个小改动将确保 Univ sig 不会自动合成，也不会影响您模型的其余部分。

希望这对您有所帮助。