alloy - 对合金4中的一组效用数/自然数求和

Question

我发现自己试图总结一组自然值。运行简单模型时，我对以下行为感到困惑。

（假设以下代码在 util/natural 的副本中，所以导入了 ord）

//sums the values in a set of naturals
fun setsum[nums : set Natural] : lone Natural {
    {n : Natural | #ord/prevs[n] = (sum x : nums | #ord/prevs[x])}
}

然后，在导入我的 util/natural 副本的模块中：

private open mynatural as nat

let two = nat/add[nat/One, nat/One]
let three = nat/add[two, nat/One]
let four = nat/add[two, two]
let five  = nat/add[four,nat/One]

pred showExpectSum10 {
    some x : Natural | x in setsum[{n : Natural | nat/lt[n, five]}]
}

//run showExpectSum10 for 15 //result is 10, as expected
//run showExpectSum10 for 1 but 20 Natural //result is 10  as expected
run showExpectSum10 for 1 but 40 Natural //result is 26 somehow.

为什么更改 Natural 的范围会以这种方式影响结果？

Answer 1

看来您只需要禁用溢出（“选项 - > 禁止溢出：是”），然后它应该按预期工作。每次使用整数运算并允许溢出（这是默认设置）时，由于 Alloy 中算术运算的默认“环绕”语义，可能会得到虚假的反例（即无效实例）。