:: 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;