:: The Formalization of Decision Free {P}etri Net
:: by Pratima K. Shah , Pauline N. Kawamoto and Mariusz Giero
::
:: Received March 31, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users


theorem Th10: :: PETRI_DF:1
for x, y being Nat
for f being FinSequence st f /^ 1 is one-to-one & 1 < x & x <= len f & 1 < y & y <= len f & f . x = f . y holds
x = y
proof end;

theorem Lm1: :: PETRI_DF:2
for D being non empty set
for f being non empty FinSequence of D st f is circular holds
f . 1 = f . (len f)
proof end;

registration
let D be non empty set ;
let a, b be Element of D;
cluster <*a,b,a*> -> circular for FinSequence of D;
coherence
for b1 being FinSequence of D st b1 = <*a,b,a*> holds
b1 is circular
proof end;
end;

theorem Th13: :: PETRI_DF:3
for a, b being object st a <> b holds
<*a,b,a*> is almost-one-to-one
proof end;

definition
let X be set ;
let Y be non empty set ;
let P be finite Subset of X;
let M0 be Function of X,Y;
mode Enumeration of M0,P -> FinSequence of Y means :Def12: :: PETRI_DF:def 1
( len it = len the Enumeration of P & ( for i being Nat st i in dom it holds
it . i = M0 . ( the Enumeration of P . i) ) ) if not P is empty
otherwise it = <*> Y;
existence
( ( not P is empty implies ex b1 being FinSequence of Y st
( len b1 = len the Enumeration of P & ( for i being Nat st i in dom b1 holds
b1 . i = M0 . ( the Enumeration of P . i) ) ) ) & ( P is empty implies ex b1 being FinSequence of Y st b1 = <*> Y ) )
proof end;
consistency
for b1 being FinSequence of Y holds verum
;
end;

:: deftheorem Def12 defines Enumeration PETRI_DF:def 1 :
for X being set
for Y being non empty set
for P being finite Subset of X
for M0 being Function of X,Y
for b5 being FinSequence of Y holds
( ( not P is empty implies ( b5 is Enumeration of M0,P iff ( len b5 = len the Enumeration of P & ( for i being Nat st i in dom b5 holds
b5 . i = M0 . ( the Enumeration of P . i) ) ) ) ) & ( P is empty implies ( b5 is Enumeration of M0,P iff b5 = <*> Y ) ) );

definition
func PetriNet -> Petri_net equals :: PETRI_DF:def 2
PT_net_Str(# {0},{1},([#] ({0},{1})),([#] ({1},{0})) #);
coherence
PT_net_Str(# {0},{1},([#] ({0},{1})),([#] ({1},{0})) #) is Petri_net
by PETRI:def 1, PETRI:def 2;
end;

:: deftheorem defines PetriNet PETRI_DF:def 2 :
PetriNet = PT_net_Str(# {0},{1},([#] ({0},{1})),([#] ({1},{0})) #);

notation
let N be PT_net_Str ;
synonym places_and_trans_of N for Elements N;
end;

registration
let PTN be Petri_net;
cluster places_and_trans_of PTN -> non empty ;
coherence
not places_and_trans_of PTN is empty
;
end;

definition
let PTN be Petri_net;
let fs be FinSequence of places_and_trans_of PTN;
func places_of fs -> finite Subset of PTN equals :: PETRI_DF:def 3
{ p where p is place of PTN : p in rng fs } ;
coherence
{ p where p is place of PTN : p in rng fs } is finite Subset of PTN
proof end;
func transitions_of fs -> finite Subset of the carrier' of PTN equals :: PETRI_DF:def 4
{ t where t is transition of PTN : t in rng fs } ;
coherence
{ t where t is transition of PTN : t in rng fs } is finite Subset of the carrier' of PTN
proof end;
end;

:: deftheorem defines places_of PETRI_DF:def 3 :
for PTN being Petri_net
for fs being FinSequence of places_and_trans_of PTN holds places_of fs = { p where p is place of PTN : p in rng fs } ;

:: deftheorem defines transitions_of PETRI_DF:def 4 :
for PTN being Petri_net
for fs being FinSequence of places_and_trans_of PTN holds transitions_of fs = { t where t is transition of PTN : t in rng fs } ;

:: Relation Between P and NAT
definition
let N be PT_net_Str ;
func nat_marks_of N -> FUNCTION_DOMAIN of the carrier of N, NAT equals :: PETRI_DF:def 5
Funcs ( the carrier of N,NAT);
correctness
coherence
Funcs ( the carrier of N,NAT) is FUNCTION_DOMAIN of the carrier of N, NAT
;
;
end;

:: deftheorem defines nat_marks_of PETRI_DF:def 5 :
for N being PT_net_Str holds nat_marks_of N = Funcs ( the carrier of N,NAT);

definition
let N be PT_net_Str ;
mode marking of N is Element of nat_marks_of N;
end;

:: Generation of nat marking and summation of that
definition
let N be PT_net_Str ;
let P be finite Subset of N;
let M0 be marking of N;
func num_marks (P,M0) -> Element of NAT equals :: PETRI_DF:def 6
Sum the Enumeration of M0,P;
coherence
Sum the Enumeration of M0,P is Element of NAT
;
end;

:: deftheorem defines num_marks PETRI_DF:def 6 :
for N being PT_net_Str
for P being finite Subset of N
for M0 being marking of N holds num_marks (P,M0) = Sum the Enumeration of M0,P;

:: Decision-Free Petri Net Concept and Properties of Circuits in Petri Nets
definition
let IT be Petri_net;
attr IT is decision_free_like means :Def1: :: PETRI_DF:def 7
for s being place of IT holds
( ex t being transition of IT st [t,s] in the T-S_Arcs of IT & ( for t1, t2 being transition of IT st [t1,s] in the T-S_Arcs of IT & [t2,s] in the T-S_Arcs of IT holds
t1 = t2 ) & ex t being transition of IT st [s,t] in the S-T_Arcs of IT & ( for t1, t2 being transition of IT st [s,t1] in the S-T_Arcs of IT & [s,t2] in the S-T_Arcs of IT holds
t1 = t2 ) );
end;

:: deftheorem Def1 defines decision_free_like PETRI_DF:def 7 :
for IT being Petri_net holds
( IT is decision_free_like iff for s being place of IT holds
( ex t being transition of IT st [t,s] in the T-S_Arcs of IT & ( for t1, t2 being transition of IT st [t1,s] in the T-S_Arcs of IT & [t2,s] in the T-S_Arcs of IT holds
t1 = t2 ) & ex t being transition of IT st [s,t] in the S-T_Arcs of IT & ( for t1, t2 being transition of IT st [s,t1] in the S-T_Arcs of IT & [s,t2] in the S-T_Arcs of IT holds
t1 = t2 ) ) );

:: directed_path_like Attribute for
:: FinSequence of places_and_trans_of Petri_net
definition
let PTN be Petri_net;
let IT be FinSequence of places_and_trans_of PTN;
attr IT is directed_path_like means :Def5: :: PETRI_DF:def 8
( len IT >= 3 & (len IT) mod 2 = 1 & ( for i being Nat st i mod 2 = 1 & i + 1 < len IT holds
( [(IT . i),(IT . (i + 1))] in the S-T_Arcs of PTN & [(IT . (i + 1)),(IT . (i + 2))] in the T-S_Arcs of PTN ) ) & IT . (len IT) in the carrier of PTN );
end;

:: deftheorem Def5 defines directed_path_like PETRI_DF:def 8 :
for PTN being Petri_net
for IT being FinSequence of places_and_trans_of PTN holds
( IT is directed_path_like iff ( len IT >= 3 & (len IT) mod 2 = 1 & ( for i being Nat st i mod 2 = 1 & i + 1 < len IT holds
( [(IT . i),(IT . (i + 1))] in the S-T_Arcs of PTN & [(IT . (i + 1)),(IT . (i + 2))] in the T-S_Arcs of PTN ) ) & IT . (len IT) in the carrier of PTN ) );

theorem Th12: :: PETRI_DF:4
for fs being FinSequence of places_and_trans_of PetriNet st fs = <*0,1,0*> holds
fs is directed_path_like
proof end;

registration
let PTN be Petri_net;
cluster directed_path_like -> non empty for FinSequence of places_and_trans_of PTN;
coherence
for b1 being FinSequence of places_and_trans_of PTN st b1 is directed_path_like holds
not b1 is empty
;
end;

:: With_directed_path Mode for place\transition Nets
definition
let IT be Petri_net;
attr IT is With_directed_path means :Def9: :: PETRI_DF:def 9
ex fs being FinSequence of places_and_trans_of IT st fs is directed_path_like ;
end;

:: deftheorem Def9 defines With_directed_path PETRI_DF:def 9 :
for IT being Petri_net holds
( IT is With_directed_path iff ex fs being FinSequence of places_and_trans_of IT st fs is directed_path_like );

:: directed_circuit_like Attribute for FinSequence of
:: places_and_trans_of PetriNet
definition
let PTN be Petri_net;
attr PTN is With_directed_circuit means :Def7: :: PETRI_DF:def 10
ex fs being FinSequence of places_and_trans_of PTN st
( fs is directed_path_like & fs is circular & fs is almost-one-to-one );
end;

:: deftheorem Def7 defines With_directed_circuit PETRI_DF:def 10 :
for PTN being Petri_net holds
( PTN is With_directed_circuit iff ex fs being FinSequence of places_and_trans_of PTN st
( fs is directed_path_like & fs is circular & fs is almost-one-to-one ) );

registration
cluster PetriNet -> Petri decision_free_like With_directed_circuit ;
coherence
( PetriNet is decision_free_like & PetriNet is With_directed_circuit & PetriNet is Petri )
proof end;
end;

registration
cluster non empty non void V128() with_S-T_arc with_T-S_arc Petri decision_free_like With_directed_circuit for PT_net_Str ;
existence
ex b1 being Petri_net st
( b1 is With_directed_circuit & b1 is Petri & b1 is decision_free_like )
proof end;
end;

registration
cluster non empty non void with_S-T_arc with_T-S_arc With_directed_circuit -> With_directed_path for PT_net_Str ;
coherence
for b1 being Petri_net st b1 is With_directed_circuit holds
b1 is With_directed_path
;
end;

registration
cluster non empty non void V128() with_S-T_arc with_T-S_arc With_directed_path for PT_net_Str ;
existence
ex b1 being Petri_net st b1 is With_directed_path
proof end;
end;

registration
let Dftn be With_directed_path Petri_net;
cluster V7() V10( NAT ) V11( places_and_trans_of Dftn) Function-like finite FinSequence-like FinSubsequence-like directed_path_like for FinSequence of places_and_trans_of Dftn;
existence
ex b1 being FinSequence of places_and_trans_of Dftn st b1 is directed_path_like
by Def9;
end;

theorem Thd: :: PETRI_DF:5
for Dftn being With_directed_path Petri_net
for dct being directed_path_like FinSequence of places_and_trans_of Dftn holds [(dct . 1),(dct . 2)] in the S-T_Arcs of Dftn
proof end;

theorem The: :: PETRI_DF:6
for Dftn being With_directed_path Petri_net
for dct being directed_path_like FinSequence of places_and_trans_of Dftn holds [(dct . ((len dct) - 1)),(dct . (len dct))] in the T-S_Arcs of Dftn
proof end;

theorem Thc: :: PETRI_DF:7
for i being Nat
for Dftn being Petri With_directed_path Petri_net
for dct being directed_path_like FinSequence of places_and_trans_of Dftn st dct . i in places_of dct & i in dom dct holds
i mod 2 = 1
proof end;

theorem Thcc: :: PETRI_DF:8
for i being Nat
for Dftn being Petri With_directed_path Petri_net
for dct being directed_path_like FinSequence of places_and_trans_of Dftn st dct . i in transitions_of dct & i in dom dct holds
i mod 2 = 0
proof end;

theorem Thf: :: PETRI_DF:9
for i being Nat
for Dftn being Petri With_directed_path Petri_net
for dct being directed_path_like FinSequence of places_and_trans_of Dftn st dct . i in transitions_of dct & i in dom dct holds
( [(dct . (i - 1)),(dct . i)] in the S-T_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the T-S_Arcs of Dftn )
proof end;

theorem Thg: :: PETRI_DF:10
for i being Nat
for Dftn being Petri With_directed_path Petri_net
for dct being directed_path_like FinSequence of places_and_trans_of Dftn st dct . i in places_of dct & 1 < i & i < len dct holds
( [(dct . (i - 2)),(dct . (i - 1))] in the S-T_Arcs of Dftn & [(dct . (i - 1)),(dct . i)] in the T-S_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the S-T_Arcs of Dftn & [(dct . (i + 1)),(dct . (i + 2))] in the T-S_Arcs of Dftn & 3 <= i )
proof end;

definition
let PTN be Petri_net;
let M0 be marking of PTN;
let t be transition of PTN;
pred t is_firable_at M0 means :: PETRI_DF:def 11
for m being Nat st m in M0 .: (*' {t}) holds
m > 0 ;
end;

:: deftheorem defines is_firable_at PETRI_DF:def 11 :
for PTN being Petri_net
for M0 being marking of PTN
for t being transition of PTN holds
( t is_firable_at M0 iff for m being Nat st m in M0 .: (*' {t}) holds
m > 0 );

notation
let PTN be Petri_net;
let M0 be marking of PTN;
let t be transition of PTN;
antonym t is_not_firable_at M0 for t is_firable_at M0;
end;

definition
let PTN be Petri_net;
let M0 be marking of PTN;
let t be transition of PTN;
func Firing (t,M0) -> marking of PTN means :Def11: :: PETRI_DF:def 12
for s being place of PTN holds
( ( s in *' {t} & not s in {t} *' implies it . s = (M0 . s) - 1 ) & ( s in {t} *' & not s in *' {t} implies it . s = (M0 . s) + 1 ) & ( ( ( s in *' {t} & s in {t} *' ) or ( not s in *' {t} & not s in {t} *' ) ) implies it . s = M0 . s ) ) if t is_firable_at M0
otherwise it = M0;
existence
( ( t is_firable_at M0 implies ex b1 being marking of PTN st
for s being place of PTN holds
( ( s in *' {t} & not s in {t} *' implies b1 . s = (M0 . s) - 1 ) & ( s in {t} *' & not s in *' {t} implies b1 . s = (M0 . s) + 1 ) & ( ( ( s in *' {t} & s in {t} *' ) or ( not s in *' {t} & not s in {t} *' ) ) implies b1 . s = M0 . s ) ) ) & ( not t is_firable_at M0 implies ex b1 being marking of PTN st b1 = M0 ) )
proof end;
uniqueness
for b1, b2 being marking of PTN holds
( ( t is_firable_at M0 & ( for s being place of PTN holds
( ( s in *' {t} & not s in {t} *' implies b1 . s = (M0 . s) - 1 ) & ( s in {t} *' & not s in *' {t} implies b1 . s = (M0 . s) + 1 ) & ( ( ( s in *' {t} & s in {t} *' ) or ( not s in *' {t} & not s in {t} *' ) ) implies b1 . s = M0 . s ) ) ) & ( for s being place of PTN holds
( ( s in *' {t} & not s in {t} *' implies b2 . s = (M0 . s) - 1 ) & ( s in {t} *' & not s in *' {t} implies b2 . s = (M0 . s) + 1 ) & ( ( ( s in *' {t} & s in {t} *' ) or ( not s in *' {t} & not s in {t} *' ) ) implies b2 . s = M0 . s ) ) ) implies b1 = b2 ) & ( not t is_firable_at M0 & b1 = M0 & b2 = M0 implies b1 = b2 ) )
proof end;
correctness
consistency
for b1 being marking of PTN holds verum
;
;
end;

:: deftheorem Def11 defines Firing PETRI_DF:def 12 :
for PTN being Petri_net
for M0 being marking of PTN
for t being transition of PTN
for b4 being marking of PTN holds
( ( t is_firable_at M0 implies ( b4 = Firing (t,M0) iff for s being place of PTN holds
( ( s in *' {t} & not s in {t} *' implies b4 . s = (M0 . s) - 1 ) & ( s in {t} *' & not s in *' {t} implies b4 . s = (M0 . s) + 1 ) & ( ( ( s in *' {t} & s in {t} *' ) or ( not s in *' {t} & not s in {t} *' ) ) implies b4 . s = M0 . s ) ) ) ) & ( not t is_firable_at M0 implies ( b4 = Firing (t,M0) iff b4 = M0 ) ) );

definition
let PTN be Petri_net;
let M0 be marking of PTN;
let Q be FinSequence of the carrier' of PTN;
pred Q is_firable_at M0 means :: PETRI_DF:def 13
( Q = {} or ex M being FinSequence of nat_marks_of PTN st
( len Q = len M & Q /. 1 is_firable_at M0 & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
( Q /. (i + 1) is_firable_at M /. i & M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) );
end;

:: deftheorem defines is_firable_at PETRI_DF:def 13 :
for PTN being Petri_net
for M0 being marking of PTN
for Q being FinSequence of the carrier' of PTN holds
( Q is_firable_at M0 iff ( Q = {} or ex M being FinSequence of nat_marks_of PTN st
( len Q = len M & Q /. 1 is_firable_at M0 & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
( Q /. (i + 1) is_firable_at M /. i & M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) ) );

notation
let PTN be Petri_net;
let M0 be marking of PTN;
let Q be FinSequence of the carrier' of PTN;
antonym Q is_not_firable_at M0 for Q is_firable_at M0;
end;

definition
let PTN be Petri_net;
let M0 be marking of PTN;
let Q be FinSequence of the carrier' of PTN;
func Firing (Q,M0) -> marking of PTN means :Defb: :: PETRI_DF:def 14
it = M0 if Q = {}
otherwise ex M being FinSequence of nat_marks_of PTN st
( len Q = len M & it = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) );
existence
( ( Q = {} implies ex b1 being marking of PTN st b1 = M0 ) & ( not Q = {} implies ex b1 being marking of PTN ex M being FinSequence of nat_marks_of PTN st
( len Q = len M & b1 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) )
proof end;
uniqueness
for b1, b2 being marking of PTN holds
( ( Q = {} & b1 = M0 & b2 = M0 implies b1 = b2 ) & ( not Q = {} & ex M being FinSequence of nat_marks_of PTN st
( len Q = len M & b1 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) & ex M being FinSequence of nat_marks_of PTN st
( len Q = len M & b2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) implies b1 = b2 ) )
proof end;
correctness
consistency
for b1 being marking of PTN holds verum
;
;
end;

:: deftheorem Defb defines Firing PETRI_DF:def 14 :
for PTN being Petri_net
for M0 being marking of PTN
for Q being FinSequence of the carrier' of PTN
for b4 being marking of PTN holds
( ( Q = {} implies ( b4 = Firing (Q,M0) iff b4 = M0 ) ) & ( not Q = {} implies ( b4 = Firing (Q,M0) iff ex M being FinSequence of nat_marks_of PTN st
( len Q = len M & b4 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) ) );

theorem :: PETRI_DF:11
for PTN being Petri_net
for M0 being marking of PTN
for t being transition of PTN holds Firing (t,M0) = Firing (<*t*>,M0)
proof end;

theorem :: PETRI_DF:12
for PTN being Petri_net
for M0 being marking of PTN
for t being transition of PTN holds
( t is_firable_at M0 iff <*t*> is_firable_at M0 )
proof end;

theorem :: PETRI_DF:13
for PTN being Petri_net
for M0 being marking of PTN
for Q, Q1 being FinSequence of the carrier' of PTN holds Firing ((Q ^ Q1),M0) = Firing (Q1,(Firing (Q,M0)))
proof end;

theorem :: PETRI_DF:14
for PTN being Petri_net
for M0 being marking of PTN
for Q, Q1 being FinSequence of the carrier' of PTN st Q ^ Q1 is_firable_at M0 holds
( Q1 is_firable_at Firing (Q,M0) & Q is_firable_at M0 )
proof end;

:: The theorem stating that the number of tokens in a circuit
:: remains the same after any firing sequence
theorem Thb: :: PETRI_DF:15
for Dftn being Petri decision_free_like With_directed_path Petri_net
for dct being directed_path_like FinSequence of places_and_trans_of Dftn
for t being transition of Dftn st dct is circular & ex p1 being place of Dftn st
( p1 in places_of dct & ( [p1,t] in the S-T_Arcs of Dftn or [t,p1] in the T-S_Arcs of Dftn ) ) holds
t in transitions_of dct
proof end;

definition
mode Decision_free_PT is Petri decision_free_like With_directed_circuit Petri_net;
end;

registration
let Dftn be With_directed_circuit Petri_net;
cluster V7() V10( NAT ) V11( places_and_trans_of Dftn) Function-like finite FinSequence-like FinSubsequence-like circular almost-one-to-one directed_path_like for FinSequence of places_and_trans_of Dftn;
existence
ex b1 being FinSequence of places_and_trans_of Dftn st
( b1 is directed_path_like & b1 is circular & b1 is almost-one-to-one )
by Def7;
end;

definition
let Dftn be With_directed_circuit Petri_net;
mode Circuit_of_places_and_trans of Dftn is circular almost-one-to-one directed_path_like FinSequence of places_and_trans_of Dftn;
end;

theorem Th7: :: PETRI_DF:16
for Dftn being Decision_free_PT
for dct being Circuit_of_places_and_trans of Dftn
for M0 being marking of Dftn
for t being transition of Dftn holds num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (t,M0)))
proof end;

theorem :: PETRI_DF:17
for Dftn being Decision_free_PT
for dct being Circuit_of_places_and_trans of Dftn
for M0 being marking of Dftn
for Q being FinSequence of the carrier' of Dftn holds num_marks ((places_of dct),M0) = num_marks ((places_of dct),(Firing (Q,M0)))
proof end;