6 / 10
состояния, обозначаются прописными символами
B
и индексируются,
если это необходимо, например, как
Bi
. Условия перехода
c
1
?
a
1
.c
2
!
a
2
или
c
2
!
a
2
.c
1
?
a
1
представляются функторами. Пока соответствующие
функторы будем обозначать как
f
(
x
)
, где
x
— это
c
1
?
a
1
.c
2
!
a
2
или
c
2
!
a
2
.c
1
?
a
1
. Используя введенные обозначения для того, чтобы вве-
сти структуру используемых логических программ на языке VISUAL
PROLOG, введем следующие предикаты и правила:
•
initial
(
Bi
) — одноместный предикат, истинный, когда автомат
находится в начальном состоянии
Bi
;
•
final
(
Bj
) — одноместный предикат, истинный, когда автомат на-
ходится в конечном состоянии
Bj
;
•
transition
(
Bi, f
(
x
)
, Bj
) — трехместные предикаты, называемые
переходами и истинные, если на процессном графе переходов
имеются переходы из состояния
Bi
в состояние
Bj
, условиями
перехода которых, являются соответственно
x
;
•
accessible
(
Bi
, [
X
]
, Bj
)) — двуместный предикат, истинный, если
состояние
Bj
достижимо из состояния
Bi
в результате последо-
вательного выполнения условий перехода из списка [
X
] (наличия
на процессном графе переходов пути, ведущем из состояния
Bi
в состояние
Bj
, дуги которого помечены условиями перехода из
списка [
X
]);
•
accessible
(
Bi
,
X, Bj
): —
transition
(
Bi
,
X, Bj
) – нерекурсивное
правило достижимости состояния
Bj
из состояния
Bi
;
•
accessible
(
Bi
, [
Х
|
Rest
]
, Bj
): —
transition
(
Bi
,
X, Bk
),
accessible
(
Bk
,
[
Rest
],
Bj
) — pекурсивное правило достижимости состояния
Bj
из состояния
Bi
.
Логическая схема программы (псевдокод) на языке VISUAL
PROLOG 5.0 для проверки правильного окончания для пары графов
UAC и UAS будет содержать следующие разделы:
•
domains
, описывающий структуру функторов
f
=
f
(
x
)
, пред-
ставляющих переходы
x
и структуру списка из этих перeходов
list
=
f
∗
;
•
predicates
, описывающий предикаты перехода
transition
(
symbol,
list, symbol
) между состояниями графов и предикаты достижимо-
сти
accessible
(
symbol, list, symbol
) одних состояний из других;
•
clauses,
содержащий описание всех переходов (фактов) и правил
достижимости;
•
goal,
который ставит задачу проверки условий правильного по-
ведения агентов.
Логическая программа проверки правильности SIP-специфи-
каций (на примере проверки условия правильного окончания).
Рассмотрим в качестве примера простые графы, показанные на рис. 3
и 4. Для выполнения условия правильного окончания для каждого
112 ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2015. № 2