CODEWITHSUNDEEP
alloy
eakyurek
eakyurek

Reputation: 124

Mathematical Operations in Alloy

I have a very simple model in alloy. It should only attach maximum of 5 doctors to a clinic but when i execute the model it attaches more than 5 doctors to a clinic. Here is my model.

abstract sig Clinic {
    doctors : set Doctor
}
abstract sig Doctor {
}
fact ClinicDoctorRestriction {
    all c:Clinic | #c.doctors <= 5
}
pred showresult{
}
run showresult for exactly 1 Clinic, exactly 100 Doctor

Is there something wrong with my model?

Upvotes: 0

Views: 551

Answers (2)

Daniel Jackson
Daniel Jackson

Reputation: 2768

Be careful about your scope. Why do you need 100 doctors?

Note that with 100 doctors and 1 clinic, the relation doctors has 2^100 = 10^30 values. Remember that the Alloy Analyzer is like a model checker, so you have to watch the state space. No model checker would be happy with that kind of state space.

Upvotes: 1

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

Reputation: 4171

There is nothing especially wrong in your model if it is the scope you use to analyse it.

Note that in your fact, you check the number of doctor associated to the clinic. Now, you enforced in your run command that there is exactly 100 Doctors.

You should always be careful when playing with numbers in Alloy, as the range of integers you can use depends on the bit-width assigned to them through their scope.

By default, the scope of integer is 4, and so integers range from -8 to 7.

Going back to your question:

Why is there more than 5 doctors associated to a clinic?

Suppose there is 8 doctors assigned to the clinic, how can the fact you provided let that happen? Alloy can't represent 8 in the range given [-8,7] so an "overflow" occurs, leading to the surprising result that the number of doctor assigned to the clinic is -8. The fact that -8 is indeed smaller than 5 is the reason why your model allows e.g. 8 doctors to be associated to a single clinic.

How to fix that :

Two options among others :

  • decrease the number of doctor
  • increase the range of Integers. You would need in order to represent enough integers a bit-width of at least 8 in order to "frame" those 100 doctors. run .. for 8 Int will give you the following range of integer : [-128,127]

Upvotes: 5

Related Questions