UPPAAL 또는 NuSMV를 사용한 엘리베이터 컨트롤

Question

저는 NuSMV 및 UPPAAL을 처음 사용하며이 문제를 해결하기 위해 노력하고 있습니다. 다음 질문 중 하나를 해결할 수 있습니까?

모델 (5 4 말 또는)과
liXs의 번호 (예를 들어 2 또는 3) 숫자와 바닥의 수를 제공하여
자신의 디자인의 엘리베이터 시스템의 제어 시스템을 분석 사용자가
개별 층에 있으며 서로 젤에 대한 개별적인 희망이 있습니다
층입니다. 수도 시스템 :
• 및/또는, 사용자가 LIX가 특정 층에 필요하다는 것을 나타낼 수
을 허용 위로 또는 아래로 갈 필요가 및/또는
특정 층으로 이동하도록 요청
• 또는 사용자는 실제 바닥에서 liX 요청을 할 수 있습니다.
• 이동하려면 문을 닫아야합니다. • 바닥을 건너 뛸 수 없습니다. • 모든 liX의 바닥면은 바닥 1입니다. a 엘리베이터는 엘리베이터를 설 치할 수있는 층에 주문할 수있는 하나의 부스로 제어되는
입니다.

Answer 1

나는 프로그램을 작성하지 않겠다.하지만 몇 가지 힌트를 줄 수있다.

포함 할 엔티티와 엔티티가 가질 수있는 상태를 결정하십시오. 예 : 단추, 오두막, 컨트롤러, 문 ...은 엔터티 일 수 있으며 엔터티는 상태를 가질 수 있습니다. 버튼을 누를 수 있고, 캐빈이 움직이거나 유휴 상태 일 수 있으며, 문을 열거 나 닫을 수 있습니다.

엔티티를 SMV가있는 모듈로 모델링합니다. SMV를 모른다면 간단한 예제를 통해 배우십시오.

만족해야하는 사양을 결정하십시오. 예를 들면 : 문이 열려있는 동안 엘리베이터가 바닥을 바꾸면 안됩니다.

다른 예제 SMV 프로그램으로 연습하면 쉽게 시작할 수 있습니다. 문제를 해결하기 위해 노력하는 코드를 게시하면 더 잘 도와 드릴 수 있습니다.