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.