Volume 14, 2002

University of Bialystok

Copyright (c) 2002 Association of Mizar Users

### The abstract of the Mizar article:

### Processes in Petri nets

**by****Grzegorz Bancerek,****Mitsuru Aoki,****Akio Matsumoto, and****Yasunari Shidama**- Received December 20, 2002
- 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;

Back to top