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
#{SomeFormulaOrSet}
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.