시스템 모델을 모델 검사를위한 전환 시스템으로 변환

Question

현재 시스템 프로토 타입을 전환 시스템 모델로 변환하려고합니다. 일부 LTL 속성이 있고 모델 검사 도구 NuSMV를 사용하여 이러한 속성을 확인하려고합니다. 필자는 단지 원자 속성 및 기타 수학적 측면을 정의하여 모델링을 시작하는 방법에 대한 정보만을 제공합니다. NuSMV 그 전환 시스템의에

Pictorial Representation of Model

Answer 1

아주 간단한 인코딩하지만, 난 당신이 제공모델에 맞게 너무 단순 조금이라고 생각

MODULE main() 
VAR 
    state : { GETINFO, ACK, SEND }; 
ASSIGN 
    init(state) := GETINFO; 
    next(state) := case 
    state = GETINFO : SEND; 
    state = SEND : ACK; 
    state = ACK  : {GETINFO, SEND}; 
    esac; 

것이다 당신의 문제 설명입니다. 따라서 귀하가하려는 의도에 대한 추가 정보를 제공 할 것을 권합니다.