CODEWITHSUNDEEP
alloyformal-verification
Kevin
Kevin

Reputation: 685

Count using # not working in Fact (Alloy)

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

Upvotes: 1

Views: 284

Answers (1)

Lo&#239;c Gammaitoni
Lo&#239;c Gammaitoni

Reputation: 4171

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).

Upvotes: 3

Related Questions