:: Processes in {P}etri nets :: by Grzegorz Bancerek , Mitsuru Aoki , Akio Matsumoto and Yasunari Shidama :: :: Received December 20, 2002 :: Copyright (c) 2002-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, XXREAL_0, CARD_1, FINSEQ_1, RELAT_1, TARSKI, XBOOLE_0, NAT_1, ARYTM_3, FUNCT_1, FUNCOP_1, ARYTM_1, PETRI, NET_1, MCART_1, FUNCT_2, FUNCT_7, PARTFUN1, ORDINAL4, VALUED_1, PNPROC_1; notations TARSKI, XBOOLE_0, DOMAIN_1, XTUPLE_0, RELAT_1, FUNCT_1, SUBSET_1, PARTFUN1, CARD_1, FINSEQ_1, FUNCT_2, FUNCOP_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, NAT_D, MCART_1, FINSEQ_2, FUNCT_7, INT_1, XXREAL_0, PRE_POLY, VALUED_1; constructors WELLORD2, DOMAIN_1, REAL_1, FUNCT_7, NAT_D, RELSET_1, PRE_POLY, XTUPLE_0, FINSEQ_6; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, FINSEQ_1, FUNCT_7, FINSEQ_6, VALUED_0, VALUED_1, FUNCT_2, MEMBERED, CARD_1, NAT_1, XTUPLE_0; requirements BOOLE, SUBSET, REAL, NUMERALS, ARITHM; begin :: Markings on Petri nets reserve i,j,k,l for Nat, x,x1,x2,y1,y2 for set; definition let P be set; mode marking of P is Function of P,NAT; end; reserve P,p,x,y,x1,x2 for set, m1,m2,m3,m4,m for marking of P, i,j,j1,j2,k,k1,k2,l,l1 for Nat; notation let P be set; let m be marking of P; let p be object; synonym m multitude_of p for m.p; end; scheme :: PNPROC_1:sch 1 MarkingLambda { P() -> set, F(object) -> Element of NAT }: ex m being Function of P(),NAT st for p st p in P() holds m.p = F(p); definition let P,m1,m2; redefine pred m1 = m2 means :: PNPROC_1:def 1 for p being object 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 2 P --> 0; end; definition let P be set; let m1, m2 be marking of P; pred m1 c= m2 means :: PNPROC_1:def 3 for p being set st p in P holds m1 multitude_of p <= m2 multitude_of p; reflexivity; end; theorem :: PNPROC_1:1 {$}P c= m; theorem :: PNPROC_1:2 m1 c= m2 & m2 c= m3 implies m1 c= m3; definition let P be set; let m1, m2 be marking of P; redefine func m1 + m2 -> marking of P means :: PNPROC_1:def 4 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:3 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 5 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:4 m1 c= m1 + m2; theorem :: PNPROC_1:5 m - {$}P = m; theorem :: PNPROC_1:6 m1 c= m2 & m2 c= m3 implies m3 - m2 c= m3 - m1; theorem :: PNPROC_1:7 (m1 + m2) - m2 = m1; theorem :: PNPROC_1:8 m c= m1 & m1 c= m2 implies m1 - m c= m2 - m; theorem :: PNPROC_1:9 m1 c= m2 implies m2 + m3 -m1 = m2 - m1 + m3; theorem :: PNPROC_1:10 m1 c= m2 & m2 c= m1 implies m1 = m2; theorem :: PNPROC_1:11 (m1 + m2) + m3 = m1 + (m2 + m3); theorem :: PNPROC_1:12 m1 c= m2 & m3 c= m4 implies m1 + m3 c= m2 + m4; theorem :: PNPROC_1:13 m1 c= m2 implies m2 - m1 c= m2; theorem :: PNPROC_1:14 m1 c= m2 & m3 c= m4 & m4 c= m1 implies m1 - m4 c= m2 - m3; theorem :: PNPROC_1:15 m1 c= m2 implies m2 = (m2 - m1) + m1; theorem :: PNPROC_1:16 (m1 + m2) - m1 = m2; theorem :: PNPROC_1:17 m2 + m3 c= m1 implies (m1 - m2) - m3 = m1 - (m2 + m3); theorem :: PNPROC_1:18 m3 c= m2 & m2 c= m1 implies m1 - (m2 - m3) = (m1 - m2) + m3; begin :: Transitions and firing definition let P; mode transition of P -> set means :: PNPROC_1:def 6 ex m1,m2 st it=[m1,m2]; end; reserve t,t1,t2 for transition of P; notation let P,t; synonym Pre t for t`1; synonym Post t for t`2; end; definition let P,t; redefine func Pre t -> marking of P; redefine func Post t -> marking of P; end; definition let P, m, t; func fire(t,m) -> marking of P equals :: PNPROC_1:def 7 (m - Pre t) + Post t if Pre t c= m otherwise m; end; theorem :: PNPROC_1:19 (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 8 dom it = Funcs(P, NAT) & for m being marking of P holds it.m = fire(t,m); end; theorem :: PNPROC_1:20 rng fire t c= Funcs(P, NAT); theorem :: PNPROC_1:21 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 9 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 10 ex F being Function-yielding FinSequence st it = compose(F, Funcs(P, NAT)) & len F = len C & for i being Element of 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:22 fire(<*>N) = id Funcs(P, NAT); :: Firing of firing-sequence with one translation <*e*> theorem :: PNPROC_1:23 fire <*e*> = fire e; theorem :: PNPROC_1:24 (fire e)*id Funcs(P, NAT) = fire e; :: Firing of firing-sequence with two translations <*e1,e2*> theorem :: PNPROC_1:25 fire <*e1,e2*> = (fire e2)*(fire e1); theorem :: PNPROC_1:26 dom fire C = Funcs(P, NAT) & rng fire C c= Funcs(P, NAT); :: Firing of compound firing-sequence theorem :: PNPROC_1:27 fire (C1^C2) = (fire C2)*(fire C1); theorem :: PNPROC_1:28 fire (C^<*e*>) = (fire e)*(fire C); definition let P, N, C, m; func fire(C, m) -> marking of P equals :: PNPROC_1:def 11 (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 let P, N, R1, R2; func R1 before R2 -> process of N equals :: PNPROC_1:def 12 {C1^C2: C1 in R1 & C2 in R2}; end; registration let P, N; let R1, R2 be non empty process of N; cluster R1 before R2 -> non empty; end; theorem :: PNPROC_1:29 (R1 \/ R2) before R = (R1 before R) \/ (R2 before R); theorem :: PNPROC_1:30 R before (R1 \/ R2) = (R before R1) \/ (R before R2); theorem :: PNPROC_1:31 {C1} before {C2} = {C1^C2}; theorem :: PNPROC_1:32 {C1,C2} before {C} = {C1^C, C2^C}; theorem :: PNPROC_1:33 {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 13 {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:34 (R1 \/ R2) concur R = (R1 concur R) \/ (R2 concur R); theorem :: PNPROC_1:35 {<*e1*>} concur {<*e2*>} = {<*e1,e2*>, <*e2,e1*>}; theorem :: PNPROC_1:36 {<*e1*>,<*e2*>} concur {<*e*>} = {<*e1,e*>, <*e2,e*>, <*e,e1*>, <*e,e2*>}; theorem :: PNPROC_1:37 (R1 before R2) before R3 = R1 before (R2 before R3); notation let p be FinSubsequence; let i be Element of NAT; synonym i Shift p for Shift(p,i); end; reserve q,q1,q2,q3,q4 for FinSubsequence, p1,p2 for FinSequence; theorem :: PNPROC_1:38 (R1 concur R2) concur R3 = R1 concur (R2 concur R3); theorem :: PNPROC_1:39 R1 before R2 c= R1 concur R2; theorem :: PNPROC_1:40 R1 c= P1 & R2 c= P2 implies R1 before R2 c= P1 before P2; theorem :: PNPROC_1:41 R1 c= P1 & R2 c= P2 implies R1 concur R2 c= P1 concur P2; theorem :: PNPROC_1:42 (R1 concur R2) before (P1 concur P2) c= (R1 before P1) concur (R2 before P2); registration 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 14 {<*>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 15 {<*t*>}; end; theorem :: PNPROC_1:43 NeutralProcess(N) before R = R; theorem :: PNPROC_1:44 R before NeutralProcess(N) = R; theorem :: PNPROC_1:45 NeutralProcess(N) concur R = R;