저는 합금으로 된 매우 간단한 모델을 가지고 있습니다. 단지 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
내 모델에 문제가 있습니까?
모델을 분석하는 데 사용하는 범위가 있다면 모델에 특히 문제가 없습니다.
실제로 귀하는 진료소와 관련된 의사의 수를 확인합니다. 자, 정확히 100 명의 의사가 있다는 명령을 실행 명령에 적용했습니다.
사용할 수있는 정수의 범위로, 합금의 숫자와 함께 연주 할 때 항상 조심해야 자신의 범위를 통해 그들에게 할당 된 비트 폭에 따라 달라집니다.
기본적으로 정수의 범위는 4, 그래서 정수는 다시 귀하의 질문에가는 -8 7.
범위 :
왜 병원에 관련된 5 명 이상의 의사가있다 ?
진료소에 지정된 의사가 8 명 있다고 가정 할 때 제공 한 사실이 어떻게 될 수 있습니까? 합금은 [-8,7]의 범위에서 8을 나타낼 수 없기 때문에 오버플로가 발생하여 병원에 배정 된 의사의 수는 -8입니다. -8이 실제로 5보다 작다는 사실은 귀하의 모델에서 허용하는 이유입니다. 8 명의 의사가 하나의 진료소에 연결됩니다.
어떻게 그 문제를 해결하기 :
두 가지 옵션을 다른 사람의 사이에서 :
범위에주의하십시오. 왜 100 명의 의사가 필요합니까?
의사 100 명과 병원 1 명과 관계 의사는 2^100 = 10^30 값을 갖습니다. Alloy Analyzer는 모델 검사기와 같으므로 상태 공간을 관찰해야합니다. 그런 종류의 상태 공간에 만족할 모델 검사기는 없습니다.
나는 그저 많이 확인하고 싶지 않아. 하지만 나는 합금 분석기가 모든 관계를 점검하지 않는다고 생각합니다. 그것은 내가 생각하기에 몇 번 발견되면 멈 춥니 다. 하지만 조언을 주셔서 감사 드리며 앞으로 이것을 고려해 보겠습니다. – eakyurek
"합금에서 숫자로 재생할 때는 항상주의해야합니다". 뛰어난 원칙, 훌륭한 표현. –