Стр. 12 - А.М. Андреев, И.А. Козлов - Подход к верификации моделей систем реального времени с помощью метода Model Checking

Рис. 8. Схема связей автоматов А1 и А2
Проверим для этого автомата утверждение: “При попадании в со-
стояние s12 показания часов c3 должны превышать 60”. Такое условие
должно гарантировать заданный промежуток времени между движе-
нием поездов.
Система верификации выдает следующий результат проверки:
[AG(/(s12)|(c3>=10))]
Subformulas:
#sub1= s12
#sub2= / #sub1
#sub3= c3>=10
#sub4= #sub2 | #sub3
#sub5= / #sub4
#sub6= E(#sub0 U #sub5)
#sub7= / #sub6
#sub1 #sub2 #sub3 #sub4 #sub5 #sub6 #sub7
State 58: 0 1 0 1 0 1 0
Result of verification is negative for the initial state of the graph
(state 58)
58 ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012