Дубинин В.Н., Зинкин С.А. Языки логического программирования в проектировании вычислительных систем и сетей
Подождите немного. Документ загружается.
3.2.3. Реализация других временных операторов
Рекурсивные уравнения для операторов INEV и SOME имеют следующий
вид:
T,s ╞ INEV(p1,p2), если T,s ╞ p2 ∨ (p1 & PRETILDA INEV(p1,p2)).
T,s ╞ SOME(p1,p2), если T,s ╞ p2 & (∼p1 ∨ PRE SOME(p1,p2)).
Ниже приводится прологовская реализация данных операторов, включая
ограничительные условия:
inev(P1,P2,L,S):-inl(S,L),!,fail.
inev(P1,P2,L,S):-P2=..K,insert(K,[S],P00),P02=..P00,call(P02),
!.
inev(P1,P2,L,S):-arc(S,T,S1),
!,
P1=..K,insert(K,[S],P0),P01=..P0,call(P01),
pretilda(inev(P1,P2),[S|L],S).
some(P1,P2,L,S):-inl(S,L),
!.
some(P1,P2,L,S):-P2=..K,insert(K,[S],P0),P02=..P0,call(P02),
non(arc(S,T,S1)),
!.
some(P1,P2,L,S):-P2=..K,insert(K,[S],P00),P02=..P00,call(P02),
P1=..T,insert(T,[S],P0),P01=..P0,
non(P01),
!.
some(P1,P2,L,S):-P2=..K,insert(K,[S],P0),P02=..P0,call(P02),
pre(some(P1,P2),[S|L],S).
Некоторые упрощения
Ниже приводятся некоторые упрощения представления операторов
временной логики. Во-первых, список l используется только в ходе
выполнения программы. Таким образом, временной оператор может
вызываться без использования этого параметра. В случае POT-оператора, это
упрощение определяется следующим клозом:
pot(P1,P2,S):-pot(P1,P2,[],S).
Заметим, что начальное значение списка l есть [], что является признаком
пустого списка.
Дальнейшие упрощения достигаются путем устранения условного
предиката р1. В этом случае мы предполагаем, что предикат р1 имеет
значение "истина" в некотором состоянии. Декларация этого факта дается
следующим прологовским клозом:
true(S).
Безусловный POT-оператор имеет только два аргумента. Сокращение
аргументов POT-оператора может быть задано следующим клозом:
pot(P,S):-pot(true,P,[],S).
Подобные упрощения могут применяться ко всем другим временным
операторам.
3.2.4. Реализация невременных логических операторов
При интерпретации ЛДВ-формул на языке Пролог необходимо оценивать
не только временные, но и невременные логические операторы.
Для этого выражения должны быть записаны в клаузальной форме и
переведены в прологовские клозы.
Ниже приводятся прологовские клозы для оценки следующих
невременных логических операторов: отрицания (NOT), дизъюнкции (OR),
конъюнкции (AND), импликации (IMPLIES), эквивалентности (EQU):
not(P,S):-P=..T,insert(T,[S],P0),P01=..P0,call(P01),
!,
fail.
not(P,S).
or(P1,P2,S):-P1=..T,insert(T,[S],P0),P01=..P0,call(P01),!.
or(P1,P2,S):-P2=..T,insert(T,[S],P0),P02=..P0,call(P02).
and(P1,P2,S):-P1=..T,insert(T,[S],P0),P01=..P0,call(P01),
P2=..K,insert(K,[S],P00),P02=..P00,call(P02).
implies(P1,P2,S):-P1=..T,insert(T,[S],P0),P01=..P0,call(P01),
not(P2,S),!,fail.
implies(P1,P2,S).
equ(P1,P2,S):-P1=..T,insert(T,[S],P0),P01=..P0,call(P01),
P2=..K,insert(K,[S],P00),P02=..P00,call(P02),
!.
equ(P1,P2,S):-not(P1,S),
not(P2,S).
3.3. Исследование сетевых моделей
Ниже приводятся результаты исследований сетевых моделей,
рассмотренных в главе 2, с помощью временной логики. Временная логика
выступает в роли языка описания доказываемых свойств системы. Следует
отметить, что ниже будут использоваться только безусловные временные
операторы. При записи формулы для всех предикатов будет опускаться
аргумент, определяющий состояние системы.
3.3.1. Доказательство свойств сетевых моделей
Свойства сетевых моделей были определены в разд. 1.2. Для
доказательства свойств определим предикат enable. Истинное значение
выражения enable(t,s) показывает, что в состоянии s разрешен переход t.
Этот предикат истинен в состоянии s, если существует дуга из состояния s в
состояние s1. Прологовское определение этого предиката следующее:
enable(T,S):-arc(S,T,S1).
Свойство живости
Для доказательства того, что переход t сетевой модели живой,
используется следующая ЛДВ-формула:
╞ init → ALL(POT(enable(t))).
Иными словами, переход t живой, если во всех состояниях сетевой
модели, начинающей свое функционирование из начального состояния,
переход t потенциально разрешен.
На языке Пролог данная формула может быть проинтерпретирована
следующим образом:
live(T):- init(S),implies(init,all(pot(enable(T))),S).
Если на запрос live(t) Пролог-система ответит yes, то переход t является
живым. Следует заметить, что может быть составлено несколько ЛДВ-
формул для проверки свойства живости перехода. Так, например, с
использованием эквивалентных соотношений, приведенных в разд. 3.1, могут
быть получены следующие формулы:
╞ init → ALL(∼ALL(∼enable(t))),
╞ init → ∼POT(ALL(∼enable(t))),
╞ init → ∼POT(∼POT(enable(t))).
Доказательство того, что сетевая модель является живой, производится с
помощью следующей формулы:
∀ t [init → ALL(POT(enable(t)))].
Заменяя квантор всеобщности квантором существования, получаем:
∼∃ t [∼(init → ALL(POT(enable(t))))].
Трансформированная таким образом ЛДВ-формула интерпретируется на
языке Пролог так:
liveness:-init(S),transition(T),
not(implies(init,all(pot(enable(T)))),S),
!,
fail.
liveness.
Eсли на запрос liveness Пролог-система ответит yes, то исследуемая
сетевая модель является живой.
Свойство мертвости
Для доказательства того, что переход t сетевой модели мертвый,
используется следующая ЛДВ-формула:
╞ init → ALL(∼enable(t)).
Иными словами, переход t мертвый, если во всех состояниях сетевой
модели, начинающей свое функционирование из начального состояния,
переход t не разрешен.
На языке Пролог данная формула может быть проинтерпретирована
следующим образом:
dead(T):- init(S),implies(init,all(not(enable(T))),S).
Если на запрос dead(t) Пролог-система ответит yes, то переход t является
мертвым.
Доказательство того, что сетевая модель является мертвой,
производится с помощью следующей формулы:
╞ ∀t [init → ALL(∼enable(t))].
Заменяя квантор всеобщности квантором существования, получаем:
╞ ∼∃t [∼(init → ALL(∼enable(t)))].
Интерпретация данной формулы на языке Пролог следующая:
deadness:- init(S),transition(T),
not(implies(init,all(not(enable(T)))),S),
!,fail.
deadness.
Если на запрос deadness Пролог-система ответит yes, то исследуемая
сетевая модель является мертвой.
Свойство потенциальной живости
Для доказательства того, что переход t сетевой модели потенциально
живой, используется следующая ЛДВ-формула:
╞ init → POT(ALL(POT(enable(t)))).
Иными словами, переход t потенциально-живой, если возможна такая
ситуация, когда он всегда имеет возможность стать разрешенным. Следует
отметить, что множество потенциально живых переходов входит в
множество условно-живых переходов, поэтому потенциально живой
переход также является и условно-живым.
На языке Пролог данная формула может быть проинтерпретирована
следующим образом:
potlive(T):- init(S),implies(init,pot(all(pot(enable(T)))),S).
Если на запрос potlive(t) Пролог-система ответит yes, то переход t
является потенциально живым.
Доказательство того, что сетевая модель является потенциально живой,
производится с помощью следующей формулы:
╞ ∀t [init → POT(ALL(POT(enable(t))))].
Заменяя квантор всеобщности квантором существования, получаем:
╞ ∼∃t [∼(init → POT(ALL(POT(enable(t)))))].
Интерпретация данной формулы на языке Пролог следующая:
potliveness:- init(S),transition(T),
not(implies(init,pot(all(pot(enable(t))))),S),
!,fail.
potliveness.
Если на запрос potliveness Пролог-система ответит yes, то исследуемая
сетевая модель является потенциально живой.
Детерминизм срабатывания переходов
Как следует из правил функционирования сетей Петри, выбор перехода
для срабатывания из множества разрешенных переходов недетерминирован.
Для некоторых приложений сетевых моделей полезно знать, срабатывает
ли конкретный переход в результате детерминированного или
недетерминированного выбора. Детерминированный выбор перехода t
случается в том случае, когда переход t появляется в списке разрешенных
переходов лишь в единственном числе. Для определения этого свойства с
использованием временной логики введем предикат fired. Истинное
значение выражения fired(t,s) означает, что при срабатывании перехода t
сетевая модель переходит в состояние s. Иными словами, существует
состояние s1, из которого есть дуга, помеченная переходом t, ведущая в
состояние s. Определим данный предикат на языке Пролог следующим
образом:
fired(T,S):- arc(S1,T,S).
Для доказательства того, что при срабатывании перехода t отсутствует
недетерминированный выбор, может использоваться следующая ЛДВ-
формула:
╞ init → ALL(enable(t)→PRETILDA(fired(t))).
Иными словами, при срабатывании перехода t отсутствует
недетерминированный выбор, если во всех состояниях сетевой модели,
начинающей свое функционирование из начального состояния из
разрешенности перехода t на следующем шаге всегда следует его
срабатывание. Следует заметить, что из состояния может выходить только
одна дуга, помеченная переходом t.
На языке Пролог данная формула может быть проинтерпретирована
следующим образом:
determ(T):- init(S),implies(init,all(implies(enable(T),
pretilda(fired(T)))),S).
Если на запрос determ(t) Пролог-система ответит yes, то переход t
cрабатывает всегда детерминированно.
3.3.2. Система с общими ресурсами
Определим, отсутствуют ли в системе из 2-х параллельных процессов,
разделяющих пару общих ресурсов (рис.2.1), тупики. Под тупиком
подразумевается такая ситуация, когда ни один из процессов не может
развиваться.
Отсутствие тупиков является одним из основных свойств систем с
параллельными процессами. Для доказательства отсутствия тупиков
достаточно показать, что соответствующая сетевая модель жива.
Определим предикат transition, используемый в теле клоза с заголовком
liveness, следующим образом:
transition(t11).
transition(t12).
transition(t13).
transition(t21).
transition(t22).
transition(t23).
На целевое утверждение liveness Пролог-интерпретатор отвечает no, что
указывает на присутствие в рассматриваемой системе тупиков.
3.3.3. Задача взаимного исключения
Покажем, что сетевая модель, представленная на рис.2.3, описывает
задачу взаимного исключения. Как было отмечено в разд. 2.2, одним из
основных свойств критической области является то, что одновременно в ней
может находиться не более одного процесса (свойство взаимного
исключения). Сформулируем данное требование в терминах сетевых
моделей и временной логики.
Определим предикат crit следующим образом:
crit(I,S):-inlist(cr(I),S).
Этот предикат истинен, если позиция cr(I) входит в состояние S.
Истинное значение выражения crit(I,S) интерпретируется как нахождение i-
го процесса в критической области. С использованием этого предиката
можно написать следующую формулу временной логики, выражающую
свойство взаимного исключения:
init ╞ ALL ∼(crit(a) & crit(b))
или, используя теорему дедукции, ее можно переписать в виде:
╞ init→ ALL ∼(crit(a) & crit(b)),
где init - предикат, определяющий начальное состояние системы. Данная
формула будет истинной, если во всех состояниях системы, начиная от
начального, всегда будет выполняться следующее условие: позиции cr(a) и
cr(b) одновременно не маркированы.
Интерпретация данной формулы на языке Пролог может быть
следующей:
implies(init,all(not(and(crit(a),crit(b)))),S).
Выполнение данного целевого утверждения приводит к положительному
результату (true), что можно интерпретировать как наличие свойства
взаимного исключения.
Покажем выполнение следующего требования, предъявляемого к
системе в данной задаче (см. разд. 2.2): "Решение о вхождении процессов в
их критические области ... не откладывается на неопределенное время, а
является конечным по времени".
Для этого определим предикат outside следующим образом:
outside(I,S):-inlist(idle(I),S).
Этот предикат истинен, если позиция idle(I) входит в состояние S.
Истинное значение выражения outside(I,S) интерпретируется как нахождение
i-го процесса вне критической области. С использованием этого предиката
можно написать следующие формулы временной логики, выражающие
отмеченное требование:
╞ init→ALL(outside(a)→INEV(crit(a)) и
╞ init→ALL(outside(b)→INEV(crit(b)).
Интерпретация первой из этих двух формул на языке Пролог будет
следующей:
implies(init,all(implies(req(a),inev(crit(a)))),S).
Вторая формула представляется аналогичным образом. Интерпретация
данных Пролог-выражений показала их истинность, следовательно,
отмеченное требование выполняется.
Докажем отсутствие тупиков в данной системе. Предикат transition,
используемый в теле клоза liveness, определяется следующим образом:
transition(T0):- index(S),tr(T),T0=..[T,S].
index(a).
index(b).
tr(seize).
tr(release).
В результате выполнения целевого утверждения liveness Пролог-
интерпретатор выдает yes (цель достигнута). Значит тупики в системе
отсутствуют.
3.3.4. Задача "обедающие философы"
Докажем отсутствие ситуации голодной смерти философов (см. рис.2.6),
иначе - отсутствие тупиков.
Определим предикат transition, используемый в клозе liveness cледующим
образом:
transition(T0):- philosopher(S),tr(T),T0=..[T,S].
philosopher(1).
philosopher(2).
philosopher(3).
philosopher(4).
philosopher(5).
tr(get).
tr(put).
Целевое утверждение liveness в этом случае истинно, следовательно,
ситуация голодной смерти отсутствует.
Докажем наличие ситуации голодания в представленной системе, или как
ее еще называют, ситуации оттеснения.
Определим предикат thinking следующим образом:
thinking(I,S):- inlist(think(I),S).
Истинное значение выражения thinkihg(I,S) интерпретируется как
размышление и желание i-го философа пообедать.
Определим предикат eating cледующим образом:
eating(I,S):-inlist(eat(I),S).
Истинное значение предиката интерпретируется как пребывание i-го
философа в состоянии потребления пищи.
Для доказательства наличия оттеснений предлагается следующая
формула:
╞∃i ∼(init→ALL(thinking(i)→INEV(eating(i)))),
истинное значение которой будет свидетельствовать о наличии оттеснений.
Интерпретация данной формулы на языке Пролог будет следующей:
starvation_free:-philosopher(I),
not(implies(init,all(implies(req(I),inev(eating(I))))),S),!.
starvation_free:-fail.
На запрос starvation_free Пролог-система ответит yes, что означает, что в
системе имеет место ситуация оттеснения.
3.3.5. Алгоритм взаимного исключения в РВС
Докажем свойство взаимного исключения. Взаимное исключение имеет
место, если для всех вариантов функционирования системы, стартующей