根据合金4.2的release notes，存在与整数有关的语义更改。这些变化似乎对《合金》一书的练习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上执行的代码不同。
最佳答案
当没有用户定义的信号时，Alloy将自动合成一个称为“ Univ”的新信号。这是一项方便的功能，因为它使您可以在整个宇宙中编写公式，而不必引入任何信号。
当您明确给出Int的作用域时，则该Universe当然将包含给定范围内的所有Int原子。如果另外没有用户定义的信号，则最终也将具有合成的Univ信号。当明确使用Int的作用域时，综合Univ sig是否有意义尚有争议。
要变通解决此问题，您有几种选择：
如果您不关心图形节点的类型是什么（即您不明确希望这些节点为Ints），则可以简单地更改run命令以说run show for 3代替run show for 3 Int。
如果这样做，将没有Int原子，只有Univ原子。如果您不喜欢Univ信号，只需引入一个新信号，例如sig Node {}，在这种情况下所有原子都将为Node类型。
如果您确实希望图形仅位于Ints上，则可以在所有谓词中将univ->univ更改为Int->Int。
如果您确实希望您的宇宙仅包含Int原子（在这种情况下，您可以在谓词中保留univ->univ），则可以引入虚拟签名并添加一个事实，以确保其基数为零。
sig Dummy {}
fact { no Dummy }
这个很小的变化将确保Univ信号不会自动合成，并且不会影响模型的其余部分。
希望这可以帮助。