PETRI_DF: The Formalization of Decision Free {P}etri Net

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;

proof end;

consistency ;

end;

:: deftheorem Def12 defines Enumeration PETRI_DF:def 1 :

definition

func PetriNet -> Petri_net equals :: PETRI_DF:def 2
PT_net_Str(# {0},{1},([#] ({0},{1})),([#] ({1},{0})) #);

coherence by PETRI:def 1, PETRI:def 2;

end;

:: deftheorem defines PetriNet PETRI_DF:def 2 :

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 ;

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

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

proof end;

end;

:: deftheorem defines places_of PETRI_DF:def 3 :

:: deftheorem defines transitions_of PETRI_DF:def 4 :

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

end;

:: deftheorem defines nat_marks_of PETRI_DF:def 5 :

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;

end;

:: deftheorem defines num_marks PETRI_DF:def 6 :

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

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

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;

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 :

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

registration

cluster PetriNet -> Petri decision_free_like With_directed_circuit ;

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 ;

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 ;

end;

registration

cluster non empty non void V128() with_S-T_arc with_T-S_arc With_directed_path for PT_net_Str ;

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

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 :

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;

proof end;

uniqueness

proof end;

correctness ;

end;

:: deftheorem Def11 defines Firing PETRI_DF:def 12 :

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 :

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