CODEWITHSUNDEEP
alloy
David Faitelson
David Faitelson

Reputation: 211

Why does the Alloy analyzer fail to find a counter example to the following assertion?

Checking the following assertion produces no counter examples:

assert G4_3__10
{ 
  all x : Int | (x = 1) 
}
check G4_3__10

Produces the following output:

Executing "Check G4_3__10"

Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
0 vars. 0 primary vars. 0 clauses. 4ms.
No counterexample found. Assertion may be valid. 0ms.

It does find a counter example when I add facts or signatures that use Ints (for example, adding 

fact { 0 in Int }

Can anyone explain the reason for this behavior?

Upvotes: 1

Views: 279

Answers (1)

Loïc Gammaitoni
Loïc Gammaitoni

Reputation: 4171

As you do not enforce the set of Integer to be non-empty in your original model, the analysis will only consider instances with no Integers. Your assertion will thus always hold hence no counter-example will be found.

The fact added in your second attempt pushes Alloy to consider instances where 0 is in the set of Integers. Alloy, will implicitly associate the default bitwith of 4 to Int, so that instances considered now contain integers in the interval [-8,7]. In those instances counter examples will befound.

You could also explicitly specify the Integer bitwidth to be used in your check command (rather than using this dummy fact) to enforce the presence of integers, e.g: check G4_3__10 for 4 Int

Upvotes: 3

Related Questions