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

definition

let P be set ;
mode marking of P is Function of P,NAT;

end;

notation

let P be set ;
let m be marking of P;
let p be object ;
synonym m multitude_of p for P . m;

end;

scheme :: PNPROC_1:sch 1
MarkingLambda{ F₁() -> set , F₂( object ) -> Element of NAT } :

ex m being Function of F₁(),NAT st
for p being set st p in F₁() holds
m . p = F₂(p)

proof end;

definition

let P be set ;
let m1, m2 be marking of P;

:: original: =
redefine pred m1 = m2 means :: PNPROC_1:def 1
for p being object st p in P holds
p multitude_of = p multitude_of ;

compatibility
( m1 = m2 iff for p being object st p in P holds
p multitude_of = p multitude_of )

proof end;

end;

:: deftheorem defines = PNPROC_1:def 1 :
for P being set
for m1, m2 being marking of P holds
( m1 = m2 iff for p being object st p in P holds
p multitude_of = p multitude_of );

definition

let P be set ;

func {$} P -> marking of P equals :: PNPROC_1:def 2
P --> 0;

coherence
P --> 0 is marking of P ;

end;

:: deftheorem defines {$} PNPROC_1:def 2 :
for P being set holds {$} P = P --> 0;

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
p multitude_of <= p multitude_of ;

reflexivity
for m1 being marking of P
for p being set st p in P holds
p multitude_of <= p multitude_of ;

end;

:: deftheorem defines c= PNPROC_1:def 3 :
for P being set
for m1, m2 being marking of P holds
( m1 c= m2 iff for p being set st p in P holds
p multitude_of <= p multitude_of );

Lm1: for P, p being set st p in P holds
({$} P) . p = 0
by FUNCOP_1:7;

theorem Th1: :: PNPROC_1:1

for P being set
for m being marking of P holds {$} P c= m by Lm1;

theorem Th2: :: PNPROC_1:2

for P being set
for m1, m2, m3 being marking of P st m1 c= m2 & m2 c= m3 holds
m1 c= m3

proof end;

definition

let P be set ;
let m1, m2 be marking of P;

:: original: +
redefine func m1 + m2 -> marking of P means :Def4: :: PNPROC_1:def 4
for p being set st p in P holds
p multitude_of = (p multitude_of ) + (p multitude_of );

coherence
m1 + m2 is marking of P

proof end;

compatibility
for b₁ being marking of P holds
( b₁ = m1 + m2 iff for p being set st p in P holds
p multitude_of = (p multitude_of ) + (p multitude_of ) )

proof end;

end;

:: deftheorem Def4 defines + PNPROC_1:def 4 :
for P being set
for m1, m2, b₄ being marking of P holds
( b₄ = m1 + m2 iff for p being set st p in P holds
p multitude_of = (p multitude_of ) + (p multitude_of ) );

theorem :: PNPROC_1:3

for P being set
for m being marking of P holds m + ({$} P) = m

proof end;

definition

let P be set ;
let m1, m2 be marking of P;
assume A1: m2 c= m1 ;

func m1 - m2 -> marking of P means :Def5: :: PNPROC_1:def 5
for p being set st p in P holds
p multitude_of = (p multitude_of ) - (p multitude_of );

existence
ex b₁ being marking of P st
for p being set st p in P holds
p multitude_of = (p multitude_of ) - (p multitude_of )

proof end;

uniqueness
for b₁, b₂ being marking of P st ( for p being set st p in P holds
p multitude_of = (p multitude_of ) - (p multitude_of ) ) & ( for p being set st p in P holds
p multitude_of = (p multitude_of ) - (p multitude_of ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines - PNPROC_1:def 5 :
for P being set
for m1, m2 being marking of P st m2 c= m1 holds
for b₄ being marking of P holds
( b₄ = m1 - m2 iff for p being set st p in P holds
p multitude_of = (p multitude_of ) - (p multitude_of ) );

theorem Th4: :: PNPROC_1:4

for P being set
for m1, m2 being marking of P holds m1 c= m1 + m2

proof end;

theorem :: PNPROC_1:5

for P being set
for m being marking of P holds m - ({$} P) = m

proof end;

theorem :: PNPROC_1:6

for P being set
for m1, m2, m3 being marking of P st m1 c= m2 & m2 c= m3 holds
m3 - m2 c= m3 - m1

proof end;

theorem Th7: :: PNPROC_1:7

for P being set
for m1, m2 being marking of P holds (m1 + m2) - m2 = m1

proof end;

theorem Th8: :: PNPROC_1:8

for P being set
for m1, m2, m being marking of P st m c= m1 & m1 c= m2 holds
m1 - m c= m2 - m

proof end;

theorem Th9: :: PNPROC_1:9

for P being set
for m1, m2, m3 being marking of P st m1 c= m2 holds
(m2 + m3) - m1 = (m2 - m1) + m3

proof end;

theorem :: PNPROC_1:10

for P being set
for m1, m2 being marking of P st m1 c= m2 & m2 c= m1 holds
m1 = m2

proof end;

theorem Th11: :: PNPROC_1:11

for P being set
for m1, m2, m3 being marking of P holds (m1 + m2) + m3 = m1 + (m2 + m3)

proof end;

theorem :: PNPROC_1:12

for P being set
for m1, m2, m3, m4 being marking of P st m1 c= m2 & m3 c= m4 holds
m1 + m3 c= m2 + m4

proof end;

theorem :: PNPROC_1:13

for P being set
for m1, m2 being marking of P st m1 c= m2 holds
m2 - m1 c= m2

proof end;

theorem Th14: :: PNPROC_1:14

for P being set
for m1, m2, m3, m4 being marking of P st m1 c= m2 & m3 c= m4 & m4 c= m1 holds
m1 - m4 c= m2 - m3

proof end;

theorem Th15: :: PNPROC_1:15

for P being set
for m1, m2 being marking of P st m1 c= m2 holds
m2 = (m2 - m1) + m1

proof end;

theorem Th16: :: PNPROC_1:16

for P being set
for m1, m2 being marking of P holds (m1 + m2) - m1 = m2

proof end;

theorem Th17: :: PNPROC_1:17

for P being set
for m1, m2, m3 being marking of P st m2 + m3 c= m1 holds
(m1 - m2) - m3 = m1 - (m2 + m3)

proof end;

theorem :: PNPROC_1:18

for P being set
for m1, m2, m3 being marking of P st m3 c= m2 & m2 c= m1 holds
m1 - (m2 - m3) = (m1 - m2) + m3

proof end;

definition

let P be set ;

mode transition of P -> set means :Def6: :: PNPROC_1:def 6
ex m1, m2 being marking of P st it = [m1,m2];

existence
ex b₁ being set ex m1, m2 being marking of P st b₁ = [m1,m2]

proof end;

end;

:: deftheorem Def6 defines transition PNPROC_1:def 6 :
for P, b₂ being set holds
( b₂ is transition of P iff ex m1, m2 being marking of P st b₂ = [m1,m2] );

notation

let P be set ;
let t be transition of P;
synonym Pre t for P `1 ;
synonym Post t for P `2 ;

end;

definition

let P be set ;
let t be transition of P;
:: original: Pre
redefine func Pre t -> marking of P;
coherence
Pre is marking of P

proof end;

:: original: Post
redefine func Post t -> marking of P;
coherence
Post is marking of P

proof end;

end;

definition

let P be set ;
let m be marking of P;
let t be transition of P;

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

coherence
( ( Pre t c= m implies (m - (Pre t)) + (Post t) is marking of P ) & ( not Pre t c= m implies m is marking of P ) ) ;
consistency
for b₁ being marking of P holds verum ;

end;

:: deftheorem Def7 defines fire PNPROC_1:def 7 :
for P being set
for m being marking of P
for t being transition of P holds
( ( Pre t c= m implies fire (t,m) = (m - (Pre t)) + (Post t) ) & ( not Pre t c= m implies fire (t,m) = m ) );

theorem :: PNPROC_1:19

for P being set
for m being marking of P
for t1, t2 being transition of P st (Pre t1) + (Pre t2) c= m holds
fire (t2,(fire (t1,m))) = (((m - (Pre t1)) - (Pre t2)) + (Post t1)) + (Post t2)

proof end;

definition

let P be set ;
let t be transition of P;

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

existence
ex b₁ being Function st
( dom b₁ = Funcs (P,NAT) & ( for m being marking of P holds b₁ . m = fire (t,m) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = Funcs (P,NAT) & ( for m being marking of P holds b₁ . m = fire (t,m) ) & dom b₂ = Funcs (P,NAT) & ( for m being marking of P holds b₂ . m = fire (t,m) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines fire PNPROC_1:def 8 :
for P being set
for t being transition of P
for b₃ being Function holds
( b₃ = fire t iff ( dom b₃ = Funcs (P,NAT) & ( for m being marking of P holds b₃ . m = fire (t,m) ) ) );

theorem Th20: :: PNPROC_1:20

for P being set
for t being transition of P holds rng (fire t) c= Funcs (P,NAT)

proof end;

theorem :: PNPROC_1:21

for P being set
for m being marking of P
for t1, t2 being transition of P holds fire (t2,(fire (t1,m))) = ((fire t2) * (fire t1)) . m

proof end;

definition

let P be set ;

mode Petri_net of P -> non empty set means :Def9: :: PNPROC_1:def 9
for x being set st x in it holds
x is transition of P;

existence
ex b₁ being non empty set st
for x being set st x in b₁ holds
x is transition of P

proof end;

end;

:: deftheorem Def9 defines Petri_net PNPROC_1:def 9 :
for P being set
for b₂ being non empty set holds
( b₂ is Petri_net of P iff for x being set st x in b₂ holds
x is transition of P );

definition

let P be set ;
let N be Petri_net of P;
:: original: Element
redefine mode Element of N -> transition of P;
coherence
for b₁ being Element of N holds b₁ is transition of P by Def9;

end;

definition

let P be set ;
let N be Petri_net of P;
mode firing-sequence of N is Element of N * ;

end;

definition

let P be set ;
let N be Petri_net of P;
let C be firing-sequence of N;

func fire C -> Function means :Def10: :: 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) ) );

existence
ex b₁ being Function ex F being Function-yielding FinSequence st
( b₁ = 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) ) )

proof end;

uniqueness
for b₁, b₂ being Function st ex F being Function-yielding FinSequence st
( b₁ = 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) ) ) & ex F being Function-yielding FinSequence st
( b₂ = 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) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines fire PNPROC_1:def 10 :
for P being set
for N being Petri_net of P
for C being firing-sequence of N
for b₄ being Function holds
( b₄ = fire C iff ex F being Function-yielding FinSequence st
( b₄ = 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) ) ) );

:: Firing of empty firing-sequence <*>N

theorem :: PNPROC_1:22

for P being set
for N being Petri_net of P holds fire (<*> N) = id (Funcs (P,NAT))

proof end;

:: Firing of firing-sequence with one translation <*e*>

theorem Th23: :: PNPROC_1:23

for P being set
for N being Petri_net of P
for e being Element of N holds fire <*e*> = fire e

proof end;

theorem Th24: :: PNPROC_1:24

for P being set
for N being Petri_net of P
for e being Element of N holds (fire e) * (id (Funcs (P,NAT))) = fire e

proof end;

:: Firing of firing-sequence with two translations <*e1,e2*>

theorem :: PNPROC_1:25

for P being set
for N being Petri_net of P
for e1, e2 being Element of N holds fire <*e1,e2*> = (fire e2) * (fire e1)

proof end;

theorem Th26: :: PNPROC_1:26

for P being set
for N being Petri_net of P
for C being firing-sequence of N holds
( dom (fire C) = Funcs (P,NAT) & rng (fire C) c= Funcs (P,NAT) )

proof end;

:: Firing of compound firing-sequence

theorem Th27: :: PNPROC_1:27

for P being set
for N being Petri_net of P
for C1, C2 being firing-sequence of N holds fire (C1 ^ C2) = (fire C2) * (fire C1)

proof end;

theorem :: PNPROC_1:28

for P being set
for N being Petri_net of P
for e being Element of N
for C being firing-sequence of N holds fire (C ^ <*e*>) = (fire e) * (fire C)

proof end;

definition

let P be set ;
let N be Petri_net of P;
let C be firing-sequence of N;
let m be marking of P;

func fire (C,m) -> marking of P equals :: PNPROC_1:def 11
(fire C) . m;

coherence
(fire C) . m is marking of P

proof end;

end;

:: deftheorem defines fire PNPROC_1:def 11 :
for P being set
for N being Petri_net of P
for C being firing-sequence of N
for m being marking of P holds fire (C,m) = (fire C) . m;

definition

let P be set ;
let N be Petri_net of P;
mode process of N is Subset of (N *);

end;

definition

let P be set ;
let N be Petri_net of P;
let R1, R2 be process of N;

func R1 before R2 -> process of N equals :: PNPROC_1:def 12
{ (C1 ^ C2) where C1, C2 is firing-sequence of N : ( C1 in R1 & C2 in R2 ) } ;

coherence
{ (C1 ^ C2) where C1, C2 is firing-sequence of N : ( C1 in R1 & C2 in R2 ) } is process of N

proof end;

end;

:: deftheorem defines before PNPROC_1:def 12 :
for P being set
for N being Petri_net of P
for R1, R2 being process of N holds R1 before R2 = { (C1 ^ C2) where C1, C2 is firing-sequence of N : ( C1 in R1 & C2 in R2 ) } ;

registration

let P be set ;
let N be Petri_net of P;
let R1, R2 be non empty process of N;

cluster R1 before R2 -> non empty ;

coherence
not R1 before R2 is empty

proof end;

end;

theorem Th29: :: PNPROC_1:29

for P being set
for N being Petri_net of P
for R, R1, R2 being process of N holds (R1 \/ R2) before R = (R1 before R) \/ (R2 before R)

proof end;

theorem Th30: :: PNPROC_1:30

for P being set
for N being Petri_net of P
for R, R1, R2 being process of N holds R before (R1 \/ R2) = (R before R1) \/ (R before R2)

proof end;

theorem Th31: :: PNPROC_1:31

for P being set
for N being Petri_net of P
for C1, C2 being firing-sequence of N holds {C1} before {C2} = {(C1 ^ C2)}

proof end;

theorem :: PNPROC_1:32

for P being set
for N being Petri_net of P
for C, C1, C2 being firing-sequence of N holds {C1,C2} before {C} = {(C1 ^ C),(C2 ^ C)}

proof end;

theorem :: PNPROC_1:33

for P being set
for N being Petri_net of P
for C, C1, C2 being firing-sequence of N holds {C} before {C1,C2} = {(C ^ C1),(C ^ C2)}

proof end;

definition

let P be set ;
let N be Petri_net of P;
let R1, R2 be process of N;

func R1 concur R2 -> process of N equals :: PNPROC_1:def 13
{ C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } ;

coherence
{ C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } is process of N

proof end;

commutativity
for b₁, R1, R2 being process of N st b₁ = { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } holds
b₁ = { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) }

proof end;

end;

:: deftheorem defines concur PNPROC_1:def 13 :
for P being set
for N being Petri_net of P
for R1, R2 being process of N holds R1 concur R2 = { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } ;

theorem Th34: :: PNPROC_1:34

for P being set
for N being Petri_net of P
for R, R1, R2 being process of N holds (R1 \/ R2) concur R = (R1 concur R) \/ (R2 concur R)

proof end;

theorem Th35: :: PNPROC_1:35

for P being set
for N being Petri_net of P
for e1, e2 being Element of N holds {<*e1*>} concur {<*e2*>} = {<*e1,e2*>,<*e2,e1*>}

proof end;

theorem :: PNPROC_1:36

for P being set
for N being Petri_net of P
for e, e1, e2 being Element of N holds {<*e1*>,<*e2*>} concur {<*e*>} = {<*e1,e*>,<*e2,e*>,<*e,e1*>,<*e,e2*>}

proof end;

theorem :: PNPROC_1:37

for P being set
for N being Petri_net of P
for R1, R2, R3 being process of N holds (R1 before R2) before R3 = R1 before (R2 before R3)

proof end;

notation

let p be FinSubsequence;
let i be Element of NAT ;
synonym i Shift p for Shift (p,i);

end;

theorem :: PNPROC_1:38

for P being set
for N being Petri_net of P
for R1, R2, R3 being process of N holds (R1 concur R2) concur R3 = R1 concur (R2 concur R3)

proof end;

theorem :: PNPROC_1:39

for P being set
for N being Petri_net of P
for R1, R2 being process of N holds R1 before R2 c= R1 concur R2

proof end;

theorem :: PNPROC_1:40

for P being set
for N being Petri_net of P
for R1, R2, P1, P2 being process of N st R1 c= P1 & R2 c= P2 holds
R1 before R2 c= P1 before P2

proof end;

theorem :: PNPROC_1:41

for P being set
for N being Petri_net of P
for R1, R2, P1, P2 being process of N st R1 c= P1 & R2 c= P2 holds
R1 concur R2 c= P1 concur P2

proof end;

Lm2: for p1, p2 being FinSequence
for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds
dom (q1 \/ ((len p1) Shift q2)) c= dom (p1 ^ p2)

proof end;

Lm3: for p1 being FinSequence
for q1, q2 being FinSubsequence st q1 c= p1 holds
q1 misses (len p1) Shift q2
by VALUED_1:50, XBOOLE_1:63;

theorem :: PNPROC_1:42

for P being set
for N being Petri_net of P
for R1, R2, P1, P2 being process of N holds (R1 concur R2) before (P1 concur P2) c= (R1 before P1) concur (R2 before P2)

proof end;

registration

let P be set ;
let N be Petri_net of P;
let R1, R2 be non empty process of N;

cluster R1 concur R2 -> non empty ;

coherence
not R1 concur R2 is empty

proof end;

end;

definition

let P be set ;
let N be Petri_net of P;

func NeutralProcess N -> non empty process of N equals :: PNPROC_1:def 14
{(<*> N)};

coherence
{(<*> N)} is non empty process of N ;

end;

:: deftheorem defines NeutralProcess PNPROC_1:def 14 :
for P being set
for N being Petri_net of P holds NeutralProcess N = {(<*> N)};

definition

let P be set ;
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*>};

coherence
{<*t*>} is non empty process of N ;

end;

:: deftheorem defines ElementaryProcess PNPROC_1:def 15 :
for P being set
for N being Petri_net of P
for t being Element of N holds ElementaryProcess t = {<*t*>};

theorem :: PNPROC_1:43

for P being set
for N being Petri_net of P
for R being process of N holds (NeutralProcess N) before R = R

proof end;

theorem :: PNPROC_1:44

for P being set
for N being Petri_net of P
for R being process of N holds R before (NeutralProcess N) = R

proof end;

theorem :: PNPROC_1:45

for P being set
for N being Petri_net of P
for R being process of N holds (NeutralProcess N) concur R = R

proof end;