:: by Pratima K. Shah , Pauline N. Kawamoto and Mariusz Giero

::

:: Received March 31, 2014

:: Copyright (c) 2014-2018 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

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)

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;

coherence

for b_{1} being FinSequence of D st b_{1} = <*a,b,a*> holds

b_{1} is circular

end;
let a, b be Element of D;

coherence

for b

b

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;

( ( not P is empty implies ex b_{1} being FinSequence of Y st

( len b_{1} = len the Enumeration of P & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = M0 . ( the Enumeration of P . i) ) ) ) & ( P is empty implies ex b_{1} being FinSequence of Y st b_{1} = <*> Y ) )

for b_{1} being FinSequence of Y holds verum
;

end;
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 ( 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;

( ( not P is empty implies ex b

( len b

b

proof end;

consistency for b

:: 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 b_{5} being FinSequence of Y holds

( ( not P is empty implies ( b_{5} is Enumeration of M0,P iff ( len b_{5} = len the Enumeration of P & ( for i being Nat st i in dom b_{5} holds

b_{5} . i = M0 . ( the Enumeration of P . i) ) ) ) ) & ( P is empty implies ( b_{5} is Enumeration of M0,P iff b_{5} = <*> Y ) ) );

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 b

( ( not P is empty implies ( b

b

definition

PT_net_Str(# {0},{1},([#] ({0},{1})),([#] ({1},{0})) #) is Petri_net by PETRI:def 1, PETRI:def 2;

end;

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})) #);

PT_net_Str(# {0},{1},([#] ({0},{1})),([#] ({1},{0})) #) is Petri_net by PETRI:def 1, PETRI:def 2;

:: deftheorem defines PetriNet PETRI_DF:def 2 :

PetriNet = PT_net_Str(# {0},{1},([#] ({0},{1})),([#] ({1},{0})) #);

PetriNet = PT_net_Str(# {0},{1},([#] ({0},{1})),([#] ({1},{0})) #);

definition

let PTN be Petri_net;

let fs be FinSequence of places_and_trans_of PTN;

{ p where p is place of PTN : p in rng fs } is finite Subset of PTN

{ t where t is transition of PTN : t in rng fs } is finite Subset of the carrier' of PTN

end;
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 } ;

{ 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 } ;

{ t where t is transition of PTN : t in rng fs } is finite Subset of the carrier' of PTN

proof 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 } ;

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

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 ;

coherence

Funcs ( the carrier of N,NAT) is FUNCTION_DOMAIN of the carrier of N, NAT ;

;

end;
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 Funcs ( the carrier of N,NAT);

coherence

Funcs ( the carrier of N,NAT) is FUNCTION_DOMAIN of the carrier of N, NAT ;

;

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

for N being PT_net_Str holds nat_marks_of N = Funcs ( the carrier of N,NAT);

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

coherence

Sum the Enumeration of M0,P is Element of NAT ;

end;
let P be finite Subset of N;

let M0 be marking of N;

coherence

Sum the Enumeration of M0,P is Element of NAT ;

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

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;

end;
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 ) );

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

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

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

:: FinSequence of places_and_trans_of Petri_net

definition

let PTN be Petri_net;

let IT be FinSequence of places_and_trans_of PTN;

end;
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 );

( 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 );

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

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

fs is directed_path_like

proof end;

registration

let PTN be Petri_net;

coherence

for b_{1} being FinSequence of places_and_trans_of PTN st b_{1} is directed_path_like holds

not b_{1} is empty
;

end;
coherence

for b

not b

:: With_directed_path Mode for place\transition Nets

definition

let IT be Petri_net;

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

ex fs being FinSequence of places_and_trans_of IT st fs is directed_path_like ;

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

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

:: places_and_trans_of PetriNet

definition

let PTN be Petri_net;

end;
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 );

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

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

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

coherence

( PetriNet is decision_free_like & PetriNet is With_directed_circuit & PetriNet is Petri )

end;
( PetriNet is decision_free_like & PetriNet is With_directed_circuit & PetriNet is Petri )

proof end;

registration

ex b_{1} being Petri_net st

( b_{1} is With_directed_circuit & b_{1} is Petri & b_{1} is decision_free_like )
end;

cluster non empty non void V128() with_S-T_arc with_T-S_arc Petri decision_free_like With_directed_circuit for Petri_net;

existence ex b

( b

proof end;

registration

for b_{1} being Petri_net st b_{1} is With_directed_circuit holds

b_{1} is With_directed_path
;

end;

cluster non empty non void with_S-T_arc with_T-S_arc With_directed_circuit -> With_directed_path for Petri_net;

coherence for b

b

registration

let Dftn be With_directed_path Petri_net;

ex b_{1} being FinSequence of places_and_trans_of Dftn st b_{1} is directed_path_like
by Def9;

end;
cluster V7() V10( NAT ) V11( places_and_trans_of Dftn) Function-like finite FinSequence-like FinSubsequence-like directed_path_like for of ;

existence ex b

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

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

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

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

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 )

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 )

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;

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

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

definition

let PTN be Petri_net;

let M0 be marking of PTN;

let t be transition of PTN;

( ( t is_firable_at M0 implies ex b_{1} being marking of PTN st

for s being place of PTN holds

( ( s in *' {t} & not s in {t} *' implies b_{1} . s = (M0 . s) - 1 ) & ( s in {t} *' & not s in *' {t} implies b_{1} . s = (M0 . s) + 1 ) & ( ( ( s in *' {t} & s in {t} *' ) or ( not s in *' {t} & not s in {t} *' ) ) implies b_{1} . s = M0 . s ) ) ) & ( not t is_firable_at M0 implies ex b_{1} being marking of PTN st b_{1} = M0 ) )

for b_{1}, b_{2} 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 b_{1} . s = (M0 . s) - 1 ) & ( s in {t} *' & not s in *' {t} implies b_{1} . s = (M0 . s) + 1 ) & ( ( ( s in *' {t} & s in {t} *' ) or ( not s in *' {t} & not s in {t} *' ) ) implies b_{1} . s = M0 . s ) ) ) & ( for s being place of PTN holds

( ( s in *' {t} & not s in {t} *' implies b_{2} . s = (M0 . s) - 1 ) & ( s in {t} *' & not s in *' {t} implies b_{2} . s = (M0 . s) + 1 ) & ( ( ( s in *' {t} & s in {t} *' ) or ( not s in *' {t} & not s in {t} *' ) ) implies b_{2} . s = M0 . s ) ) ) implies b_{1} = b_{2} ) & ( not t is_firable_at M0 & b_{1} = M0 & b_{2} = M0 implies b_{1} = b_{2} ) )

consistency

for b_{1} being marking of PTN holds verum;

;

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

( ( t is_firable_at M0 implies ex b

for s being place of PTN holds

( ( s in *' {t} & not s in {t} *' implies b

proof end;

uniqueness for b

( ( t is_firable_at M0 & ( for s being place of PTN holds

( ( s in *' {t} & not s in {t} *' implies b

( ( s in *' {t} & not s in {t} *' implies b

proof end;

correctness consistency

for b

;

:: 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 b_{4} being marking of PTN holds

( ( t is_firable_at M0 implies ( b_{4} = Firing (t,M0) iff for s being place of PTN holds

( ( s in *' {t} & not s in {t} *' implies b_{4} . s = (M0 . s) - 1 ) & ( s in {t} *' & not s in *' {t} implies b_{4} . s = (M0 . s) + 1 ) & ( ( ( s in *' {t} & s in {t} *' ) or ( not s in *' {t} & not s in {t} *' ) ) implies b_{4} . s = M0 . s ) ) ) ) & ( not t is_firable_at M0 implies ( b_{4} = Firing (t,M0) iff b_{4} = M0 ) ) );

for PTN being Petri_net

for M0 being marking of PTN

for t being transition of PTN

for b

( ( t is_firable_at M0 implies ( b

( ( s in *' {t} & not s in {t} *' implies b

definition

let PTN be Petri_net;

let M0 be marking of PTN;

let Q be FinSequence of the carrier' of PTN;

end;
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)) ) ) ) );

( 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)) ) ) ) );

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

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

definition

let PTN be Petri_net;

let M0 be marking of PTN;

let Q be FinSequence of the carrier' of PTN;

( ( Q = {} implies ex b_{1} being marking of PTN st b_{1} = M0 ) & ( not Q = {} implies ex b_{1} being marking of PTN ex M being FinSequence of nat_marks_of PTN st

( len Q = len M & b_{1} = 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)) ) ) ) )

for b_{1}, b_{2} being marking of PTN holds

( ( Q = {} & b_{1} = M0 & b_{2} = M0 implies b_{1} = b_{2} ) & ( not Q = {} & ex M being FinSequence of nat_marks_of PTN st

( len Q = len M & b_{1} = 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 & b_{2} = 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 b_{1} = b_{2} ) )

consistency

for b_{1} being marking of PTN holds verum;

;

end;
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 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)) ) );

( ( Q = {} implies ex b

( len Q = len M & b

M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) )

proof end;

uniqueness for b

( ( Q = {} & b

( len Q = len M & b

M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) & ex M being FinSequence of nat_marks_of PTN st

( len Q = len M & b

M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) implies b

proof end;

correctness consistency

for b

;

:: 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 b_{4} being marking of PTN holds

( ( Q = {} implies ( b_{4} = Firing (Q,M0) iff b_{4} = M0 ) ) & ( not Q = {} implies ( b_{4} = Firing (Q,M0) iff ex M being FinSequence of nat_marks_of PTN st

( len Q = len M & b_{4} = 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)) ) ) ) ) );

for PTN being Petri_net

for M0 being marking of PTN

for Q being FinSequence of the carrier' of PTN

for b

( ( Q = {} implies ( b

( len Q = len M & b

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)

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 )

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

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 )

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

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

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;

registration

let Dftn be With_directed_circuit Petri_net;

ex b_{1} being FinSequence of places_and_trans_of Dftn st

( b_{1} is directed_path_like & b_{1} is circular & b_{1} is almost-one-to-one )
by Def7;

end;
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 of ;

existence ex b

( b

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;
mode Circuit_of_places_and_trans of Dftn is circular almost-one-to-one directed_path_like FinSequence of places_and_trans_of Dftn;

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

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

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;