Теория процессов
 Скачать 1.62 Mb.
|
|
4. Операторы проверки условия (второй вид внутренних операторов), которые представляют собой знакосочетания вида b ? где b ∈ F m. Действие, соответствующее такому оператору, исполняется путём вычисления значения формулы b на текущих значе- ниях переменных процесса P , и • если оно равно 0, то выполнение всего действия счи- тается невозможным, • иначе - выполнение действия считается завершённым. 7.3.4 Определение процесса Процессом называется пятёрка P вида P = (X P , I P , S P , s 0 P , R P ) (7.6) компоненты которой имеют следующий смысл: 1. X P – множество переменных процесса P 175 2. I P – формула, называемая начальным условием процес- са P 3. S P – множество состояний процесса P 4. s 0 P ∈ S P – начальное состояние 5. R P – подмножество вида R P ⊆ S P × O × S P Элементы множества R P называются переходами. Если переход из R P имеет вид (s 1 , op, s 2 ), то мы будем обо- значать его знакосочетанием s 1 - op s 2 и говорить, что • состояние s 1 является началом этого перехода, • состояние s 2 – его концом, • оператор op является меткой этого перехода. Также мы будем предполагать, что для каждого процесса P множество его переменных X P содержит специальную перемен- ную at P , множеством значений которой является множество S P состояний процесса P . 7.3.5 Функционирование процесса Функционирование процесса P заключается в обходе множе- ства его состояний (начиная с начального состояния s 0 P ), с вы- полнением операторов, являющихся метками проходимых пере- ходов. Более подробно: на каждом шаге функционирования i ≥ 0 • процесс находится в некотором состоянии s i (s 0 = s 0 P ) 176 • определено некоторое означивание ξ i переменных процесса P (ξ 0 (I P ) должно быть равно 1) • если есть хотя бы один переход из R P с началом в s i , то процесс – недетерминированно выбирает переход с началом в s i , помеченный таким оператором op i , который можно вы- полнить в текущий момент времени, (если таких переходов нет, то процесс временно при- останавливает свою работу до того момента, когда по- явится хотя бы один такой переход) – выполняет оператор op i , и после этого – переходит в состоние s i+1 , которое является концом выбранного перехода • если в R P нет переходов с началом в s i , то процесс закан- чивает свою работу. Для каждого i ≥ 0 означивание ξ i+1 определяется • по означиванию ξ i , и • по оператору op i , который исполняется на i–м шаге функ- ционирования процесса P . Связь между означиваниями ξ i , ξ i+1 и оператором op i имеет сле- дующий вид: 1. если op i = α ? x, и при выполнении этого оператора в про- цесс было введено сообщение v, то ξ i+1 (x) = v ∀y ∈ X P \ {x, at P } ξ i+1 (y) = ξ i (y) 2. если op i = α ! e, то при выполнении этого оператора процесс выводит сообщение ξ i (e) а значения переменных из X P \ {at P } не изменяются: ∀x ∈ X P \ {at P } ξ i+1 (x) = ξ i (x) 177 3. если op i = (x := e), то ξ i+1 (x) = ξ i (e) ∀x ∈ X P \ {x, at P } ξ i+1 (x) = ξ i (x) 4. если op i = b ? и ξ i (b) = 1, то ∀x ∈ X P \ {at P } ξ i+1 (x) = ξ i (x) Мы будем предполагать, что для каждого i ≥ 0 значение переменной at P при означивании ξ i равно тому состоянию s ∈ S P , в котором процесс P находится в момент времени i, т.е. • ξ 0 (at P ) = s 0 P • ξ 1 (at P ) = s 1 , где s 1 – конец первого перехода • ξ 2 (at P ) = s 2 , где s 2 – конец второго перехода • и т.д. 7.4 Изображение процессов в виде блок- схем В целях повышения наглядности, процессы иногда изображают в виде блок-схем. Отметим, что язык блок-схем возник в программировании, где использование этого языка позволяет существенно облегчить описание и понимание функционирования алгоритмов и программ. 7.4.1 Понятие блок-схемы Блок-схема представляет собой ориентированный граф, каж- дому узлу n которого сопоставлен оператор op(n) одного из пе- речисляемых ниже видов. Каждый узел n блок-схемы изображается в виде геометриче- ской фигуры (прямоугольника, овала или кружочка). Если op(n) не является оператором выбора или оператором соединения, то он изображается внутри этой фигуры. 178 оператор начала: ' & $ % start Init ? (7.7) где Init – формула, называемая начальным условием. оператор присваивания: ? ? x := e ? (7.8) где • x ∈ V ar, • e ∈ Expr, причём t(e) = t(x) оператор условного перехода: ? ? ' & $ % b ? - + − (7.9) где b ∈ F m. 179 оператор посылки сообщения: ? ? α ! e ? (7.10) где • α – имя (например, имя процесса, которому посылает- ся сообщение), и • e – выражение, значенем которого является посылае- мое сообщение. оператор получения сообщения: ? ? α ? x ? (7.11) где • α – имя (например, имя процесса, от которого прихо- дит сообщение), и • x – переменная, в которую следует записать получае- мое сообщение. 180 оператор выбора: ? @ @ @ @ R (7.12) оператор соединения: ? @ @ @ @ R (7.13) Иногда • кружочек, изображающий оператор соединения, не ри- суют, • и также не рисуют концы некоторых стрелок, ведущих в этот оператор т.е., например, фрагмент блок-схемы вида ? ? - 181 может быть изображён следующим образом: ? - оператор остановки: @ @ @ @ R halt (7.14) Блок-схемы должны удовлетворять следующим условиям: • узел вида (7.7) может быть только один • из узлов вида (7.7), (7.8), (7.10), (7.11), (7.13) выходит толь- ко одно ребро • из узлов вида (7.9) выходят одно или два ребра, причём – если из узла вида (7.9) выходит одно ребро, оно имеет метку “+”, и – если из узла вида (7.9) выходят два ребра, то одно из них имеет метку “+”, а другое – метку “−” • в узлы вида (7.12) входит только одно ребро • из узлов вида (7.14) не выходит ни одного ребра 7.4.2 Функционирование блок-схемы Функционирование блок-схемы представляет собой последо- вательность переходов от одного узла к другому по рёбрам, на- чиная с узла n 0 вида (7.7) (называемого начальным узлом), с выполнением операторов, сопоставленных проходимым узлам. 182 Более подробно: каждый шаг функционирования i ≥ 0 связан с некоторым узлом n i , который называется текущим узлом, и • если n i не имеет вид (7.14), то после выполнения оператора, соответствующего узлу n i , происходит переход по ребру, выходящему из n i , к следующему узлу n i+1 , который будет текущим узлом на следующем шаге функционирования • если же n i имеет вид (7.14), то функционирование блок- схемы завершается. Обозначим символом X совокупность всех переменных, вхо- дящих в блок-схему. На каждом шаге i функционирования (i = 0, 1, . . .) каждой переменной x ∈ X сопоставлено значение ξ i (x). Совокупность значений переменных {ξ i (x) | x ∈ X} обозначается символом ξ i и называется означиванием перемен- ных из X на i–м шаге функционирования блок-схемы. Значения переменных в начальный момент времени должны удовлетво- рять начальному условию, т.е. должно быть верно соотношение ξ 0 (Init) = 1 Операторы выполняются следующим образом. • Оператор (7.8) – вычисляет значение выражения e на текущем означи- вании ξ i переменных из X, и – заносит это значение в переменную x т.е. ξ i+1 (x) def = ξ i (e) ∀ y ∈ X \ {x} ξ i+1 (y) def = ξ i (y) • Оператор (7.9) вычисляет значение формулы b на текущем означивании ξ i переменных из X, и – если ξ i (b) = 1, то происходит переход к следующему узлу по ребру с меткой “+”, 183 – иначе - ∗ если из текущего узла выходят два ребра, то про- исходит переход к следующему узлу по ребру с меткой “−”, и ∗ если из текущего узла выходит одно ребро, то в данный момент времени выполнение оператора, со- ответствущего текущему узлу, считается невозмож- ным. • Оператор (7.10) может выполниться в текущий момент вре- мени только в том случае, когда в этот момент времени процесс может послать объект с именем α. Если это возможно, то выполняется посылка α ! ξ i (e) • Оператор (7.11) может выполниться в текущий момент вре- мени только в том случае, когда в этот момент времени процесс может принять объект с именем α. Если это возможно, то – этот объект принимается, – сообщение v, содержащееся в этом объекте, записыва- ется в переменную x, т.е. ξ i+1 (x) def = v ∀y ∈ X \ {y} ξ i+1 (y) def = ξ i (y) • Если текущий узел помечен оператором (7.12), то – из рёбер, которые из него выходят, выбирается ребро, ведущее в узел, помеченный таким оператором, кото- рый возможно выполнить в текущий момент времени, и – происходит переход в этот узел. (если таких операторов, которые возможно выполнить в те- кущий момент времени, несколько, то выбор производится недетерминированно) 184 • Оператор (7.14) завершает функционирование блок-схемы. 7.4.3 Построение процесса, определяемого блок- схемой Алгоритм построения процесса по блок-схеме имеет следующий вид. 1. На каждом ребре блок-схемы рисуется точка. 2. Для • каждого узла n блок-схемы, который не имеет вида (7.12) или (7.13), и • каждой пары F 1 , F 2 рёбер блок-схемы, таких что F 1 входит в n, а F 2 - выходит из n выполняются следующие действия: (a) рисуется стрелка f , соединяющая точку на F 1 с точкой на F 2 , (b) на этой стрелке f рисуется метка hf i, определяемая следующим образом: i. если op(n) имеет вид (7.8), то hf i def = (x := e) ii. если op(n) имеет вид (7.9), и ребро, выходящее из n, помечено символом “+”, то hf i def = b ? iii. если op(n) имеет вид (7.9), и ребро, выходящее из n, помечено символом “−”, то hf i def = ¬b ? iv. если op(n) имеет вид (7.10) или (7.11), то hf i сов- падает с op(n). 185 3. Для каждого узла n вида (7.12) и каждого ребра F , выхо- дящего из n, выполняются следующие действия: • стрелка, соответствующая тому узлу, в который вхо- дит F , заменяется на стрелку – с тем же концом и с той же меткой, – но с началом – на ребре, входящем в n • точка на ребре F удаляется. 4. Для каждого узла n вида (7.13) и каждого ребра F , входя- щего в n, выполняются следующие действия: • стрелка, соответствующая тому узлу, из которого вы- ходит F , заменяется на стрелку – с тем же началом и с той же меткой, – но с концом – на ребре, выходящем из n • точка на ребре F удаляется. 5. Состояниями искомого процесса являются оставшиеся на- рисованные точки. 6. Начальное состояние s 0 P определяется следующим образом. • Если точка, нарисованная на том ребре блок-схемы, которое выходит из её начального узла, не была уда- лена, то эта точка является начальным состоянием s 0 P • Если же эта точка была удалена, то нетрудно заме- тить, что это могло произойти только в том случае, когда концом ребра, выходящего из начального узла блок-схемы, является узел n вида (7.13). В этом слу- чае начальным состоянием s 0 P является точка, нарисо- ванная на ребре, выходящем из n. 7. Переходы процесса соответствуют нарисованным стрелкам: для каждой такой стрелки f процесс содержит переход s 1 - hf i s 2 где s 1 и s 2 – начало и конец стрелки f соответственно. 186 8. Множество переменных процесса содержит • все переменные, входящие в какой-либо из операторов блок-схемы, • а также переменную at P 9. Начальное условие процесса совпадает с начальным усло- вием Init блок-схемы. 7.5 Пример процесса с передачей сооб- щений В этом параграфе мы рассмотрим в качестве примера процесс “буфер”: • сначала мы определим этот процесс в виде блок-схемы, и • затем мы построим по этой блок-схеме представление про- цесса “буфер” в стандартной форме. 7.5.1 Понятие буфера Пусть n – некоторое положительное целое число. Под буфером размера n мы в этом параграфе будем по- нимать систему (называемую ниже просто буфером), которая обладает следующими свойствами. • В буфер можно вводить символы. Символы, введённые в буфер, можно выводить из буфера. Если некоторый символ c введён в буфер, то мы будем го- ворить, что символ c содержится в буфере (до тех пор пока этот символ не будет выведен из буфера). В буфере может одновременно содержаться не более n сим- волов. 187 • В каждый момент времени совокупность символов, содер- жащихся в буфере, представляет собой упорядоченную по- следовательность c 1 , . . . , c k (0 ≤ k ≤ n) (7.15) которая называется содержимым буфера. Число k на- зывается размером содержимого буфера. Случай k = 0 соответствует ситуации, когда в буфере не содержится ни одного символа, в этом случае мы будем говорить, что буфер пуст. • Если в текущий момент времени содержимое буфера имеет вид (7.15), и k < n, то в буфер можно ввести произвольный символ c, и после выполнения этой операции содержимое буфера примет вид c 1 , . . . , c k , c • Если в текущий момент времени содержимое буфера имеет вид (7.15), и k > 0, то из буфера можно вывести символ, расположенный в начале его содержимого (т.е. c 1 ), после выполнения этой операции содержимое буфера примет вид c 2 , . . . , c k Таким образом, в каждый момент времени содержимое буфе- ра представляет собой очередь символов, причём • каждая операция ввода символа в буфер добавляет вводи- мый символ в конец этой очереди, и • каждая операция вывода символа из буфера – выводит из буфера первый элемент этой очереди, и – удаляет этот элемент из очереди Очереди, операции с которыми выглядят описанным выше об- разом, называются очередями типа FIFO (First Input - First Output). 188 7.5.2 Представление поведения буфера в виде блок-схемы Одним из возможных формальных уточнений понятия буфера является процесс Buffer n , описание которого приводится в этом параграфе в виде блок-схемы. В этом процессе • операция ввода символа в буфер представляется действием с именем In, и • операция вывода символа из буфера представляется дей- ствием с именем Out. Процесс Buffer n имеет следующие переменные: • переменная n типа int, её значение не изменяется, оно рав- но максимальному размеру содержимого буфера • переменная k типа int, её значение равно размеру содер- жимого буфера в текущий момент времени • переменная q типа string, её значение равно содержимому буфера в текущий момент времени • переменная f типа char, в эту переменную будут записы- ваться вводимые символы при выполнении операции ввода. Блок-схема, представляющая процесс Buffer n , имеет следу- ющий вид (используемые в этой блок-схеме обозначения были определены в параграфе 7.2.3): 189 ' & $ % start n > 0 q = ε k = 0 k < n k > 0 Out ! ˆ q q := q 0 k := k − 1 In ? f q := q · [f ] k := k + 1 - ? ? ? ? ? ? ? − − + + - ? ? 7.5.3 Представление поведения буфера в виде процесса Для построения процесса Buffer n , который соответствует опре- делённой выше блок-схеме, мы нарисуем точки на её рёбрах: 190 s A s B s C s F s G s H s D s E s L s M s K s N s O s P ' & $ % start n > 0 q = ε k = 0 k < n k > 0 Out ! ˆ q q := q 0 k := k − 1 In ? f q := q · [f ] k := k + 1 - ? ? ? ? ? ? ? − − + + - ? ? При построении процесса по этой блок-схеме будут удалены точки A, G, H, K и N . Искомый процесс Buffer n имеет следующий вид: 191 B D C E L F M ? @ @ @ @ @ @ @ @ @ R ? ? ? ? - - O P - k := k + 1 k := k − 1 In ? f Out ! ˆ q q := q · [f ] q := q 0 In ? f Out ! ˆ q (k > 0) ? (k < n) ? (k ≤ 0) ? (k ≥ n) ? 7.6 Операции на процессах с передачей сообщений Операции на процессах с передачей сообщений аналогичны опе- рациям на процессах в исходном смысле данного понятия (см. главу 3). 7.6.1 Префиксное действие Пусть заданы процесс P и оператор op. Процесс op.P получается из процесса P добавлением • к множеству его состояний – нового состояния s, которое является начальным в op.P , • к множеству переходов – нового перехода с меткой op из s в s 0 P • к множеству переменных – всех переменных, входящих в op. 192 7.6.2 Альтернативная композиция Пусть процессы P 1 и P 2 таковы, что S P 1 ∩ S P 2 = ∅. Тогда можно определить процесс P 1 + P 2 , называемый аль- тернативной композицией процессов P 1 и P 2 : • множества его состояний, переходов, и начальное состояние определяются так же, как определяются соответствующие компоненты процесса P 1 + P 2 в главе 3 • X P 1 +P 2 def = X P 1 ∪ X P 2 • I P 1 +P 2 def = I P 1 ∧ I P 2 Если же S P 1 ∩ S P 2 6= ∅, то для определения процесса P 1 + P 2 сначала надо заменить в P 2 те состояния, которые входят также и в P 1 , на новые элементы, и модифицировать соответствующим образом другие компоненты P 2 7.6.3 Параллельная композиция Пусть процессы P 1 и P 2 таковы, что X P 1 ∩ X P 2 = ∅. Тогда можно определить процесс P 1 | P 2 , называемый парал- лельной композицией процессов P 1 и P 2 : • множество его состояний и начальное состояние определя- ются так же, как определяются соответствующие компо- ненты процесса P 1 | P 2 в главе 3 • X P 1 +P 2 def = X P 1 ∪ X P 2 • I P 1 +P 2 def = I P 1 ∧ I P 2 • множество переходов процесса P 1 | P 2 определяется следу- ющим образом: – для ∗ каждого перехода s 1 - op s 0 1 процесса P 1 , и ∗ каждого состояния s процесса P 2 193 процесс P 1 | P 2 содержит переход (s 1 , s) - op (s 0 1 , s) – для ∗ каждого перехода s 2 - op s 0 2 процесса P 2 , и ∗ каждого состояния s процесса P 1 процесс P 1 | P 2 содержит переход (s, s 2 ) - op (s, s 0 2 ) – для каждой пары переходов вида s 1 - op 1 s 0 1 ∈ R P 1 s 2 - op 2 s 0 2 ∈ R P 2 где ∗ один из операторов op 1 , op 2 имеет вид α ? x, ∗ а другой – α ! e, причём t(x) = t(e) (имя в обоих операторах – одно и то же) процесс P 1 | P 2 содержит переход (s 1 , s 2 ) - x := e (s 0 1 , s 0 2 ) Если же X P 1 ∩ X P 2 6= ∅, то для определения процесса P 1 | P 2 сначала надо заменить в одном из процессов те переменные, ко- торые входят также и в другой процесс, на новые переменные. 7.6.4 Ограничение Пусть заданы процесс P и подмножество L ⊆ N ames. Ограничением P по L называется процесс P \ L который получается из P удалением тех переходов, метки кото- рых содержат имена из L. 194 7.6.5 Переименование Пусть заданы процесс P и функция f : N ames → N ames. Действие операции переименования [f ] на процесс P заклю- чается в изменении имён в метках переходов: каждое имя α в какой-либо из этих меток заменяется на f (α). Получившийся процесс обозначается знакосочетанием P [f ]. Если f действует нетождественно лишь на имена из списка α 1 , . . . , α n и отображает их в имена β 1 , . . . , β n соответственно, то для P [f ] мы будем иногда использовать эк- вивалентное обозначение P [β 1 /α 1 , . . . , β n /α n ] 7.7 Эквивалентность процессов 7.7.1 Понятие конкретизации процесса Пусть P – произвольный процесс. Обозначим знакосочетанием Conc(P ) процесс в исходном смысле данного понятия (см. пара- граф 2.4), который называется конкретизацией процесса P , и имеет следующие компоненты. 1. Состояниями Conc(P ) являются • всевозможные означивания из Eval(X P ), • а также дополнительное состояние s 0 , которое являет- ся начальным в Conc(P ) 2. Для • каждого перехода s 1 - op s 2 процесса P , и • каждого означивания ξ ∈ Eval(X P ), такого, что ξ(at P ) = s 1 195 Conc(P ) содержит переход ξ - a ξ 0 если ξ 0 (at P ) = s 2 , и имеет место один из следующих случа- ев: • – op = α ? x, a = α ? v, где v – произвольное значе- ние из D t(x) – ξ 0 (x) = v, ∀y ∈ X P \ {x, at P } ξ 0 (y) = ξ(y) • – op = α ! e, a = α ! ξ(e) – ∀x ∈ X P \ {at P } ξ 0 (x) = ξ(x) • – op = (x := e), a = τ – ξ 0 (x) = ξ(e), ∀y ∈ X P \ {x, at P } ξ 0 (y) = ξ(y) • – op = b ?, ξ(b) = 1, a = τ – ∀x ∈ X P \ {at P } ξ 0 (x) = ξ(x) 3. Для • каждого означивания ξ ∈ Eval(X P ), такого, что ξ(I P ) = 1 • и каждого перехода в Conc(P ) вида ξ - a ξ 0 Conc(P ) содержит переход s 0 - a ξ 0 Из определений • понятия функционирования процесса с передачей сообще- ний (см. пункт 7.3.5), и • понятия функционирования процесса в исходном смысле (см. пункт 2.4) следует, что имеется взаимно однозначное соответствие между • множеством всех вариантов функционирования процесса P , и 196 • множеством всех вариантов функционирования его конкре- тизации Conc(P ). Читателю предлагается самостоятельно исследовать переста- новочность функции Conc с операциями на процессах, т.е. уста- новить истинность или ложность соотношений вида Conc(P 1 | P 2 ) = Conc(P 1 ) | Conc(P 2 ) и т.п. 7.7.2 Понятие эквивалентности процессов На множестве процессов с передачей сообщений можно опреде- лить те же отношения эквивалентности, которые можно опре- делить для процессов в исходном смысле данного понятия (см. главу 4). Мы будем считать, что любые два процесса с передачей со- общений P 1 , P 2 по определению находятся в том же самом отно- шении эквивалентности (∼, ≈, + ≈, . . .), в котором находятся их конкретизации, т.е. P 1 ∼ P 2 ⇔ Conc(P 1 ) ∼ Conc(P 2 ), и т.д. Читателю предлагается самостоятельно • исследовать связь операций на процессах с различными от- ношениями эквивалентности, т.е. установить свойства, ана- логичные свойствам, изложенным в параграфах 3.7, 4.5, 4.8.4, 4.9.5 • сформулировать и обосновать необходимые и достаточные условия эквивалентности (≈, + ≈, . . .) процессов, не исполь- зующие понятие конкретизации процесса. 197 7.8 Процессы с составными оператора- ми 7.8.1 Мотивировка понятия процесса с состав- ными операторами Сложность задачи анализа процесса существенно зависит от раз- мера его описания (в частности, от количества состояний). По- этому для построения эффективных алгоритмов анализа про- цессов необходим поиск методов понижения сложности описания анализируемых процессов. В этом параграфе мы рассматриваем один из таких методов. Мы обобщаем понятие процесса до понятия процесса с состав- ными операторами. Составной оператор является комбинацией нескольких обычных операторов. За счёт того, что мы объеди- няем последовательность обычных операторов в один составной, у нас появляется возможность исключить из описания процесса те состояния, в которых он находится на промежуточных шагах выполнения этой последовательности операторов. Мы определяем понятие редукции процессов с составными операторами, с таким расчётом, чтобы при выполнении редук- ции получался процесс, • имеющий менее сложное описание, и • эквивалентный (в некотором смысле) исходному процессу. С использованием описанных выше понятий задача анализа процесса может решаться следующим образом. 1. Сначала мы сопоставляем исходному процессу P процесс P 0 с составными операторами, в некотором смысле совпадаю- щий с P (говоря неформально, мы просто рассматриваем каждый оператор, входящий в P , как составной оператор). 2. Затем мы редуцируем P 0 , получая процесс P 00 , сложность которого может быть существенно меньше сложности ис- ходного процесса P . 198 3. После этого мы выполняем анализ процесса P 00 , и по ре- зультатам этого анализа мы составляем заключение о свой- ствах исходного процесса P . 7.8.2 Понятие составного оператора Составным оператором (СО) называется конечная последо- вательность Op операторов Op = (op 1 , . . . , op n ) (n ≥ 1) (7.16) обладающая следующими свойствами: 1. op 1 является оператором проверки условия, формулу, входящую в этот оператор, мы будем обозначать знакосочетанием cond (Op) 2. последовательность (op 2 , . . . , op n ) • не содержит операторов проверки условия, и • содержит не более одного оператора ввода или вывода. Пусть Op – некоторый СО. • Op называется СО ввода (или вывода), если среди опера- торов, входящих в Op, есть оператор ввода (или вывода). • Op называется внутренним, если все операторы, входя- щие в Op – внутренние. • Если Op является СО ввода или вывода, то знакосочетание name (Op) обозначает имя, входящее в Op. • Если ξ – некоторое означивание переменных, входящих в cond (Op), то мы будем говорить, что Op открыт на ξ, если ξ(cond (Op)) = 1 199 7.8.3 Понятие процесса с СО Понятие процесса с СО отличается от понятия процесса из параграфа 7.3.4 только тем, что метки переходов у процесса с СО представляют собой СО. 7.8.4 Функционирование процесса с СО Функционирование процесса с СО • определяется почти так же, как определяется функциони- рование процесса в параграфе 7.3.5, и • тоже представляет собой обход множества его состояний (начиная с начального состояния), с выполнением СО, яв- ляющихся метками проходимых переходов. Пусть P = (X P , I P , S P , s 0 P , R P ) - процесс с СО. На каждом шаге функционирования i ≥ 0 • процесс P находится в некотором состоянии s i (s 0 = s 0 P ) • определено некоторое означивание ξ i переменных из X P (ξ 0 (I P ) = 1, ξ i (at P ) = s i ) • если есть хотя бы один переход из R P с началом в s i , то процесс – недетерминированно выбирает переход с началом в s i , помеченный таким СО Op i , который обладает следу- ющими свойствами: ∗ Op i открыт на ξ i ∗ если среди операторов, входящих в Op i , есть опе- ратор вида α ? x или α ! e то процесс P может в текущий момент времени выполнить действие вида α ? v или α ! v соответственно 200 (если таких переходов нет, то процесс временно при- останавливает свою работу до того момента, когда по- явится хотя бы один такой переход) – выполняет последовательно все операторы, входящие в Op i , изменяя соответствующим образом текущее озна- чивание после выполнения каждого оператора, входя- щего в Op i , и после этого – переходит в состояние s i+1 , которое является концом выбранного перехода • если в R P нет переходов с началом в s i , то процесс закан- чивает свою работу. 7.8.5 Операции на процессах с СО Определения операций на процессах с СО почти совпадают с соответствующими определениями из параграфа 7.6, поэтому мы лишь укажем отличия в этих определениях. • В определениях всех операций на процессах с СО вместо операторов участвуют СО. • Определение операции | отличается только в том пункте, в котором определяются “диагональные” переходы. Для про- цессов с СО данный пункт выглядит следующим образом: для каждой пары переходов вида s 1 - Op 1 s 0 1 ∈ R P 1 s 2 - Op 2 s 0 2 ∈ R P 2 где один из СО Op 1 , Op 2 имеет вид (op 1 , . . . , op i , α ? x, op i+1 , . . . , op n ) а другой – (op 0 1 , . . . , op 0 j , α ! e, op 0 j+1 , . . . , op 0 m ) где 201 – t(x) = t(e), – подпоследовательности (op i+1 , . . . , op n ) и (op 0 j+1 , . . . , op 0 m ) могут быть пустыми процесс P 1 | P 2 содержит переход (s 1 , s 2 ) - Op (s 0 1 , s 0 2 ) где Op имеет вид (cond (Op 1 ) ∧ cond (Op 2 )) ?, op 2 , . . . , op i , op 0 2 , . . . , op 0 j , (x := e), op i+1 , . . . , op n , op 0 j+1 , . . . , op 0 m 7.8.6 Преобразование процессов с передачей со- общений в процессы с СО Каждый процесс с передачей сообщений можно преобразовать в процесс с СО путём замены меток его переходов: для каждого перехода s 1 - op s 2 его метка op заменяется на СО Op, определяемый следующим образом. • Если op – оператор проверки условия, то Op def = (op) • Если op – оператор присваивания, ввода или вывода, то Op def = (>? , op) где > – тождественно истинная формула. Для каждого процесса с передачей сообщений P мы будем обозначать соответствующий ему процесс с СО тем же символом P . 202 7.8.7 Конкатенация СО В этом параграфе мы вводим понятие конкатенации СО: для некоторых пар СО (Op 1 , Op 2 ) мы определяем СО, обозначаемый знакосочетанием Op 1 · Op 2 (7.17) и называемый конкатенацией Op 1 и Op 2 СО (7.17) отражает идею последовательного выполнения опе- раторов из Op 1 и Op 2 : в (7.17) • сначала выполняются операторы, входящие в Op 1 , • а затем - операторы, входящие в Op 2 Необходимым условием для того, чтобы можно было опреде- лить конкатенацию (7.17), является условие того, чтобы хотя бы один из СО Op 1 , Op 2 был внутренним. Ниже мы будем использовать следующие обозначения. 1. Для каждого • СО Op = (op 1 , . . . , op n ), и • оператора присваивания op знакосочетание Op · op обозначает СО (op 1 , . . . , op n , op) (7.18) 2. Для каждого • внутреннего СО Op = (op 1 , . . . , op n ), и • оператора ввода или вывода op знакосочетание Op · op обозначает СО (7.18) 3. Для каждого • СО Op = (op 1 , . . . , op n ), и |