ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012 183
снижая общности, ограничимся двумя модальностями, т. е. сократим
процесс
P
1
до процесса
1
:
P
′
1
0.(? 1. 11.(? 1.! 12. . 13.0 ? 1. 14.! . 15.0) ? 1. 16.! . 17.0)
0.(? 2. 21.(? 1. 22.(? 2. 23.! . 24.0 ? 2. 25.! . 26.0) ? 1. 27.! . 28.0) ? 2. 28.! . 29.0).
'
t
m t
z t в t
z t
п t
m t
п t
t
m t
z t
z t
в t
z t
п t
z t
п t
m t
п t
P
Программа, написанная на языке «Пролог», по принципу «найти
и проверить» для процесса
1
P
′
содержит множество фактов, задающих
переходы процесса. Чтобы представить в языке «Пролог» множество
переходов процесса
1
,
P
′
которые перечислены ниже, используем пре-
дикат
transition
(
state
,
action
,
state
).
Здесь
state
—
состояние процесса;
action
—
действие. Состояния обозначим теми же именами, что и
в процессных выражениях, а действия переименуем (?
m
1
в
m
1;
? 1
m
в
notm
1; ?
m
2
в
m
2;
? 2
m
в
notm
2;
!
п
в
cont
; ?
z
1
в
z
1;
? 1
z
в
notz
1; ?
z
2
в
z
2;
? 2
z
в
notz
2;
!
в
в
turnoff
):
0.? 1. 11.
0.? 1. 16.
16.! . 17.
11.? 1. 12.
12.! . 13.
11.? 1. 14.
14.! . 15.
0.? 2. 21.
21.? 1. 22. 22.? 2. 23. 22.? 2. 25. 25.! . 26.
0.? 2. 28. 28.! . 29.
23.! . 24.
21.? 1. 27.
27.! . 28.
t
m t
t
m t
t
п t
t
z t
t
в t
t
z t
t
п t
t
m t
t
z t
t
z t
t
z t
t
п t
t
m t
t
п t
t
в t
t
z t
t
п t
Кроме перечисленных фактов, задающих переходы, введем дву-
местный предикат
accessible
(
S
1, [
X
],
S
2).
С помощью этого предика-
та добавим следующие правила, обусловливающие условия дости-
жимости состояния
S
2
из состояния
S
1
после передачи процессу,
находящемуся в состоянии
S
1
последовательности входных симво-
лов, представленных списком
[
X
]:
нерекурсивное правило достижимости:
accessible
(
B
1,
X
,
В
2)):-
transition
(
S
1,
X
,
В
2);
рекурсивное правило достижимости:
(
accessible
(
S
1, [
Х
|
Rest
],
В
2):-
transition
(
S
1,
X
,
S
3),
accessible
(
S
3,[
Rest
],
S
2)).
Если разработчика ИМИ интересует только проверка свойства

1
(? 1.? 1.)
f m z
⊃
◊
1
(
)
turnoff
ϕ
,
то на языке «Пролог» для этого фор-
мулируется цель:
accessible
(
t
0,
X
,
t
13),
nl
.
Указанное свойство будет
удовлетворено, если из состояния
t
0
в состояние
t
13
ведет един-
ственная нить 1. 1.
m z turnoff
.
Программа, написанная на языке «Про-
лог» с использованием введенных фактов и правил, приведена ниже:
domains
state=symbol
action= symbol
list=action*
predicates
nondeterm transition(state, action, state)
nondeterm accessible(symbol, list, symbol)
nondeterm member(action,list)