I am a beginner in Alloy (The Modelling Language made by MIT). I am trying to model the leasing of a 2 bedroom apartment in Alloy. I am trying to add a fact such that the number of people in each leased apartment is not more than 4. However the instance generated on running, still shows only one 2 bedroom leased apartment having 10 occupants. What am I doing wrong? Also if possible could someone point to some good resources on learning Alloy apart from the tutorial on the MIT website? Thanks.
abstract sig apartment {}
sig twoLeased extends apartment {
occupants: some People
} { #occupants < 5 }
sig twoUnleased extends apartment {
}
sig People {}
run {} for 3 but 4 twoLeased, 10 People
By default the bit width used to represent integers is 4 so your instance contains integers ranging from -8 to 7. In an instance where the number of occupant is 10, an integer overflow thus occur (as 10>8), #occupants returning a negative number it is thus inferior to 5 hence satisfying your invariant.
To fix this issue, you can either forbid integer overflow in the Alloy Analyzer settings or increase the bit width used to represent integers (e.g. run {} for 6 Int).