util/Natural unexpected behavior in alloy

Question

I tried the following snippet of Alloy4, and found myself confused by the behavior of the util/Natural module. The comments explain more in detail what was unexpected. I was hoping someone could explain why this happens.

module weirdNatural
private open util/natural as nat

//Somehow, using number two obtained from incrementing one works as I expect, (ie, there is no 
//number greater than it in {0,1,2}. but using number two obtained from the natrual/add function
//seems to work differently. why is that?

let twoViaAdd = nat/add[nat/One, nat/One]
let twoViaInc = nat/inc[nat/One]

pred biggerAdd {
    some x: nat/Natural | nat/gt[x, twoViaAdd]
}

pred biggerInc {
    some y: nat/Natural | nat/gt[y, twoViaInc]
}

//run biggerAdd for 10 but 3 Natural //does not work well, it does find a number gt2 in {0,1,2}
run biggerInc for 10 but 3 Natural //works as expected, it finds a number gt2 in {0,1,2,3}, but not in {0,1,2}

Answer 1

Thanks for this bug report. You are absolutely right, that is a weird behavior.

Alloy4.2 introduced some changes to how integers are handled; namely, the + and - operators in Alloy4.2 are always interpreted as set union/difference, so built-in functions plus/minus have to be used to express arithmetic addition/subtraction. On the other side, the util/natural module (mistakenly) hasn't been updated to use the latest syntax, which was the root cause of the weird behavior you experienced (specifically, the nat/add function uses the old + operator instead of plus, whereas nat/inc doesn't).

To work around this issue, you can either

• 1. open the util/natural module (choose "File -> Open Sample Models" from the main menu)
  2. edit the file and replace the two occurrences of <a> + <b> with plus[<a>, <b>]
  3. save the new file in the same folder with your model als file (e.g., as "my_nat.als")
  4. open it from your main module (e.g., open my_nat as nat)

or

• download the latest unofficial version where this bug is fixed (you might need to manually delete the Alloy temp folder to make sure that the Alloy Analyzer is not using the old (cached) version of the util/natural library).