Summing over a set of util/natural numbers in alloy4

Question

I found myself trying to sum a set of naturals. I was puzzled by the following behavior when running a simple model.

(assume the following code is in a copy of util/natural, so ord is imported)

//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])}
}

then, in a module importing my copy of 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.

Why does changing the scope of Natural affect the result this way?

Answer 1

It seems you just need to disable overflows ("Options -> Forbid Overflows: Yes"), and then it should work as expected. Every time integer arithmetic is used and overflows are allowed (which is the default setting) it possible to get spurious counterexamples (i.e., invalid instances) due to the default "wraparound" semantics of arithmetic operations in Alloy.