2

I am using # operator to get the cardinality of Cartesian product (A->B) and Union (A+B). But it returns weird negative numbers and I have no idea what they are!?

Please see the snapshot bellow showing A->B and A+B content for my model and the cardinalities Alloy give me using # operator. ( I expect to get 12 for the first and 8 for the second, but I get -4 for the first and -8 for the second)

Any comment?!

enter image description here

bellow is my specification if it helps:

open util/relation

sig A {}

sig B{}

sig C{r1: one A,r2:one B}

run {} for 6

Community
  • 1
  • 1
qartal
  • 2,024
  • 19
  • 31

1 Answers1

6

By default, Alloy integers are 4-bit twos-complement values, so the range of possible values runs from -8 to 7. For reasons bound up with complicated tradeoffs in design and implementation, the Analyzer handles the limited range of integers by wrap-around. In your example, the cardinality of A->B is 12, which overflows the available range; the values wrap around and the evaluator displays the value -4.

To allow for cardinalities as high as 12, the simplest workaround is to ensure that Int has a bitwidth greater than 4, using the keyword int in the scope specification.

Concretely: change run {} for 6 to run {} for 6 but 5 int. (You can of course use a bitwidth greater than 5.)

Newer versions of Alloy also have a Forbid Overflow option, which prevents spurious examples and counter-examples from being presented when predicates are run or assertions checked.

See also the recent question Why does Alloy tell me that 3 >= 10?

Community
  • 1
  • 1
C. M. Sperberg-McQueen
  • 24,596
  • 5
  • 38
  • 65