Home Articles

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

Asked
Viewed 763 times
3

根据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 Answer

  • 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不会自动合成,不会影响您的其他模型 .

    希望这可以帮助 .

Related