Формальное определение CPN

Раскрашенная сеть Петри CPN- это кортеж

CPN = {Θ, Σ, P, T, A, N, C, G, E, I}. (2.13)

Рассмотрим элементы определения (2.13).

1. Θ = {θ = 0, 1, 2, …} – множество дискретных моментов времени (шагов), в которые происходит функционирование сети. Номер шага есть переменная целого типа:

var teta: Integer;

2. Σ – конечное множество непустых типов, называемое цветами. Типы имеют общее название color и задаются аналогично тому, как это принято в языках программирования.

Например:

type colorI = Integer; - целый тип;

type colorP = product U * I; - прямое произведение типов.

При описании переменных, используемых в сети, указывают их принадлежность к типу, например:

Var x: colorU; vari: colorI; varj: colorP.

В последнем примере переменная j состоит из пары элементов j=(jU, jI), где элемент jU принадлежит типу colorU, а jI – типу color I.

3. P – конечное множество позиций. Это множество может быть представлено перечисляемым типом:

Type P=(p1, p2, …, pn);

а для работы с ним вводится переменная

var p: P.

С каждой позицией может быть связана определенная маркировка, которая учитывает наличие различных типов ресурсов. Маркировка позиции p Є P представляет собой мультимножество, например, следующего вида:

m (p)=(1`x, 2`, 1`j).

Здесь х, i, j - переменные указанных в п. 2 цветовых типов, определяющие различные виды ресурсов, а цифры, стоящие перед кавычками – количество фишек соотвествующего типа в позиции р Є Р.

Совокупность маркировок всех позиций называется маркировкой сети.

М = {т(р,), т(р₂),.. .т(р_п)}.

В языке Паскаль мультимножество, определяющее маркировку позиции, может быть представлено, напримертипом - множество, состоящим из записей вида

type m — record

i: Integer; x: colorU end;

Операции над мультимножествами можно определить соответствующими процедурами. Аналогично определяется мультимножество, задающее маркировку сети.

4. Т - конечное множество переходов, которое представить перечисляемым типом

type T - (tl, t2,..., tm);

и соответствующей переменной:

var t: T.

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

5. А - конечное множество дуг, связывающих между собой позиции и переходы. В отличие от обыкновенных сетей Петри, где дуги задаются матрицами инцидентности F ^р и F^t, а на языкеCPN ML указываются все дуги с помощью выражения вида р to t и t to p. где рЄ Р, t Є T. Такая нотация введена для того, чтобы можно было пару элементов pi, tj соединить несколькими дугами с различными свойствами.

В этих выражениях первый элемент указывает начало дуги, второй – конец дуги.

Множество А имеет следующую структуру:

А = {a₁, a₂, …a_p},

где дуги а_k Є А определяются одним из видов выражений

a_k = p_i to t_j или a_k = t_j to p_i, p_i Є P, t_j Є T,

Поскольку дуги имеют два вида: от позиции к переходу (p to t) и от перехода к позиции (t to p), то множество А можно представить в виде суммы непересекающихся множеств:

A = A^p A^t, A^p A^t = Ø,

Где множество A^p содержит элементы вида p to t, а множество At – элементы вида t to p.

Как и в случае обыкновенных сетей Петри, элементы множеств P, T, A не пересекаются:

P T = P A = T A = Ø.

6. N(a) – узловая функция, которая для каждой дуги a Є A указывает ее исходный и конечный узел. Формально соответствует выражение s to d. Здесь s – имя узла, от которого начинается дуга, d – имя узла, где она заканчивается. Рассмотрим один из способов задания этой функции. Каждая дуга может быть представлена в виде записи. Дуга типа p_i to t_j задаются записью

Type AP= record (2.14)

p: P; t: T end;

Дуги типа t_j to p_i задаются аналогично:

Type AT=record (2.15)

t: T p: P; end;

Множества дуг A^p и A^t могут быть представлены перечисляемыми типами:

Type AP=(ap1, ap2, …, apk); (2.16)

Type AT=(at1, at2, …, atk);

Для работы с дугами вводится переменные соответствующих типов:

Var ap: AP; var at: AT;

7. C(p) – цветовая функция, определяющая множество типовцветов, разрещенных для каждой позиции. Например, запись

colorU if p Î {p₁, p₂, p₄},

C(p) =

colorI otherwise

означает, что цвета типа U разрешены для позиций p₁, p₂, p₄, а цвета типа I разрешены для всех остальных позиций из Р.

8. G(t) - блокировочная (спусковая) функция, описывающая дополнительные условия, которые должны быть выполнены для срабатывания перехода t Є T. Эта функция представляет собой предикат, составленный из переменных принадлежащих типов цветов Σ. Например, функции

x = q if t = t₁,

G(t)=

true otherwise

Принимает истинное значение для перехода t_i, если переменная x = q, а во всех остальных случаях она ложь. Таким образом, для того, чтобы было разрешено срабатывание перехода t_i, требуется выполнение дополнительного условия x = q на входной дуге к t_i. Если эта функция не определена, то по умолчания предполагается истинной.

9. Е(а) – функция, задающая выражения на дугах a Є А.Эта функция для каждой дуги a определяет мультимножество, состоящее из элементов, описанных в множестве цветов Σ. Мы будем говорить, что это мультимножество помечает дугу. Введение в CPN функции Е(а) является развитием понятия кратности дуг в формализме обыкновенных СП.

Рассмотрим примеры задания функции Е(а).

Е(а₁) = 2’е

- дуга а_} помечается двумя фишками типа е;

Е(а₂) = case x of p => 2’e | q => 1’e

- дуга а₂ помечается двумя фишками типа e, если переменная x=pи одной фишкой типа e, если x=q.

Е(а₃) = if x=p then 1’e else empty

- дуга а₃ помечается одной фишкой типа e, если x=p, иначе не помечается.

Е(а₄) = if x=q hten 1’(q? i + 1) else empty

- дуга а₄ помечается одной фишкой типа Р (см. пример в п.2), если х=q и не помечается в противном случае.

Отсутствие выражения для какой-либо дуги означает, что дуга не помечена.

9. I(p) – функция инициализации сети CPN. Эта функция по аналогии с обыкновенными СП задает начальную маркировку (разметку) сети М₀, т.е. для каждой позиции р Є Р указывает цветовое мультимножество, обозначаемое m₀(p).

Например, m₀(p₁) = 3’e; m₀(p₂)=2’(p, 0); m₀(p₃)=Ø – начальные маркировки позиций;

М₀ ={3’e; 2’(p, 0); Ø } – начальная маркировка сети.