Set the bitwidth when integers are used

[grayswandyr]

When integers are used, not necessarily with explicit constants but also when the # operator is used, when arithmetic operations are used, etc., there is a risk of distortion of results when executing commands, because the bitwidth could be wrong for the problem.

To minimize errors here (in particular for newcomers), I think something should be done:

• either by emitting a reminder warning recalling that the bitwidth should be well thought out
• or by requiring an explicit bitwidth to be set in the scope of commands (and then failing otherwise)

[pkriens]

I fully agree! Last night I was tracing kodkod to figure out if I could detect overflow since it is clearly not detected in a lot of cases. I.e. Int must at least contain the max scope I think or cardinality will fail. seq also requires integers.

I think there are a number of other places where we can optimize integers. I've not seen an AST optimizer that could actually do some constant folding and other optimizations?

I also was wondering if we need negative nrs by default? As long as there are no negative constants nor minus operator in the source then I think we could double our current range and limit to positive numbers?

I wonder if we could also after a solution simulate the integer expressions to see if they are really correctly solved? In that case we can get rid of the solution and try a next solution?

I also do not see where overflow is detected/reported.

[aleksandarmilicevic]

I agree that emitting some friendly warnings is reasonable.

detect overflow since it is clearly not detected in a lot of cases.

File a bug. I'm not aware of any outstanding implementation bugs (i.e., where the implementation doesn't meet the intended semantics), so if you know some, please share them.

I also do not see where overflow is detected/reported.

The semantics of overflow prevention is not about reporting overflows, but instead excluding them from the search space. In other words, to find a satisfying instance, Alloy only considers those instances that satisfy the specification without causing any arithmetic overflows.

Since Alloy does not perform an iterative search over the whole search space and instead it translates the problem into a single SAT problem, the semantics I just described must be encoded in the translation of relational first/higher-order formulas into propositional boolean formulas.

I've not seen an AST optimizer that could actually do some constant folding and other optimizations?

I am not 100% sure, but I think that constant integer expressions (like 2.plus[2]) actually get folded by Kodkod during the translation to boolean circuits, purely as a byproduct of how the translation works: Kodkod allocates symbolic boolean variables only for the symbolic relations present in the formula to be solved, so everything that does not involve any symbolic variables get evaluated to 0 or 1 during that translation.

Int must at least contain the max scope I think or cardinality will fail.

Cardinality won't "fail", it will be unsatisfiable. So yes, when "prevent overflows" is set to true something like

sig S {}
run { #S = 5 } for 2 Int, 5 S

becomes unsatisfiable, because computing the cardinality of a set with 5 elements when max int is 1 results in an overflow, hence that model is discarded. Without overflow prevention (i.e., with wraparound semantics for arithmetic operations), the cardinality of a set with say 5 elements may result in a negative number, which, in many scenarios, is clearly not good. If in the example above int bitwidth is set to 4 (meaning max int is 7), the model becomes satisfiable.

I also was wondering if we need negative nrs by default?

Perfecting defaults is a rat hole and I don't think we should be in that business. What we should do though, is allow the user to specify whatever integers they want to use; currently, unfortunately, the user can only specify the bitwidth and Alloy then uses all integers within that bitwidth. Alloy* provides somewhat more flexibility in that respect, so there it is possible to write something like for 0..10 Int.

I wonder if we could also after a solution simulate the integer expressions to see if they are really correctly solved? In that case we can get rid of the solution and try a next solution?

That would likely be super inefficient compared to the current implementation: the current implementation translates the whole problem into a single propositional formula and hence invokes the SAT solver exactly once, whereas your approach could take arbitrarily many SAT invocations before it concludes.

[pkriens]

I think we should consider the 2 cases of expert users and newbies. My main concern with Alloy is at the moment that you need to understand a lot before you can use it. I.e. it requires a pilot license to operate. This turns away a lot of potential users that would be willing to learn but need something to work before the can start learning.

I would prefer a strategy:

• Work out of the box with decent defaults. Most people start with very simple models.
• When models fail, try 'learning' strategies while telling people where the time is spend so they see how they can tune their model.
• Warn about anything fishy with good messages
• Provide tuning knobs

[aleksandarmilicevic]

it requires a pilot license to operate.

Indeed, if you want to fly a plane, you should get a pilot license first.

Now, I'm not the one saying that Alloy is as difficult to use as operating a plane, but if you think that, then getting a license first seems warranted.

• Work out of the box with decent defaults. Most people start with very simple models.

Done. That's how it already works. Using ints from -8 to 7 is a decent default. Now anyone can start arguing that a better default would be to use -2..17, or 0..34, or whatever, and that's the rat hole I was talking about.

• When models fail, try 'learning' strategies while telling people where the time is spend so they see how they can tune their model.

Sounds great. Now you just need to define what a "learning" strategy is, what exactly to do with it, and how to actually implement it.

And yes, models cannot fail, they can be satisfiable or unsatisfiable.

• Warn about anything fishy with good messages

Done: Alloy already warns about a bunch of things. There are certainly more things Alloy could warn about, and I was never opposed to it.

• Provide tuning knobs

Done: look at the plethora of existing options you can already set. If there are other concrete tuning knobs we should provide, we should discuss them one at a time, in separate discussions.

[aleksandarmilicevic]

Should we close this now that integers are always used by default?

[pkriens]

Yup, though I will create an issue to move the overflow option to a pragma. After our discussion I feel very uncomfortable how a user setting can influence the meaning of the specification.

[grayswandyr]

+1 for creating a pragma for every such decision.

Now I stand by my initial issue as I fail to see how the decisions made at the FoA workshop will address the fact that it's easy for beginners but also experienced users to forget to set the bitwidth in a scope. I still think that emitting a warning message would be useful.

Perhaps it won't be useful if, as talked about at the end of the workshop, it becomes possible to write "for ? Int" and let the analyzer find a bound by itself, but I think even this would only be possible with an SMT solver, not a SAT one. So I'd advocate for reopening this issue.

[pkriens]

Well, the problem that became clearer to me is that the key issue is that the current default int width is so low that it causes havoc. (I.e. it is often so small it cannot represent the cardinality of the sets.)

With SMT solvers we should be able to get large integers so that will get rid of the primary problem. For SAT solvers we might increase the int width to provide some breathing room. We could then print a message if the solve is aborted or takes more than n seconds that the integer width could be too high and reducing it might increase the speed of finding a solution.

I think most newcomers have small simple problems where the int width is not that relevant for the resolution time?

That said, it would be nice if the default was adjusted to hold at least any constant and any sig cardinality from the scope?

Thinking a bit more about ints I wonder if they really should be part of the scope at all. After our discussion it is clear that they are fundamentally different from finite sets of atoms. Maybe requiring Ints to be expressly declared would address your problem? E.g:

 sig Int { 0..100 }

(I always found setting the 'width' of the Int very weird since it requires an unnecessary understanding of a messy detail.)

[grayswandyr]

It's not a problem of resolution time. Alloy will very quickly realize that a spec is inconsistent :-)

Besides, Cesare seemed to think that large integers can also be a problem with SMT, even if less stringent than with SAT. Secondly, SAT solvers have their own interest and will not be removed.

Sure, the idea of setting a bound large enough to hold any constant is a minimum. But I would rather address this in the following way:

1. Every spec featuring integers should set the Int scope in the command, otherwise a warning should be issued (just a warning, so it would still be possible to execute the command)
2. An Int scope not large enough to hold all integer constants explicitly present in the model should yield another warning (or even an error?).

Finally I think that the Int scope should be fixed in commands: your spec should in principle be independent from the bounded semantics because we may use other verification techniques that work in an unbounded setting.

(I can't reopen the issue by myself, would you do it?)