合金中的数学运算

Question

我有一个非常简单的合金模型.它应该只将最多5名医生附加到诊所,但是当我执行该模型时,它会将超过5名医生附加到诊所.这是我的模特.

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

我的模型有问题吗？

Answer 1

如果模型是用于分析它的范围,则模型中没有什么特别错误.

请注意,在您的事实中,您检查与诊所相关的医生数量.现在,您在运行命令中强制执行了恰好有100名医生.

在Alloy中使用数字时应始终小心,因为可以使用的整数范围取决于通过其范围分配给它们的位宽.

默认情况下,整数范围为4,因此整数范围为-8到7.

回到你的问题:

为什么诊所有超过5名医生？

假设有8名医生被分配到诊所,你提供的事实怎么可能发生呢？合金在给定[-8,7]的范围内不能代表8,因此发生"溢出",导致分配给诊所的医生数量为-8的令人惊讶的结果.事实上-8确实小于5是你的模型允许例如8名医生与一个诊所相关联的原因.

如何解决这个问题:

其中两个选项:

• 减少医生的数量
• 增加整数的范围.你需要为了表示足够的整数至少为8的位宽,以"框架"那100名医生.run .. for 8 Int将为您提供以下整数范围:[ - 128,127]