#가 작동하지 않음 (사실) (합금)

Question

저는 Alloy (MIT에서 만든 모델링 언어)의 초보자입니다. 나는 합금에 2 베드룸 아파트 임대를 모델로하고있다. 각 임대 아파트의 인원수가 4 명을 초과하지 않도록 사실을 추가하려고합니다. 그러나 달리기 인스턴스는 10 명의 거주자가있는 단 하나의 2 베드룸 임대 아파트 만 보여줍니다. 내가 도대체 ​​뭘 잘못하고있는 겁니까? 또한 가능하다면 누군가 MIT 웹 사이트의 튜토리얼과 별도로 합금 학습에 관한 좋은 자료를 가리킬 수 있습니까? 감사.

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 

Answer 1

는 기본적으로 정수를 표현하기 위해 사용되는 비트 폭은 4 그래서 인스턴스가 -8에서 7에 이르기까지 정수를 포함합니다. 점유자 수가 10 인 경우 정수 오버플로가 발생하므로 (10>8) #occupants은 음수를 반환하므로 5보다 열등하므로 불변성이 충족됩니다.

이 문제를 해결하려면 Alloy Analyzer 설정에서 정수 오버플로를 금지하거나 정수를 나타내는 데 사용되는 비트 폭을 늘리십시오 (예 : run {} for 6 Int).