3

根据 Alloy 4.2 的发行说明，存在与整数相关的语义更改。这些变化似乎对 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 上执行的代码不同。

4

1 回答 1

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 不会自动合成，并且不会影响模型的其余部分。

希望这可以帮助。

于 2012-10-02T15:47:04.610 回答