Рис. 9. Пример системы с разделенными зависимостями
Это в свою очередь означает, что верно
τ
(
S
1
,
E
2
)
H
L
τ
(
S
2
,
W
1
)
. Вме-
сте с тем субъект S
4
, содержащий единственный оператор отправки
для первой сигнальной переменной, содержит оператор захвата вто-
рого исключающего семафора, кроме того, выполнены следующие со-
отношения:
τ
(
S
3
,
L
2
)
J
L
τ
(
S
3
,
L
1
)
,
τ
(
S
5
,
L
1
)
J
L
τ
(
S
5
,
W
2
)
,
что означает справедливость отношения
τ
(
S
4
,
E
1
)
H
L
τ
(
S
5
,
W
2
)
.
Из этих соотношений следует неупорядоченность системы. Одна-
ко система является слабо локально упорядоченной, поскольку оба
эти соотношения не реализуются в одном состоянии, а именно они
требуют нахождения субъекта S
3
в двух несовместимых состояниях.
Напомним, что свойство локальной слабой упорядоченности очень
важно, поскольку оно сохраняется в процессе декомпозиции. В данном
описании представлена техника разнесения состояний вдоль одного
субъекта, позволяющая сохранять свойство слабой локальной упоря-
доченности системы.
Правило 3.
При наличии в системе субъектов с точками ветвления
или зацикливаний необходимо учитывать все возможные варианты
выполнения таких субъектов.
В качестве примера рассмотрим два субъекта на рис. 10.
Система, состоящая из субъекта S
1
, неизбежно попадет в состоя-
ние блокировки, если будет выполняться по нижней ветви точки ве-
твления, причем это произойдет независимо от начального значения
счетчика. В то же время система, состоящая из субъекта S
2
, модерни-
зирована так, чтобы не допускать состояний блокировок, поскольку
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
109
1...,5,6,7,8,9,10,11,12,13,14 16,17