Рис. 7. Модель автомата-преобразователя:
z
0
— брать ремень;
z
1
— ругать сына;
z
2
— успокаивать сына;
z
3
— надеяться;
z
4
—
радоваться;
z
5
— ликовать
ликовать”. Это утверждение можно выразить в виде CTL-формулы:
AG(
z0
→
EF(z5))
. После анализа структуры автомата становится ясно,
что эта формула для него выполняется. Приведем результат проверки,
осуществляемой разработанной системой.
[AG(/(z0)
|
EF(z5))]
Subformulas:
#sub1= z0
#sub2= / #sub1
#sub3= z5
#sub4= E(#sub0 U #sub3)
#sub5= #sub2
|
#sub4
#sub6= / #sub5
#sub7= E(#sub0 U #sub6)
#sub8= / #sub7
#sub1 #sub2 #sub3 #sub4 #sub5 #sub6 #sub7 #sub8
State 34: 0 1
0
1
1
0
0 1
Result of verification is positive for the initial state of the graph
(state 34)
Результат проверки с помощью системы верификации совпадает с
полученным теоретически.
Система логического управления
. Верификация системы логиче-
ского управления будет демонстрироваться на примере системы упра-
вления шлагбаумом на железнодорожном переезде (рис. 8–10).
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
57
1...,2,3,4,5,6,7,8,9,10 12,13,14