합금의 수학 연산

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 명의 의사가 있다는 명령을 실행 명령에 적용했습니다.

사용할 수있는 정수의 범위로, 합금의 숫자와 함께 연주 할 때 항상 조심해야 자신의 범위를 통해 그들에게 할당 된 비트 폭에 따라 달라집니다.

기본적으로 정수의 범위는 4, 그래서 정수는 다시 귀하의 질문에가는 -8 7.

범위 :

왜 병원에 관련된 5 명 이상의 의사가있다 ?

진료소에 지정된 의사가 8 명 있다고 가정 할 때 제공 한 사실이 어떻게 될 수 있습니까? 합금은 [-8,7]의 범위에서 8을 나타낼 수 없기 때문에 오버플로가 발생하여 병원에 배정 된 의사의 수는 -8입니다. -8이 실제로 5보다 작다는 사실은 귀하의 모델에서 허용하는 이유입니다. 8 명의 의사가 하나의 진료소에 연결됩니다.

어떻게 그 문제를 해결하기 :

두 가지 옵션을 다른 사람의 사이에서 :

• 는 정수의 범위를 증가
• 의사
의 수를 감소. 100 명의 의사를 "프레임"하기 위해서는 적어도 8 비트 폭의 정수를 충분히 표현해야합니다. 8 정수를 실행하면 정수 범위는 다음과 같습니다. [-128,127]

Answer 2

범위에주의하십시오. 왜 100 명의 의사가 필요합니까?

의사 100 명과 병원 1 명과 관계 의사는 2^100 = 10^30 값을 갖습니다. Alloy Analyzer는 모델 검사기와 같으므로 상태 공간을 관찰해야합니다. 그런 종류의 상태 공간에 만족할 모델 검사기는 없습니다.