Warning: session_start(): open(C:\Windows\temp\sess_f5l0sgu4kgtq8iij790of2o3h3, 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_f5l0sgu4kgtq8iij790of2o3h3, 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 Сети Петри: модификации и расширения

В общих словах, раскрашенные сети Петри [8, 9] являются расширением обычных сетей Петри за счет связывания с каждой фишкой раскрашенной СП значения некоторого типа — цвета. Это значение может быть произвольно сложного типа. Функционирование раскрашенной СП зависит не только от наличия фишек во входных местах переходов, но также и от их цвета.

Спецификация раскрашенной СП включает в себя описание структуры (места, переходы, дуги), декларации и пометки элементов сети специальными выражениями. Структура  раскрашенной СП задается сетью. Декларации  раскрашенной СП состоят из описания множеств цветов (типов) и объявления переменных, каждая из которых принимает значения из некоторого множества цветов. Декларации также могут содержать определения операций и функций. Для спецификации деклараций используется язык CPN ML [9].  Пометка  мест, переходов и дуг раскрашенной СП выражениями используется для описания правил распределения и перемещения фишек. Место помечается именем места, множеством цветов и инициализирующим выражением. Имя места служит для идентификации. Множество цветов, сопоставленное месту, определяет цвета, которые должны иметь фишки, находящиеся в данном месте. Инициализирующее выражение, сопоставленное месту, при означивании фактически определяет начальную маркировку данного места, которая в графическом представлении раскрашенной СП изображается мультимножеством, подчеркнутым снизу. Переходам сопоставляются имена и выражения (предохранители). Предохранитель перехода — логическое выражение, которое должно иметь истинное значение до того, как переход сможет сработать. Выражения, сопоставленные дугам, могут содержать переменные, константы, функции и операции, определенные в декларациях. Все переменные, входящие в выражение перехода и в выражения, сопоставленные его входным и выходным дугам, будем называть переменными перехода.

Чтобы говорить о срабатывании перехода, сначала необходимо определить значения переменных перехода. При этом вместо всех вхождений одной и той же переменной подставляются одно и то же значение. Набор значений переменных, при которых предохранитель перехода имеет истинное значение, называется связыванием. Значение выражения дуги при выбранном связывании определяет мультимножество фишек, которые могут быть "перемещены" по этой дуге. Переход раскрашенной СП  может сработать при некоторой маркировке, если в каждом его входном месте имеются фишки с цветом и в количестве, определенными значением выражения соответствующей входной дуги перехода при некотором связывании. При срабатывании перехода фишки удаляются из его входных мест и добавляются в его выходные места. Количество и цвет удаляемых/добавляемых фишек определяются значениями выражений на соответствующих дугах при заданном связывании.

Сначала введем вспомогательные понятия и обозначения, необходимые для опреления раскрашенной СП.

Мультимножество m над непустым множеством  S  — это функция m[SN]. Пусть SMS обозначает мультимножество над множеством S. Неотрицательное число m(s)N — количество элементов sS в SMS — называется коэффициетом  элемента s. Мультимножество представляется в виде суммы sSm(s)s. Элемент s  принадлежит  мультимножеству SMS, если m(s)&neq;0. Пусть обозначает пустое мультимножество. Примерами мультимножеств могут служить: m1=1a+2c+1e и m2=1a+2b+3c+1e. Операции над мультимножествами — сложение, вычитание, скалярное умножение, сравнение — определяются естественным образом. Например, m1+m2=sS(m1(s)+m2(s))s, то есть m1+m2=2a+2b+5c+2e.

Прежде чем ввести формальное определение раскрашенной СП, введем еще ряд вспомогательных обозначений. Пусть T обозначает тип (множество цветов). Иногда T будет также обозначать множество элементов типа T. Пусть V  — множество переменных. Для переменной v запись Type(v)  обозначает ее тип. Тогда Type(V) = {Type(v)  | vV} — множество типов переменных из V. Через Expr  обозначим множество выражений. Для выражения expr  запись Type(expr)  обозначает его тип, а Var(expr)  — множество переменных, встречающихся в expr. Пусть B  = {true, false} — логический тип, состоящий из логических констант.

Теперь перейдем к формальному определению раскрашенной СП. Приведенные ниже комментарии также являются частью определения.

Определение 51 Раскрашенной СП (РСП) называется кортеж CN = (Σ,S,T,A,N,C,G,E,I), удовлетворяющий следующим условиям:

(а)  Σ  конечное множество типов (множеств цветов);
(б)  S  множество мест;
(в)  T 
множество переходов;
(г)  A  множество дуг;
(д)  N:A(S×TT×S) — функция вершин;
(е)
  C:SΣ — функция цвета;
(ж)
G:T Expr  функция выражений переходов (предохранитель) такая, что
tT    [Type(G(t)) = B Type(Var(G(t)) Σ];
(з)
ϵ:A Expr  функция выражений дуг такая, что
aA    [Type(s (a)) = C(s(a))MS(Var(s (a)) Σ], где s(a)  место в дуге a;
(и)
I:S Expr  функция инициализации мест такая, что sS   [Type(I(s))=C(s)MS].

Приведенные ниже пояснения являются частью определения.

(а) Множество Σ цветов определяет типы, операции и функции, которые могут быть использованы в пометке сети. Считается, что каждое множество цветов содержит хотя бы один элемент.

(б-г) Множества мест, переходов, дуг должны быть конечными и различными. В отличие от обычных СП выше указанные множества могут быть пустыми, а также множество дуг — это отдельное множество, не являющее подмножеством множества (S×TT×S). Из последнего следует, что между двумя элементами сети может быть более, чем одна дуга.

(д)  Функция N вершин отображает каждую дугу в пару вершин — начало и конец дуги. Эти две вершины должны быть разного типа.

(е)  Функция C цвета сопоставляет каждому месту s  множество цветов C(s). Интуитивно это означает, что каждая фишка в месте s  должна иметь цвет из множества C(s).

(з) Фукция G выражений переходов сопоставляет каждому переходу t булево выражение G(t). Более того, все переменные в выражении G(t)  должны иметь тип, принадлежащий множеству Σ. В случае, когда выражение перехода не специфицировано явно, оно рассматривается как замкнутое выражение true.

(ж)  Функция E выражений дуг сопоставляет каждой дуге a  выражение E(a), которое должно иметь тип C(s)MS, т.е. каждое означивание выражения дуги должно давать мультимножество над множеством цветов, сопоставленное соответствующему месту. В случае, когда выражение дуги не специфицировано явно, оно рассматривается как пустое мультимножество. Более того, все переменные в выражении E(a) должны иметь тип, принадлежащий множеству Σ.

(и) Функция I инициализации сопоставляет каждому месту замкнутое выражение, которое должно иметь тип C(s)MS. В случае, когда инициализация места не специфицирована явно, она рассматривается как пустое мультимножество.

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

(а) Σ={U,I,PR,ER};

(б) S={A,B,C,P,R};

(в) T={T1,T2,T3};

(г) A={(AtoT1),(T1toB),(BtoT2),...,(PtoT1),(RtoT1)};

(д) N(AtoT1)=(A,T1),N(T1toB)=(T1,B), и т.д.

(е) C(s)={PR,s{A,B,C},ER,иначе;

(ж) G(t)={x=q,t=T1,true,иначе.

(з) ϵ(a)={e,a{(RtoT1),(PtoT1)},2'e,a=(T3toP),...

(и) I(s)={3(q,0),s=A,2(p,0),s=B,1e,s=R,3e,s=P,,иначе.

Теперь перейдем к рассмотрению поведения РСП.

Введем вспомогательные понятия и обозначения. Пусть X=ST и x,x1,x2X. Тогда:

  • A[(S×T)(T×S)2A], т.е. A(x1,x2)=aA|N(a)=(x1,x2) (множесво дуг, связывающих элементы x1 и x2);
  • A[X2A], т.е. A(x)=aA|&exists;xX [N(a)=(x,x)N(a)=(x,x)] (множество дуг, входящих и исходящих из элемента x);
  • tT    Var(t)={v|vVar(G(t))&exists;aA(t)    vVar(E(a))} (множество переменных перехода t, встречающихся в выражении, связанном с t,  и в выражениях, связанных с входящими и выходящими дугами t);
  • (x1,x2)(S×T)(T×S)   E(x1,x2)=aA(x1,x2)E(a).

Введем понятие связывания перехода. Неформально говоря, связывание перехода означает замену каждой переменной данного перехода на цвет, который должен быть корректного типа, а также предохранитель перехода должно иметь истинное значение.

Связывание перехода t — это функция b, определенная на множестве Var(t) такая, что выполняются условия:

(a) vVar(t)   b(v)Type(v);

(б) G(t)b.

Пусть G(t)b обозначает означивании выражения G(t) при связывании b. Далее, пусть B(t) обозначает множество связываний перехода t. Например, в раскрашенной СП, приведенной на рис. 3.12, имеем: B(T1)={x=q,i=0,x=q,i=1,...}.

Элемент-связывание — это пара (t,b), где tT и bB(t). Пусть BE — множество всех элементов-связываний. Элемент-фишка — это пара (p,c), где pS и cC(s). Пусть TE — множество всех элементов-фишек.

Например, в РСП, приведенной на рис. 3.12, имеем: BE={(T1,x=q,i=0), (T1,x=q,i=1), ..., (T2,x=p,i=0), ...} и TE={(A,(p,0)), (A,(p,1)), ..., (A,(q,0)), (A,(q,1)), ..., (R,e), (S,e), ...}.

Маркировка M — это мультимножество над множеством TE. Пусть M(CN) — множество всех маркировок в CN. Начальная маркировка M0 — это маркировка, получаемая посредством означивания инициализации мест:

(s,c)TE    M0(s,c)=(I(s))(c).

Начальная маркировка РСП, приведенной на рис. 3.12, может быть представлена в виде мультимножества

M0=3'(A,(q,0))+2'(B,(p,0))+1'(R,e)+3'(S,e).

Каждая маркировка MTEMS определяет уникальную функцию M', определенную на множестве S так, что M'(s)=C(s)MS :

sScC(s)   (M(s))(c)=M(s,c).

С другой стороны, каждая функция M', определенная на множестве S так, что M'(s)=C(s)MS  для всех sS, определяет уникальную маркировку M:

(s,c)TE    M(s,c)=(M(s))(c).

Например, начальная маркировка раскрашенной СП, приведенной на рис. 3.12, может быть представлена в виде функции

M0(s)=3'(A,(q,0)),s=A,2'(B,(p,0)),s=B,1'(R,e),s=R,3'(S,e),s=S,,иначе.

Шаг Y — это непустое конечное мультимножество над множеством BE. Пусть Y(CN) — множество всех шагов в CN. Также существует уникальное соответствие между шагом Y  и функцией Y', определенной на T  такой, что мультимножество Y(t)B(t)MS конечно и непусто по крайней мере для одного перехода tT. Таким образом, мы можем представлять шаги как функции, определенные на T.

Означивание выражения  E(s,t)b(E(t,s)b) дает мультимножество над множеством TE.

Шаг Y может сработать при маркировке M, если

sS   (t,b)YE(s,t)bM(s).

Например, в раскрашенной СП, приведенной на рис. 3.12, шаг {(T1,<x=q,i=0>), (T2,<x=p,i=0>)} может сработать при маркировке M0 .

Пусть шаг Y может сработать при маркировке M. Если (t,b)Y, то будем говорить, что (t,b) (t) может сработать (при связывании bпри маркировке M. Если (t1,b2),(t2,b2)Y и (t1,b2)(t2,b2), то будем говорить, что (t1,b2) и (t2,b2)(t1 и t2)могут сработать параллельно (при связывании b) при маркировке M. Когда Y(t,b)2|(Y(t))|2, то (t,b) (t) может сработать параллельно с самим собой при маркировке M.

В случае, когда шаг Y  может сработать при маркировке M1, его срабатывание приводит к маркировке M2 такой, что:

sS    M2(s)=(M1(s)-(t,b)Yϵ(s,t)b)+(t,b)YE(t,s)b.

Первая сумма определяет удаляемые фишки, а вторая сумма — добавляемые фишки при срабатывании шага Y. Запись M1[Y>M2 означает, что M2непосредственно достижима из M1 посредством срабатывания шага Y.

Последовательность срабатываний — это конечная или бесконечная последовательность маркировок и шагов вида:

M1[Y1>M2[Y2>M3...Mn[Yn>Mn+1...

такая, что Mi[Yi>Mi+1 для всех iN+. Здесь M1 называется началом и Mn+1 — концом (в случае конечной последовательности срабатываний) заданной последовательности срабатываний.

Маркировка M достижима из маркировки M', если существует конечная последовательность срабатываний, имеющая началом M' и концом M, т.е. для некоторого nN+ существует последовательность шагов Y1,Y2,...Yn такая, что

M'[Y1>M˜...M&hat;[Yn>M.