Journal of Formalized Mathematics
Volume 14, 2002
University of Bialystok
Copyright (c) 2002 Association of Mizar Users

Processes in Petri nets

by
Grzegorz Bancerek,
Mitsuru Aoki,
Akio Matsumoto, and
Yasunari Shidama

MML identifier: PNPROC_1
[ Mizar article, MML identifier index ]

```environ

vocabulary PNPROC_1, TARSKI, RELAT_1, FUNCT_1, BOOLE, MCART_1, ARYTM_1, NET_1,
FINSEQ_1, FUNCT_2, FUNCT_7, FUNCOP_1, PRALG_1, FINSEQ_4, CARD_1,
FINSET_1, PETRI, RELOC, INT_1;
notation TARSKI, XBOOLE_0, DOMAIN_1, RELAT_1, FUNCT_1, SUBSET_1, FINSET_1,
CARD_1, FINSEQ_1, FUNCT_2, FUNCOP_1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1,
BINARITH, MCART_1, FINSEQ_2, FINSEQ_4, LANG1, PRALG_1, FUNCT_7, INT_1,
GRAPH_2;
constructors WELLORD2, DOMAIN_1, INT_1, FINSEQ_4, FUNCT_7, BINARITH, GRAPH_2,
MEMBERED;
clusters RELAT_1, RELSET_1, FUNCT_1, FUNCT_7, FUNCOP_1, SUBSET_1, FINSEQ_1,
HEYTING2, PRELAMB, INT_1, MEMBERED, NUMBERS, ORDINAL2;
requirements BOOLE, SUBSET, REAL, NUMERALS, ARITHM;

begin :: Preliminaries

reserve i,j,k,l for Nat,
x,x1,x2,y1,y2 for set;

theorem :: PNPROC_1:1
i > 0 implies {[i,x]} is FinSubsequence;

theorem :: PNPROC_1:2
for q being FinSubsequence holds q = {} iff Seq q = {};

theorem :: PNPROC_1:3
for q being FinSubsequence st q = {[i,x]} holds Seq q = <*x*>;

definition
cluster -> finite FinSubsequence;
end;

theorem :: PNPROC_1:4
for q being FinSubsequence st Seq q = <*x*>
ex i st q = {[i,x]};

theorem :: PNPROC_1:5
{[x1,y1], [x2,y2]} is FinSequence implies
x1 = 1 & x2 = 1 & y1 = y2 or
x1 = 1 & x2 = 2 or
x1 = 2 & x2 = 1;

theorem :: PNPROC_1:6
<*x1,x2*> = {[1,x1], [2,x2]};

theorem :: PNPROC_1:7
for p being FinSubsequence holds Card p = len Seq p;

theorem :: PNPROC_1:8
for P,R being Relation st dom P misses dom R holds P misses R;

theorem :: PNPROC_1:9
for X,Y being set, P,R being Relation st X misses Y holds P|X misses R|Y;

theorem :: PNPROC_1:10
for f,g,h being Function st
f c= h & g c= h & f misses g holds dom f misses dom g;

theorem :: PNPROC_1:11
for Y being set, R being Relation holds Y|R c= R|(R"Y);

theorem :: PNPROC_1:12
for Y being set, f being Function holds Y|f = f|(f"Y);

begin :: Markings on Petri nets

definition let P be set;
mode marking of P -> Function means
:: PNPROC_1:def 1
dom it = P & rng it c= NAT;
end;

reserve P,p,x,y,x1,x2,y1,y2 for set,
m1,m2,m3,m4,m for marking of P,
i,j,j1,j2,k,k1,k2,l,l1,l2 for Nat;

definition
let P be set;
let m be marking of P;
let p be set;
redefine func m.p -> Nat;
synonym m multitude_of p;
end;

scheme MarkingLambda { P() -> set, F(set) -> Nat }:
ex m being marking of P() st
for p st p in P() holds m multitude_of p = F(p);

definition let P,m1,m2;
redefine pred m1 = m2 means
:: PNPROC_1:def 2
for p st p in P holds m1 multitude_of p = m2 multitude_of p;
end;

definition let P;
func {\$} P -> marking of P equals
:: PNPROC_1:def 3
P --> 0;
end;

definition
let P be set;
let m1, m2 be marking of P;
pred m1 c= m2 means
:: PNPROC_1:def 4
for p being set st p in P holds
m1 multitude_of p <= m2 multitude_of p;
reflexivity;
end;

theorem :: PNPROC_1:13
{\$}P c= m;

theorem :: PNPROC_1:14
m1 c= m2 & m2 c= m3 implies m1 c= m3;

definition
let P be set;
let m1, m2 be marking of P;
func m1 + m2 -> marking of P means
:: PNPROC_1:def 5
for p being set st p in P holds
it multitude_of p = (m1 multitude_of p)+(m2 multitude_of p);
commutativity;
end;

theorem :: PNPROC_1:15
m + {\$}P = m;

definition
let P be set;
let m1, m2 be marking of P such that
m2 c= m1;
func m1 - m2 -> marking of P means
:: PNPROC_1:def 6
for p being set st p in P holds
it multitude_of p = (m1 multitude_of p)-(m2 multitude_of p);
end;

theorem :: PNPROC_1:16
m1 c= m1 + m2;

theorem :: PNPROC_1:17
m - {\$}P = m;

theorem :: PNPROC_1:18
m1 c= m2 & m2 c= m3 implies m3 - m2 c= m3 - m1;

theorem :: PNPROC_1:19
(m1 + m2) - m2 = m1;

theorem :: PNPROC_1:20
m c= m1 & m1 c= m2 implies m1 - m c= m2 - m;

theorem :: PNPROC_1:21
m1 c= m2 implies m2 + m3 -m1 = m2 - m1 + m3;

theorem :: PNPROC_1:22
m1 c= m2 & m2 c= m1 implies m1 = m2;

theorem :: PNPROC_1:23
(m1 + m2) + m3 = m1 + (m2 + m3);

theorem :: PNPROC_1:24
m1 c= m2 & m3 c= m4 implies m1 + m3 c= m2 + m4;

theorem :: PNPROC_1:25
m1 c= m2 implies m2 - m1 c= m2;

theorem :: PNPROC_1:26
m1 c= m2 & m3 c= m4 & m4 c= m1 implies m1 - m4 c= m2 - m3;

::  a1 c= a2 & a2 c= a3 implies a3 - a2 c= a3 - a1 by T6';
::  a c= a1 & a1 c= a2 implies a1 - a c= a2 -a by T6';

theorem :: PNPROC_1:27
m1 c= m2 implies m2 = (m2 - m1) + m1;

theorem :: PNPROC_1:28
(m1 + m2) - m1 = m2;

theorem :: PNPROC_1:29
m2 + m3 c= m1 implies (m1 - m2) - m3 = m1 - (m2 + m3);

theorem :: PNPROC_1:30
m3 c= m2 & m2 c= m1 implies m1 - (m2 - m3) = (m1 - m2) + m3;

theorem :: PNPROC_1:31
m in Funcs(P, NAT);

theorem :: PNPROC_1:32
x in Funcs(P, NAT) implies x is marking of P;

begin :: Transitions and firing

definition let P;
mode transition of P means
:: PNPROC_1:def 7
ex m1,m2 st it=[m1,m2];
end;

reserve t,t1,t2 for transition of P;

definition
let P,t;
redefine func t`1 -> marking of P;
synonym Pre t;
func t`2 -> marking of P;
synonym Post t;
end;

definition
let P, m, t;
func fire(t,m) -> marking of P equals
:: PNPROC_1:def 8
(m - Pre t) + Post t if Pre t c= m
otherwise m;
end;

theorem :: PNPROC_1:33
(Pre t1) + (Pre t2) c= m implies
fire(t2, fire(t1,m)) = (m - (Pre t1) - Pre t2) + (Post t1) + (Post t2);

definition
let P, t;
func fire t -> Function means
:: PNPROC_1:def 9
dom it = Funcs(P, NAT) &
for m being marking of P holds it.m = fire(t,m);
end;

theorem :: PNPROC_1:34
rng fire t c= Funcs(P, NAT);

theorem :: PNPROC_1:35
fire(t2, fire(t1,m)) = ((fire t2)*(fire t1)).m;

definition
let P;
mode Petri_net of P -> non empty set means
:: PNPROC_1:def 10
for x being set st x in it holds x is transition of P;
end;

reserve N for Petri_net of P;

definition let P, N;
redefine mode Element of N -> transition of P;
end;

reserve e, e1,e2 for Element of N;

begin :: Firing sequences of transitions

definition let P, N;
mode firing-sequence of N is Element of N*;
end;

reserve C,C1,C2,C3,fs,fs1,fs2 for firing-sequence of N;

definition
let P, N, C;
func fire C -> Function means
:: PNPROC_1:def 11
ex F being Function-yielding FinSequence st
it = compose(F, Funcs(P, NAT)) &
len F = len C &
for i being Nat st i in dom C holds F.i = fire (C /. i qua Element of N);
end;

:: Firing of empty firing-sequence <*>N
theorem :: PNPROC_1:36
fire(<*>N) = id Funcs(P, NAT);

:: Firing of firing-sequence with one translation <*e*>
theorem :: PNPROC_1:37
fire <*e*> = fire e;

theorem :: PNPROC_1:38
(fire e)*id Funcs(P, NAT) = fire e;

:: Firing of firing-sequence with two translations <*e1,e2*>
theorem :: PNPROC_1:39
fire <*e1,e2*> = (fire e2)*(fire e1);

theorem :: PNPROC_1:40
dom fire C = Funcs(P, NAT) & rng fire C c= Funcs(P, NAT);

:: Firing of compound firing-sequence
theorem :: PNPROC_1:41
fire (C1^C2) = (fire C2)*(fire C1);

theorem :: PNPROC_1:42
fire (C^<*e*>) = (fire e)*(fire C);

definition
let P, N, C, m;
func fire(C, m) -> marking of P equals
:: PNPROC_1:def 12
(fire C).m;
end;

begin :: Sequential composition

definition let P, N;
mode process of N is Subset of N*;
end;

reserve R, R1, R2, R3, P1, P2 for process of N;

definition
cluster FinSequence-like -> FinSubsequence-like Function;
end;

definition
let P, N, R1, R2;
func R1 before R2 -> process of N equals
:: PNPROC_1:def 13
{C1^C2: C1 in R1 & C2 in R2};
end;

definition
let P, N;
let R1, R2 be non empty process of N;
cluster R1 before R2 -> non empty;
end;

theorem :: PNPROC_1:43
(R1 \/ R2) before R = (R1 before R) \/ (R2 before R);

theorem :: PNPROC_1:44
R before (R1 \/ R2) = (R before R1) \/ (R before R2);

theorem :: PNPROC_1:45
{C1} before {C2} = {C1^C2};

theorem :: PNPROC_1:46
{C1,C2} before {C} = {C1^C, C2^C};

theorem :: PNPROC_1:47
{C} before {C1,C2} = {C^C1, C^C2};

begin :: Concurrent composition

definition
let P, N, R1, R2;
func R1 concur R2 -> process of N equals
:: PNPROC_1:def 14
{C: ex q1,q2 being FinSubsequence st C = q1 \/ q2 & q1 misses q2 &
Seq q1 in R1 & Seq q2 in R2};
commutativity;
end;

theorem :: PNPROC_1:48
(R1 \/ R2) concur R = (R1 concur R) \/ (R2 concur R);

theorem :: PNPROC_1:49
{<*e1*>} concur {<*e2*>} = {<*e1,e2*>, <*e2,e1*>};

theorem :: PNPROC_1:50
{<*e1*>,<*e2*>} concur {<*e*>} = {<*e1,e*>, <*e2,e*>, <*e,e1*>, <*e,e2*>};

theorem :: PNPROC_1:51
(R1 before R2) before R3 = R1 before (R2 before R3);

definition
let p be FinSubsequence;
let i be Nat;
func i Shift p -> FinSubsequence means
:: PNPROC_1:def 15

dom it = {i+k where k is Nat: k in dom p} &
for j being Nat st j in dom p holds it.(i+j) = p.j;
end;

reserve q,q1,q2,q3,q4 for FinSubsequence;

theorem :: PNPROC_1:52
0 Shift q = q;

theorem :: PNPROC_1:53
(i+j) Shift q = i Shift (j Shift q);

theorem :: PNPROC_1:54
for p being FinSequence st p <> {} holds
dom (i Shift p) = {j1: i+1 <= j1 & j1 <= i+(len p)};

theorem :: PNPROC_1:55
for q being FinSubsequence holds q = {} iff i Shift q = {};

theorem :: PNPROC_1:56
for q being FinSubsequence ex ss being FinSubsequence st
dom ss = dom q & rng ss = dom (i Shift q) &
(for k st k in dom q holds ss.k = i+k) & ss is one-to-one;

theorem :: PNPROC_1:57
for q being FinSubsequence holds Card q = Card (i Shift q);

theorem :: PNPROC_1:58
for p being FinSequence holds dom p = dom Seq (i Shift p);

theorem :: PNPROC_1:59
for p being FinSequence st k in dom p holds (Sgm dom (i Shift p)).k = i + k;

theorem :: PNPROC_1:60
for p being FinSequence st k in dom p holds (Seq (i Shift p)).k = p.k;

theorem :: PNPROC_1:61
for p being FinSequence holds Seq (i Shift p) = p;

reserve p1,p2 for FinSequence;

theorem :: PNPROC_1:62
dom (p1 \/ ((len p1) Shift p2)) = Seg (len p1 + len p2);

theorem :: PNPROC_1:63
for p1 being FinSequence, p2 being FinSubsequence st len p1 <= i holds
dom p1 misses dom (i Shift p2);

theorem :: PNPROC_1:64
for p1,p2 being FinSequence holds p1^p2 = p1 \/ ((len p1) Shift p2);

theorem :: PNPROC_1:65
for p1 being FinSequence, p2 being FinSubsequence st i >= len p1
holds p1 misses i Shift p2;

theorem :: PNPROC_1:66
(R1 concur R2) concur R3 = R1 concur (R2 concur R3);

theorem :: PNPROC_1:67
R1 before R2 c= R1 concur R2;

theorem :: PNPROC_1:68
R1 c= P1 & R2 c= P2 implies R1 before R2 c= P1 before P2;

theorem :: PNPROC_1:69
R1 c= P1 & R2 c= P2 implies R1 concur R2 c= P1 concur P2;

theorem :: PNPROC_1:70
for p,q being FinSubsequence st q c= p holds
i Shift q c= i Shift p;

theorem :: PNPROC_1:71
for p1,p2 being FinSequence holds len p1 Shift p2 c= p1^p2;

theorem :: PNPROC_1:72
dom q1 misses dom q2 implies dom (i Shift q1) misses dom (i Shift q2);

theorem :: PNPROC_1:73
for q,q1,q2 being FinSubsequence st q = q1 \/ q2 & q1 misses q2 holds
(i Shift q1) \/ (i Shift q2) = i Shift q;

theorem :: PNPROC_1:74
for q being FinSubsequence holds dom Seq q = dom Seq (i Shift q);

theorem :: PNPROC_1:75
for q being FinSubsequence st k in dom Seq q
ex j st j = (Sgm dom q).k & (Sgm dom (i Shift q)).k = i + j;

theorem :: PNPROC_1:76
for q being FinSubsequence st
k in dom Seq q holds (Seq (i Shift q)).k = (Seq q).k;

theorem :: PNPROC_1:77
for q being FinSubsequence holds Seq q = Seq (i Shift q);

theorem :: PNPROC_1:78
for q being FinSubsequence st
dom q c= Seg k holds dom (i Shift q) c= Seg (i+k);

theorem :: PNPROC_1:79
for p being FinSequence, q1,q2 being FinSubsequence st q1 c= p
ex ss being FinSubsequence st ss = q1 \/ (len p Shift q2);

theorem :: PNPROC_1:80
for p1,p2 being FinSequence, q1,q2 being FinSubsequence st q1 c= p1 & q2 c= p2
ex ss being FinSubsequence st ss = q1 \/ (len p1 Shift q2) &
dom Seq ss = Seg (len Seq q1 + len Seq q2);

theorem :: PNPROC_1:81
for p1,p2 being FinSequence, q1,q2 being FinSubsequence st q1 c= p1 & q2 c= p2
ex ss being FinSubsequence st ss = q1 \/ (len p1 Shift q2) &
dom Seq ss = Seg (len Seq q1 + len Seq q2) &
Seq ss = Seq q1 \/ (len Seq q1 Shift Seq q2);

theorem :: PNPROC_1:82
for p1,p2 being FinSequence, q1,q2 being FinSubsequence st q1 c= p1 & q2 c= p2
ex ss being FinSubsequence st
ss = q1 \/ (len p1 Shift q2) & (Seq q1)^(Seq q2) = Seq ss;

theorem :: PNPROC_1:83
(R1 concur R2) before (P1 concur P2) c= (R1 before P1) concur (R2 before P2
);

definition
let P, N;
let R1, R2 be non empty process of N;
cluster R1 concur R2 -> non empty;
end;

begin  :: Neutral process

definition let P;
let N be Petri_net of P;
func NeutralProcess(N) -> non empty process of N equals
:: PNPROC_1:def 16
{<*>N};
end;

definition
let P;
let N be Petri_net of P;
let t be Element of N;
func ElementaryProcess(t) -> non empty process of N equals
:: PNPROC_1:def 17
{<*t*>};
end;

theorem :: PNPROC_1:84
NeutralProcess(N) before R = R;

theorem :: PNPROC_1:85
R before NeutralProcess(N) = R;

theorem :: PNPROC_1:86
NeutralProcess(N) concur R = R;
```