合金4.2的语义变化对合金书的练习A.1.6的影响？-Java 学习之路

根据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上执行的相同代码 .

1 回答

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

当您明确为Int提供范围时，Universe肯定会包含给定范围内的所有Int原子 . 如果另外没有用户定义的sigs，你最终也会得到合成的Univ sig . 当显式使用Int的范围时，合成Univ sig是否有意义是有争议的 .

要解决您的问题，您有以下几种选择：
- 如果您不关心图形节点的类型（即，您没有明确希望节点是Ints），那么您只需更改run命令即可
run show for 3 而不是 run show for 3 Int .

如果你这样做，你就像Univ sig一样，只需引入一个新的sig，例如 sig Node {} ，在这种情况下，所有原子的类型都是 Node .
- 如果您确实希望图表仅在Ints上，则可以在所有谓词中将 univ->univ 更改为 Int->Int .
- 如果您确实希望Universe只包含Int原子（在这种情况下，您可以在谓词中保留 univ->univ ），则可以引入虚拟签名并添加一个确保其基数为零的事实 .
```
sig Dummy {}
fact { no Dummy }
```
这一小改动将确保Univ sig不会自动合成，不会影响您的其他模型 .

希望这可以帮助 .
回复于 2024-04-24T22:26:36+08:00

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

1 回答

相关问题