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
- open the util/natural module (choose "File -> Open Sample Models" from the main menu)
- edit the file and replace the two occurrences of
<a> + <b>
withplus[<a>, <b>]
- save the new file in the same folder with your model als file (e.g., as "my_nat.als")
- 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).