NuSMV в реальном времени CTL

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

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

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


ctl nusmv
person Desmond    schedule 29.11.2016    source источник

Ответы (1)


arrow_upward
0
arrow_downward

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

CTL.

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 гарантирует, что это свойство должно сохраняться в любом месте на пути выполнения, а не только в начальном состоянии.

CTL в реальном времени.

Из списка рассылки nusmv:

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

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

person Patrick Trentin    schedule 01.12.2016
comment
Это формула CTL, я должен написать ее в CTL в реальном времени, где количество шагов указано как: int_number..int_number Если я напишу это: EBF 0..49 b.efficiency = 50 я проверяю, что от состояния 0 до состояния 49 эффективность равна 50. Но , я хотел бы знать, есть ли способ проверить свойство не из состояния (например, 0,1,2...), а из состояния, в котором условие истинно, например: EBF (s.state = on)..49 b.efficiency = 50 , которое читается как: из состояние где (s.state = on) и для следующих 49 шагов b.efficiency = 50 надеюсь теперь понятно - person Desmond; 02.12.2016
comment
@Desmond, вы можете отредактировать свой вопрос и добавить модель, о которой вы говорите? - person Patrick Trentin; 02.12.2016