NuSMV Realtime CTL

Question

Я использую NuSMV, и я пытаюсь написать свойство CTL в реальном времени.
Я хотел бы знать, если есть способ, чтобы установить шаги от государства, как:
((s.state = on) ABG (0..5 s.state = off))

читается как: if (s.state=on) is true, из этого состояния и для других 5 шагов свойства (s.state= off) is true.
Я попытался написать что-то вроде этого, но он не работает. Вы можете мне помочь?

В противном случае можно ли проверить одно и то же имущество, начиная с состояния, которое не является первым?

Answer 1

Вопрос. написать if (s.state=on) is true, из этого состояния и других 5 шагов свойства (s.state= off) is true.

ЦТЛ.

CTLSPEC AG ((s.state = on) -> 
      ((AX s.state = off) & 
      (AX AX s.state = off) & 
      (AX AX AX s.state = off) & 
      (AX AX AX AX s.state = off) & 
      (AX AX AX AX AX s.state = off) 
      )); 

С помощью этой формулы, вы проверить, является ли это правда, что каждый раз, когда вы попали s.state = on условия s.state = off будет справедливо, по крайней мере, 5 состояний после текущей, независимо от вашего выбора пути.

Начальный AG гарантирует, что это свойство должно храниться в любом месте пути выполнения, а не только в исходном состоянии.

Real CTL.

От nusmv список рассылки:

((s.state = on) ABG (1..5 s.state = off)) 

---

Примечание:остальная часть вашего вопроса не ясно мне, пожалуйста, если есть еще некоторые части без ответа просто редактировать ваш вопрос и немного уточните.