Looking at this Stack Overflow question, in response to which @peter.kriens explains that the int bitwidth needs to be set.
This is really horrible, isn’t it? Any way we could mitigate it? For example, set the integer bitwidth always to 5 or more, or set it based on other scoped sigs?
Defaults are dangerous in my opinion, because you may not realize you’re relying on them. I would rather advocate to ask for the explicit setting of the bound on Int as soon as anything Int-related is present in a spec; otherwise a warning or error would be raised. (As a nice-to-have side effect (for the Alloy engine), the default bound on Int would be 0, therefore reducing the size of the domain for specs that don’t need ints).
As often, we disagree David 
I think defaults should provide you with an out of the box experience. When you start with a tool, all the options are bewildering. Forcing people to specify parameters that they have no possibility yet to comprehend is imho not very welcoming.
In this case, as Daniel indicates, the problem is that the default is wrong. We can easily look at the AST and run scope and detect potential problems with integers. Any math with cardinalities implies you need at least be able to represent the cardinality. It is imho better that experts in special cases override it.
I can add a check and generate a warning. However, if there is a support, I can adjust the int width automatically if this seems necessary.
I was a bit sloppy: I’m not against defaults but rather against misleading defaults. And I tend to think defaults other than 0 on ints are problematic in Alloy.
See this (unfinished) conversation.
1 Like