Why can't a count of the values in an empty field be compared against an integer?

Question

I created a test to compare a count of the number of values in an empty field against a number. I am surprised at the results.

First, I created a signature with field f that optionally maps an A atom to another A atom:

sig A {f: lone A}

Then I created this expression: If f is empty, then a count of the number of A atoms mapped by f is less than 8:

check {
    no A.f =>
        # A.f < 8 
}

I ran the check command and the Alloy Analyzer found a counterexample. This surprised me greatly.

I opened the Evaluator tool and entered this:

I typed: A

The Evaluator responded: {}

I typed: no A.f

The Evaluator responded: true

I typed: # A.f

The Evaluator responded: 0

I typed: # A.f < 8

The Evaluator responded: false

Huh?

Why is 0 < 8 false?

Answer 1

Alloy has only a limited set of integers since each integer is relatively expensive in finding a solution. By default this set is:

Int
  ┌──┬──┬──┬──┬──┬──┬──┬──┬─┬─┬─┬─┬─┬─┬─┬─┐⁻¹
  │-8│-7│-6│-5│-4│-3│-2│-1│0│1│2│3│4│5│6│7│  
  └──┴──┴──┴──┴──┴──┴──┴──┴─┴─┴─┴─┴─┴─┴─┴─┘  

When you do 7+1 you actually get -8!

Try it ... Just type 8 in the evaluator:

 8
   -8

This is actually not limited to Alloy, C, C++, Java and most other languages do the same, the reason you're not generally noticing it is because the wrap around point is so much higher. For a Java int it is more than 2 billion. The reason is is that the ints are stored as a set of bits. Once you reach the maximum value, an addition will require an extra bit. Since that bit does not exist it is silently ignored. (Actually quite an horrendous idea to realize that so far I've never seen any code that handles this overflow.)

Therefore, when your maximum number is 7, the default in Alloy, and you use 8 it actually is -8!

  # A.f < -8 

The reason we have this horror is that in Alloy Int is also packed in a bit set when it is given to the SAT solver.

Alloy has been struggling a bit with this and there is an option to prevent overflows. Initially I thought this was gift send from heaven but since I realized how it worked I disabled it. The problem is that it removes solutions that might be valid. This is not too bad finding a solution since you will notice when there is nothing there but it is quite bad for assertions since an assertion might say there is no solution while the model actually has. This gives me the shivers because I want to rely on an assertion. Looking at actual use cases I decided that I'd rather explicitly handle overflows in my model since they are actually a problem in the final product as well. Many known bugs are caused by unexpected overflows. So a model that hides them is imho not very useful.

So how do you handle this? The syntax for this is a tad odd. You have to specify the bitwidth of the integer encoding. So you could change your model to:

sig A {f: lone A}

check {
    no A.f =>
        # A.f < 8 
} for 5 int

The for 5 int sets the bit width of the SAT encoding to 5 bits. 5 bits = 5^2=32. So then you have the integers -16..15.

This clearly is a huge tripwire. Fortunately there is fantastic work going on to make Alloy run on a SMT solver. SMT solvers will have a much more natural number handling that Alloy and this would not trip you up.

That said, I can try to at least generate an error if you use a constant integer that does not fit in the available Int set. Maybe you could file a bug?