NuSMV에서 모델 검사를위한 유효한 CTL 또는 LTL 식을 만들려고합니다.유효한 CTL 또는 LTL 식 구성 (NuSMV)
나는 게임에서 서로를 잡으려고하는 배우가있는 변수가 있습니다. 변수는 State_Of_Game : {Win, Lose, Playing}
이며, 모든 시작 상태에서 게임이 승리하거나 손실 될 수 있음을 표현하고 싶습니다.
그래서 어떻게 이것을 CTL 또는 LTL로 구현할 수 있습니까?
나는 AG (S_O_G = Win | S_O_G = Lose)와 같은 것을 생각하고 있었지만 모든 시작 상태에서 볼 수있는 것을 구현하는 방법을 모른다.
나는 SMV 표기법에 익숙하지 않은, 그래서 나는 이것에 대해 추측하고 있지만, 핵심 포인트는
외부에서 모든 상태 이상 정량화 방지하려면 : 당신이 원하지 않는 모든 게임이 원이나 분실 될 수 있지만 시작 게임 만 할 수 있다고 말하십시오. 그래서 그냥 함께하지 분리를 사용하려면 어떤 바깥 쪽 양상
로 시작하는 상태에서 수식을 가지고 : 당신이
당신은 각 분기를 포장 별도의 양식을 필요로 모두 winnability 및 losability을 주장 할 : winnability를 , losability는 실존 적 주장이며 조건을 성취하는 것이 가능하다고 말한다.
내가 생각하는 당신이 필요로하는 공식은 /는 init 같은 뭔가 의미 명명 된 루트에 절 또는 주장을 시작할 수있는 루트 (EG SOG = 승리) & (EG SOG = 패) 절. SMV에 EG 양식이없는 경우 EG p =! (AG! p)를 사용하여 AG로 변환 할 수 있습니다. 이는 두 가지가 De Morgan 이중 쌍이기 때문입니다.