Alloy 4.2的语义变化对Alloy书的练习A.1.6的影响？

Question

根据Alloy 4.2 的release notes，存在与整数相关的语义变化。这些变化似乎对 Alloy 书的练习 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），那么您可以简单地将运行命令更改为说

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

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

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

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

   sig Dummy {}
   fact { no Dummy }
   

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

希望这会有所帮助。