TIL Cardinality in Alloy* will happily return negative numbers

Figuring out how cardinality works in Alloy* was fun.

First off I had to ask the TA how to even get a count of a set in Alloy* which looks like this
Within it you can’t use the quantifiers such as all, some, lone, etc.

Then I had to understand how bounds work. For instance
run SomePredicate for 2 Int
bounds the system by the bitwidth of 2 which is -2, -1, 0, and 1.

Come to find out, the cardinality of something in Alloy* is limited to that same bounded list of integers and it will happily overflow!

Thus 0 = 0 and 1 = 1, but 2 = -2 and 3 = -1, etc. The first time i saw this was getting -2 when I expected 2. That really threw me for a loop.

In hindsight this makes sense, but I still can’t find this explained in the Alloy documentation. It’s probably in one of the tutorials. Thankfully stackoverflow came through when I searched for alloy* negative cardinality.

I may start doing more of these short Today I Learned posts. Idea credit to Josh Branchaud who posted his repository of TILs to Hacker News and borrowed the idea from thoughtbot. And of course this is all just a boring-software version of reddit’s TIL.