SPIN을 사용하여 전환 시스템을 모델링하는 방법

Question

새로 입문했습니다. 전이 시스템이 주어진 LTL 특성을 만족시키는 지 확인하고 싶습니다. 그러나 나는 promela에서 전이 시스템을 모델링하는 방법을 모른다. 예를 들어 아래에 표시된 전환 시스템에는 두 가지 상태가 있으며 초기 상태는 s0입니다. LTL 속성이 <> q인지 확인하는 방법. 아무도 promela 에서이 문제를 설명하는 방법을 알고 있습니까? 그건 그렇고, 스핀에 LTL의 다음 연산자를 사용하는 방법?

bool p, q; 

init 
{ 
    s1: 
    atomic { 
     p = true; 
     q = false; 
    } 
    goto s2; 

    s2: 
    atomic { 
     p = false; 
     q = true; 
    } 
} 

, 당신의 LTL 속성을 확인하여 파일 및 실행 스핀의 끝과 함께 생성 된 실행에 ltl eventually_q { <>q };을 배치하려면 :

Answer 1

당신은 라벨, 원자 블록 gotos를 사용하여 오토마타를 모델링 할 수 있습니다 -a.

끝 부분에 붙지 않는 속성 (예 : ltl always_p { []p };)을 배치하면 속성이 위반되었음을 나타내는 end state in claim reached 메시지가 표시됩니다.

다음 연산자 정보 : Spin이 기본값별로 사용하는 부분 순서 감소 알고리즘과 충돌합니다. next-operator를 사용하는 속성은 스터 터 불변 값이어야합니다. 그렇지 않으면 부분 순서 감소가 비활성화되어야합니다. this man page 끝 부분에서 자세히 읽어보십시오.