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

1 Answer 1

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?

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.