inconsistent behavior of equivalence when prevent overflows is set to 'yes'

Question

The following example shows two checks that appear equivalent, yet the second finds a counterexample while the first does not. When setting 'prevent overflow' to 'No', both return the same result:

sig A {
  x : Int,
  y : Int
 }

 pred f1[a:A] {
   y = x ++ (a -> ((a.x).add[1]))
 }

 pred f2[a:A] {
   a.y = (a.x).add[1]
   y = x ++ (a -> a.y)
 }

check {
  all a : A | {
    f1[a] => f2[a]
    f2[a] => f1[a]
 }
}

check {
  all a:A | {
    f1[a] <=> f2[a]
 }
} 

I am using Alloy 4.2_2015-02_22 on Ubuntu Linux with sat4j.

Answer 1

I am sorry not to be able to offer a more useful answer than the following. With luck, someone else will do better.

It is possible, I think, that your model exhibits a bug in Alloy. But perhaps instead the model exhibits a counter-intuitive consequence of the semantics of integers in Alloy when the Prevent Overflow flag is set. Those semantics are described in the paper Preventing arithmetic overflows in Alloy by Aleksandar Milicevic and Daniel Jackson. You may have an easier time following the details than I am having.

The following expressions seem to suggest (a) that the unintuitive results have to do with the fact that the law of excluded middle does not hold when negation is applied to undefined values, and (b) that in the case where a.x = 7 (or whatever the maximum value of Int is, in a particular scope), the predicates f1 and f2 behave differently:

pred xm1a[ a : A] { (f1[a] or not(f1[a])) }
pred xm2a[ a : A] { (f2[a] or not(f2[a])) }
pred xm1b[ a : A] { (not (f1[a] and not(f1[a]))) }
pred xm2b[ a : A] { (not (f2[a] and not(f2[a]))) }

// some sensible assertions:  no counterexamples
check x1 { all a : A | a.x = 7 implies xm1a[a] }
check x2 { all a : A | a.x = 7 implies xm2a[a] }
check x3 { all a : A | a.x = 7 implies xm1b[a] }
check x4 { all a : A | a.x = 7 implies xm2b[a] }

// some odd assertions: counterexamples for y2 and y4
check y1 { all a : A | a.x = 7 implies not xm1a[a] }
check y2 { all a : A | a.x = 7 implies not xm2a[a] } 
check y3 { all a : A | a.x = 7 implies not xm1b[a] }
check y4 { all a : A | a.x = 7 implies not xm2b[a] } 

It's not clear (to me) whether the relevant difference between f1 and f2 is that f2 refers explicitly to a.y, or that f2 has two clauses with an implicit and between them.

If the arithmetic relation between a.x and a.y is important to the model, then figuring out exactly how overflow cases are handled will be essential. If all the matters is that a.x != a.y and y = x ++ (a -> a.y), then weakening the condition will have the nice side effect that the reader need not understand Alloy's overflow semantics. (I expect you realize that already; I mention it for the benefit of later readers.)