시스템이 모든 상태를 통과하는지 확인하십시오.

Question

변수 state은 시스템 상태를 나타냅니다 (예 : state \in {"ready", "prepare", "do", "cleanup", "done"}). state이 궁극적으로 모든 5 개 주를 (어떤 순서로) 통과시켜야한다는 조건을 표현하는 방법?

---

작동 예 (허용 대답) : States = {"ready", "prepare", "do", "cleanup", "done"}를

EXTENDS Naturals 
VARIABLE n 
Init == n = 1 
Next == IF n < 3 THEN n' = n + 1 ELSE n' = n 
Spec == Init /\ [][Next]_<<n>> /\ WF_<<n>>(Next) 
Check == \A s \in {1,2,3}: <>(s = n) \* This goes: Model Overview > 
             \* > "What to check?" > Properties 

Answer 1

을 감안할 때, 당신은

<>(state = "ready") 

일부 주어진 상태에 도달 확인할 수 있습니다 그리고 당신은 모든 상태에 도달 확인할 수 있습니다 와 함께

\A s \in States: <>(state = s)