Конспект установочных лекций по комплексному курсу Информатика, Теория информации
Сети Петри - часть 11
Определенные последовательности действий одного агента должны выполняться без того, чтобы параллельно происходили определенные действия другого агента, например, для избежания конфликтов между действиями. С помощью синхронной параллельной композиции t1 ||s t2, порождается процесс, который (при отсутствии возникновения тупиков) содержит определенные линеаризации ходов работы t1 и t2, как частичных процессов. Возникают дальнейшие причинные отношения между событиями в обоих частичных процессах - это следует ввести для обеспечения взаимных исключений.
Пример (взаимное исключение через пару синхронизируемых действий). Пусть даны следующие три агента:
t1 = х1 :: а1 ; p; b1; v; х1
t2 = х2 :: а2 ; р; b2; v; х2
k = y :: p; v; y.
Предположим, что действия b1 и b2 могут конфликтовать между собой и поэтов не должны выполняться параллельно. Для агента t1 || t2 возможен ход работы, заданный с помощью следующего графа действий:
а1 -> р -> b1
-> v -> а1 -> р -> b1 -> v -> ...
а2 -> р -> b2
-> v -> а2 -> р -> b2 -> v -> ...
Этот процесс содержит пару параллельных событий, которые помечены конфликтующими действиями b1 и b2. В агенте
(t1 || t2) || {v; p}k такой ход работы исключается. Каждое выполнение действий р и v агента k совпадает с одними из действий р и v или агента t1, или агента t2, но что р и v - действия в процессах t1 и t2 не помечают каких-либо общих событий.
Методика обеспечения взаимных исключений, описанная в примере для агентов, может быть использована в более общих случаях. Пусть а - действие, находящееся в конфликте с самим собой, которое встречается сколь угодно часто в агентах t1
и t2. В агентах t1 и t2 заменим действие а на терм агентов Р ; a; v, причем пусть р и v - до сих пор не встречавшиеся действия в t1 и t2 . Агент с :: р; v; с в каждом ходе работы агента по мере надобности вынуждает один из обоих агентов ti' или ti ждать с выполнением р; а; v-до тех пор, пока агент с::р; v; с снова будет готов для события, помеченного действием р.
