은 성명 LT1, 스핀

Question

내 영어에 대한 죄송합니다, 우크라이나에서 인스턴트 메신저)의 형태로만 표시 스핀 시스템 검증을 공부하기 시작했다. 우리는 다음 문제를 물었습니다 : "LTL 표현 아래에 존재합니다 : 나는 마샤를 사랑한다면, 나는 다샤를 사랑할 수 없습니다". 나는 그것을하는 방법을 이해할 수 없다.

int m = 4; 
int d = 5; 

proctype lab1(byte a; byte b){ 
    if 
    :: (a > b) -> printf("%e\n",a) 
    :: (a < b) -> printf("%e\n",b) 
    fi 
} 

init { 
    run lab1(m, d) 
} 

ltl la { []m } 

나는이 말도 이해하지만 - (내가 작성하는 방법을 모르는 있지만) 형태 [] P 코드로 표현된다, GP를 획득 마샤 처럼 P : 여기에 내가 가진 것입니다 나는 네 도움을 간청한다. 그냥 '내가 마샤를 사랑한다면, 내가 다샤 사랑하지 수'에 대한 LTL 식을해야하는 경우

Answer 1

다음이 충분 있습니다

bool i_love_masha; 
bool i_love_dasha; 

ltl la { i_love_masha -> !i_love_dasha } 

다음 문제는 모델의 동작입니다 것입니다. 나는 다음과 같이 추측 할 것이다.

init { 
    i_love_masha = true; 
    i_love_dasha = true; /* should be a violation! */ 
} 

어쩌면 그렇게 할 수 있을지 모른다. 그러나이 질문에 정확히 답하는 지 확실하지 않습니다.