I have some questions regarding how Alloy simplifies integer bounds.

Let's suppose I have the following Alloy model:

abstract sig A {
  f1: lone A,
  f2: lone Int
}
one sig A0,A1,A2,A3 extends A {}
fact {
  f1 in  A0->A0 + A1->A1 + A2->A2
}
run {}

Next I execute the "run command" setting the message verbosity to "debug only". The output says:

{...}
Simplifying the bounds...
Comment: Simplify this/A.f1 16->3
Solver=minisatprover(jni) Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20
{...}

The comment line tells us that an upper bound  of size 3 was inferred for relation f1. By inspecting the Kodkod output it is possible to known exactly which are these three tuples : A0->A0, A1->A1 and A2->A2.

Expecting a similar upper bound should be inferred for relation f2, I introduce the following fact to the model

fact {
  f2 in A0-> 0 + A1 -> 1 + A2 ->2
}

The expected upper bound should have only three tuples : A0->0, A1->1 and A2->2. To my surprise, when I execute  the run command again the result was :

{...}
Simplifying the bounds...
Comment: Simplify this/A.f1 16->3
Comment: Simplify this/A.f2 64->48
Solver=minisatprover(jni) Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20
{...}

Instead of inferring an upper bound of size 3, Alloy inferred an upper bound that contains 48 tuples. Looking into the Kodkod output I discover that these tuples were exactly : A0 -> Int, A1 -> Int, A2 -> Int. In other words, in the presence of integer atoms, the upper bound was over approximated.

My questions are:

* Is this a desired behavior of the Alloy Analyzer ? Why the component responsible of simplifying the bounds should ?

* Is it possible that the bound simplifier should be more accurate ?

* Could this be a feature request ticket ?

Best--
Juan