Systematic inclusion of integers in univ and unclear default bound

[jbrubru]

Some aspects of the treatment of integers need clarification / improvement:

• Integers are systematically included in univ, even when they are not used in the model.
• The default bound for (the bitwidth of) Int is 4 (instead 3 for the other sigs). The user should be aware of this somehow.
• In the textual representation of an instance, integers appear twice: "integers" and "Int".
• It is possible to reason about constant integers that are above the bound of Int. For instance,

sig Foo {}
run {#Foo = 3} for 2 Int

yields an instance. This is cool but I'm not sure this is explained somewhere.

[tnelson]

I can look into this, but probably only once the Spring 2023 semester is over.

Note that the example above only yields an instance if "prevent overflows" is disabled. So perhaps we're reasoning about, not 3, but "some value congruent to 3".
We can confirm this with an experiment:

sig Foo {}
run {#Foo = 5} for 2 Int

which produces instances with 1 Foo atom. If we increase the bound:

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

we get instances with both 1 and 5 Foo atoms.

[alcinocunha]

Indeed it seems that the example is behaving correctly according to the wrap-around semantics of integers (without the prevent overflows). 3 is actually -1 with the bitwidth of 2 and if we ask in the evaluator for the value of #Foo it returns -1. Likewise if we ask for the value of 3. So, I don't think the last point is an issue, but just the normal behaviour taking into account Alloy's integer semantics.

However, I think there is an issue when we explicitly state that we want a scope of 0 for Int. In the evaluator if we ask for the value of #Foo it returns 3, but if we ask for the value of 3 it returns {}. The latter is the expected, but the former is inconsistent with the specified bitwidth. I did some experiences and, when the scope of Int is 0, the Analyzer is still using a bitwidth of 3 for computing the cardinality, but I think it should use the bitwidth specified in the scope. The consequence of that in this particular example would be that the formula #Foo = 3 would be trivially true and Foo could have any number of atoms. Btw, some other operators are defaulting to a bitwidth of 3 when the scope of Int is 0, namely the comparison operators, so the issue is not only with cardinality. Again I think the behaviour of all operators involving integers should be consistent with the specified scope for Int.

This is related to the first and second points: we could default default the scope of Int to 0 (instead of the current 4), but then the user should be aware that operators like cardinality will have a "strange" behaviour. Maybe we could issue a warning if the user uses any arithmetic operator when the scope of Int is 0. I actually like the idea of defaulting the scope of Int to 0 and issue this warning if arithmetic operators are used, because the user then as to reason explicitly about which bitwidth makes sense for the model, instead of the current default that could yield unexpected results (for example in expressions involving cardinality).

I think the third point is a bug, and its not only related to integers. The textual representation is showing other stuff it should not, for example, information related to where the the loopback occurs in the trace or the size of the trace. Maybe we could move that point into a separate issue (maybe include it in issue #193).

[alcinocunha]

Now I noticed there was a related discussion in issue #30.

[grayswandyr]

Yeah, I'm a bit more extreme than you in #30 in that I would advocate systematically emitting a warning when arithmetic is used, unless an explicit bound on Int is set.

I think the third point is a bug, and its not only related to integers. The textual representation is showing other stuff it should not, for example, information related to where the the loopback occurs in the trace or the size of the trace. Maybe we could move that point into a separate issue (maybe include it in issue #193).

OK.

[jbrubru]

About the 4th point (with the example) now I understand that it indeed behaves correctly according to the wrap-around semantics of integers, but as already proposed in #30, a warning could be raised because the Int bound is not large enough to hold all the integer constants explicitly present in the model.

About the 3rd point, I agree with Alcino: let's put it in a separate issue because it is not only about integers. I created the new issue #207 because issue #193 is related to split panes, which I find quite different.

[nmacedo]

To add to the confusion, if you set the scope of Int to 0, it actually defaults to a Kodkod bitwidth that allows the representation of the size of universe, not a default constant value. I guess this was to guarantee that # over sets always work? But if you apply the # to non-unary relations, that no longer holds.

[tnelson]

Picking this up after re-reading the above comments. I propose the following changes:

(1) Alloy must issue a warning if an integer literal is used in the model that cannot be expressed in the current bitwidth. This is imperfect (we wouldn't catch, say, add[100, 100] under 3 Int) but it is better than nothing. E.g., this model would produce a warning when run:

sig Foo {}
run { #Foo = 10 } for 10 Foo, 1 Int

Moreover, a 0 Int bitwidth should prompt a warning for any use of cardinality or if the Int sig appears in a declaration.

(2) It seems vital that the evaluator reflects the model's semantics in its answers. This means it must reflect the chosen bitwidth for the current run, including evaluating cardinality to the empty set if there are no Int atoms. Comparison operators would continue to work as they do now, where the empty set is treated like 0. (E.g., add[1, none] evaluates to 1.)

Here I am a bit concerned about why Kodkod will "adjust" a 0 bitwidth as @nmacedo points out. I know there are situations where upper and lower bounds don't suffice to express numeric scopes, and so some cardinality constraints must be added. But last I checked, these were expressed using some disj quantification, rather than #. Is it possible this used to be done with # (which would explain the defensive restoration of bitwidth by Kodkod)?

I want to look into this more on the Kodkod/Pardinus side before attempting the change.

(3) I think we should more broadly discuss changing the default bitwidth, because it might impact many pre-existing models. I know some of mine, at least, assume the default. The proposed warning above will help catch many of these backward-compatibility issues, especially if we give a warning when cardinality is used at all, but it changes the issue from a silent failure to a noisy one.

Personally, I'd also favor a 0 Int default since it forces the user (who in my case are usually students!) to consider their bitwidth, as @alcinocunha noted.

(4) As I prototyped this some, I realized that there is some syntactic confusion in the evaluator, since {} is used to denote the empty set in the evaluator's output, but {} evaluates to true when used as input, since it parses as an empty conjunction. Rather than try to come up with something clever, could we just say none, or better yet, a product of none terms building to the correct arity, rather than {}?