Warning: session_start(): open(C:\Windows\temp\sess_sda33dhipm06jadn5r6ng0uo30, O_RDWR) failed: No space left on device (28) in C:\www\lemma4.1php\login.php on line 15 Warning: session_commit(): open(C:\Windows\temp\sess_sda33dhipm06jadn5r6ng0uo30, O_RDWR) failed: No space left on device (28) in C:\www\lemma4.1php\login.php on line 36 Warning: session_commit(): Failed to write session data (files). Please verify that the current setting of session.save_path is correct (C:\Windows\temp) in C:\www\lemma4.1php\login.php on line 36 Сети Петри: модификации и расширения

Свободные от контактов ЭСС

В модели ЭСС событие может произойти в некотором состоянии, если все его предусловия выполняются и ни одно из его постусловий не выполняется в данном состоянии. Рассмотрим свойство "свободы от контактов", которое требует выполнения следующего: во всех возможных состояниях ЭСС для всех ее событий верно, что если в некотором состоянии все предусловия события выполняются, то ни одно из его постусловий не выполняется. Тогда в свободных от контактов ЭСС для того, чтобы установить, может ли событие произойти в некотором состоянии, достаточно проверить, что все его предусловия выполняются в данном состоянии. В дальнейшем мы неоднократно убедимся в важности этого свойства, которое, с одной стороны, позволяет упрощать описываемые формальные методы, а с другой не уменьшает выразительной мощности модели ЭСС.

Введем формальное определение свойства свободы от контактов.

Определение 18 Пусть N=(B,E,F,cin) ЭСС. Тогда N свободна от контактов, если верно  eEcCecec=.

Пример свободной от контактов ЭСС показан на рис. 2.1, тогда как ЭСС на рис. 2.6 не является таковой.

Рассмотрим преобразование произвольной ЭСС N в свободную от контактов ЭСС N' такую, что N и N' являются эквивалентными. Идея этого преобразования состоит в добавлении комплементарного условия каждому условию в исходной ЭСС N.

Определение 19 Пусть N=(B,E,F,cin)ЭСС. Далее, пусть B¯ множество, отличное от BE, и f:BB¯ биекция. (Через b¯ будем обозначать f(b) для каждого bB.) Тогда B-дополнение ЭСС N относительно (B¯,f) это N'=(B',E',F',cin'), где

  • B'=BB¯;
  • E'=E;
  • F'=F((e,b¯)|eE(b,e)F)((b¯,e)|eE(e,b)F);
  • cin'=cinf(B\cin).

На рис. 2.7 показана ЭСС, полученная из изображенной на рис. 2.6 ЭСС, посредством преобразования, описанного выше.

Прежде чем рассмотреть свойства такого преобразования, переопределим условие, при котором шаг может произойти в некотором состоянии ЭСС, следующим образом. Пусть N=(B,E,F,cin) ЭСС, cCN и uE. Тогда u может произойти в c, если существует c'CN такое, что (c,u,c')N. Запись c[u>N означает факт, что u может произойти в c ЭСС N. Мы часто будем опускать нижний индекс N, если ясно из контекста, что речь идет об ЭСС N. Для u={e} будем писать c[e>N вместо c[{e}>N .

Теперь можно установить ряд свойств преобразования, описанного выше.

Теорема 6 [21]. Пусть N=(B,E,F,cin)ЭСС. Далее, пусть B¯, f и N'=(B',E',F',cin')  специфицированы, как в определении 19. Тогда:

а)N'ЭСС;

б)CN'={cf(B\c)|cCN};

в)UN'=UN;

г)(c1,u,c2)N(c1f(B\c1),u,c2f(B\c2))N';

д)N'свободная от контактов ЭСС;

е)N~N'.

Доказательство. Очевидно, что N'=(B',E',F')  сеть и cin'B'. Следовательно, N'  ЭСС.

Пусть для xXN'ox={yXN'|(y,x)F'} и xo={yXN'|(x,y)F'}. Из определения N' следует, что для любого eE верно oe=ef(e) и eo=ef(e). Докажем справедливость следующего предложения, которое и будет являться ключевым в доказательстве данной теоремы.

Предложение. Пусть c1CN и c1'CN' такие, что c1'=c1f(B\c1). Тогда:

i) eE    c1[e>Nc1'[e>N';

ii) если eE может произойти в c1, то (c1'oe)eo=c2f(B\c2), где c2=(c1e)e.

Доказательство.

i) Пусть c1[e>N. Тогда ec1 и ec1=. Покажем, что oec1' и eoc1'=. Известно, что oe=ef(e). Далее, ec1c1f(B\c1)=c1'. Поскольку ec1=, то eB\c1. Следовательно, f(e)f(B\c1)c1f(B\c1)=c1'. Отсюда получаем oec1'. Так как ec1=, eB и Bf(B)=, то ec1'=. Из того, что ec1, получаем e(B\c1)=. Поскольку f - биекция, то f(e)f(B\c1)=. Очевидно, что f(e)c1=. Так как eo=ef(e), то имеем eoc1'=. Рассуждая аналогично, можно показать, что если c1'[e>N, то c1[e>N.

ii) Предположим, что e может произойти в c1. Тогда согласно пункту i) данного предложения, e также может произойти в c1'. Необходимо показать, что (c1'oe)eo=c2f(B\c2), где c2=(c1e)e. Имеем c1'oe=(c1f(B\c1))\(ef(e))=(c1e)(f(B\c1)\f(e)). Поскольку eo=ef(e), то получаем следующее: (c1'oe)eo=(c1e)(f(B\c1)\f(e))(ef(e))=((c1e)e)((f(B\c1)\f(e))f(e)). Однако верно (c1e)e=c2. Следовательно, необходимо показать, что (f(B\c1)\f(e))f(e)=f(B\c2). Предположим, что b¯f(B\c1)\f(e). Тогда bB\c1 и be. Однако bB\c1 означает bc1, что, в свою очередь, означает bc1e. Итак, имеем bc1e и be. Следовательно, b(c1e)e=c2. Таким образом, верно f(b)=b¯f(B\c2). Предположим, что b¯f(e). Тогда be и bc1e. Поскольку ee=, то be. Итак, b(c1e)e=c2. И снова мы показали, что f(b)=b¯f(B\c2). Таким образом, имеем (f(B\c1)\f(e))f(e)f(B\c2).

Покажем включение в обратную сторону. Пусть b¯f(B\c2). Значит, bB\c2. Из того, что bc2, имеем bc1e и be. Предположим bc1. Тогда be. Значит, f(b)=b¯f(e). Если bc1, то bB\c1, и тогда f(b)=b¯f(B\c1). Также нам известно, что be, и, следовательно, f(b)=b¯f(e). Поэтому bc1 влечет b¯f(B\c1)\f(e). Итак, получили обратное включение, что и завершает доказательство предложения.

Доказательство справедливости пунктов б)д) заключается в рассмотрении равенства cin'=cinf(B\cin), которое получается индукцией с применением доказанного предложения. Эквивалентность N и N' следует из предыдущих пунктов данной теоремы, определений 15, 19 и следствия 1.    □

Таким образом, требование свойства свободы от контактов не влечет потери общности. Далее покажем, что условие, когда событие может произойти, ослаблено для свободных от контактов ЭСС. Для этих целей сначала введем некоторый вариант понятия независимых событий. Пусть N=(B,E,F)  сеть и uE. Тогда

ind(u)e1,e2u    e1e2e1e2=.

Очевидно, что Ind(u) влечет ind(u), но обратное неверно в общем случае.

Теорема 7 [21]. Пусть  N=(B,E,F,cin) свободная от контактов ЭСС, cCN и uE. Тогда c[u>Nind(u)uc.

Доказательство.

(): По определению, существует состояние c'CN такое, что (c,u,c')N. Отсюда следует, что (c,u,c')Nв базовой сети N. Далее, из определения N следует, что uc и Ind(u). Кроме того, Ind(u) влечет ind(u).

(): Сначала покажем, что uc=. Рассмотрим eu. Поскольку uc, имеем ec. Так как N - свободная от контактов ЭСС, то ec=. Итак, uc=.

Далее покажем, что Ind(u), т.е. (e1e1)(e2e2)= для некоторых e1,e2u таких, что e1e2. Имеем e1e2=, поскольку ind(u). Из e1e2 следует e2c, так как e1c. Тогда верно e2c. Значит, e2c и e2c=, что противоречит свойству свободы от контактов N. Следовательно, e1e2=. Рассуждая аналогично, получим e2e1=.

Предположим, что e1e2. Известно, что e1c и e1c=. Значит, (c,e1,c1)N в базовой сети N, где c1=(ce1)e1. Однако верно cCN. Следовательно, c1CN. Так как e1e2=, то имеем e2c1. Поэтому из e1e2 следует e2c1, в силу  e1c1. Это противоречит тому, что N - свободная от контактов. Итак, мы показали, что Ind(u) и uc=. Кроме того, согласно предположению, имеем uc. Следовательно, (c,u,c')N, где c'=(cu)u. Так как cCN, то c'CN. Поэтому (c,u,c')N. Итак, c[u>.    □

Для сравнения сформулируем для всего класса ЭСС условие, когда событие может произойти.

Теорема 8 Пусть N=(B,E,F,cin) ЭСС (необязательно свободная от контактов), cCN и uE. Тогда верно c[u>NInd(u)ucuc=.

Доказательство очевидно. □