:: 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-2016 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 PETRI_DF, NUMBERS, XBOOLE_0, FUNCT_1, SUBSET_1, RELAT_1, TARSKI,
PETRI, FUNCT_2, ARYTM_3, FINSEQ_1, PARTFUN1, XXREAL_0, CARD_1, CARD_3,
ORDINAL4, NAT_1, ARYTM_1, BOOLMARK, STRUCT_0, PNPROC_1, ZFMISC_1, INT_1,
FINSET_1, AOFA_I00, NET_1, FINSEQ_4, RFINSEQ, FINSEQ_6, JORDAN23;
notations TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, NAT_1, FUNCT_1,
PARTFUN1, FUNCT_2, DOMAIN_1, XXREAL_0, STRUCT_0, ZFMISC_1, RELSET_1,
FINSEQ_1, PARTIT_2, PETRI, FINSET_1, NAT_D, WSIERP_1, RLAFFIN3, NET_1,
FINSEQ_6, FINSEQ_4, JORDAN23, RFINSEQ;
constructors PARTIT_2, NAT_D, WSIERP_1, RLAFFIN3, NET_1, FINSEQ_4, FINSEQ_6,
RFINSEQ, JORDAN23;
registrations XXREAL_0, XREAL_0, FINSEQ_1, ORDINAL1, CARD_1, RELSET_1,
STRUCT_0, XBOOLE_0, SUBSET_1, XTUPLE_0, FINSET_1, NAT_1, MEMBERED,
VALUED_0, PETRI;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Preliminaries
reserve N for PT_net_Str, PTN for Petri_net, i for Nat;
theorem :: PETRI_DF:1
for x,y be Nat, f be 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;
theorem :: PETRI_DF:2
for D be non empty set, f be non empty FinSequence of D
st f is circular holds f.1 = f.len f;
registration
let D be non empty set;
let a,b be Element of D;
cluster <*a,b,a*> -> circular for FinSequence of D;
end;
theorem :: PETRI_DF:3
for a,b be object st a <> b holds <*a,b,a*> is almost-one-to-one;
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
:: PETRI_DF:def 1
len it = len the Enumeration of P &
for i st i in dom it holds
it.i = M0.((the Enumeration of P).i) if P is non empty
otherwise it = <*>Y;
end;
definition
func PetriNet -> Petri_net equals
:: PETRI_DF:def 2
PT_net_Str(# {0},{1},[#] ({0},{1}),[#] ({1},{0}) #);
end;
notation
let N;
synonym places_and_trans_of N for Elements N;
end;
registration
let PTN;
cluster places_and_trans_of PTN -> non empty;
end;
reserve fs for FinSequence of places_and_trans_of PTN;
definition
let PTN,fs;
func places_of fs -> finite Subset of PTN equals
:: PETRI_DF:def 3
{ p where p is place of PTN : p in rng fs };
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};
end;
begin :: The number of tokens in a circuit
:: Relation Between P and NAT
definition
let N;
func nat_marks_of N -> FUNCTION_DOMAIN of the carrier of N, NAT equals
:: PETRI_DF:def 5
Funcs(the carrier of N, NAT);
end;
definition
let N;
mode marking of N is Element of nat_marks_of N;
end;
:: Generation of nat marking and summation of that
definition
let N;
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;
begin
:: 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
:: 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;
:: directed_path_like Attribute for
:: FinSequence of places_and_trans_of Petri_net
definition
let PTN;
let IT be FinSequence of places_and_trans_of PTN;
attr IT is directed_path_like means
:: PETRI_DF:def 8
len IT >= 3 & len IT mod 2 = 1 &
(for i 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;
theorem :: PETRI_DF:4
for fs be FinSequence of places_and_trans_of PetriNet st fs = <*0,1,0*>
holds fs is directed_path_like;
registration
let PTN;
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
:: PETRI_DF:def 9
ex fs being FinSequence of places_and_trans_of IT st
fs is directed_path_like;
end;
:: directed_circuit_like Attribute for FinSequence of
:: places_and_trans_of PetriNet
definition
let PTN;
attr PTN is With_directed_circuit means
:: PETRI_DF:def 10
ex fs st fs is directed_path_like circular almost-one-to-one;
end;
registration
cluster PetriNet -> decision_free_like With_directed_circuit Petri;
end;
registration
cluster With_directed_circuit Petri decision_free_like for Petri_net;
end;
registration
cluster With_directed_circuit -> With_directed_path for Petri_net;
end;
registration
cluster With_directed_path for Petri_net;
end;
registration
let Dftn be With_directed_path Petri_net;
cluster directed_path_like for FinSequence of places_and_trans_of Dftn;
end;
reserve Dftn for With_directed_path Petri_net;
reserve dct for directed_path_like FinSequence of places_and_trans_of Dftn;
theorem :: PETRI_DF:5
[dct.1, dct.2] in the S-T_Arcs of Dftn;
theorem :: PETRI_DF:6
[dct.(len dct -1), dct.(len dct)] in the T-S_Arcs of Dftn;
reserve Dftn for With_directed_path Petri Petri_net,
dct for directed_path_like FinSequence of places_and_trans_of Dftn;
theorem :: PETRI_DF:7
dct.i in places_of dct & i in dom dct implies i mod 2 = 1;
theorem :: PETRI_DF:8
dct.i in transitions_of dct & i in dom dct implies i mod 2 = 0;
theorem :: PETRI_DF:9
dct.i in transitions_of dct & i in dom dct implies
[dct.(i-1),dct.i] in the S-T_Arcs of Dftn
& [dct.i,dct.(i+1)] in the T-S_Arcs of Dftn;
theorem :: PETRI_DF:10
dct.i in places_of dct & 1 < i & i < len dct implies
[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;
begin :: Firable and Firing Conditions for Transitions with natural marking
reserve M0 for marking of PTN,
t for transition of PTN,
Q,Q1 for FinSequence of the carrier' of PTN;
definition
let PTN,M0,t;
pred t is_firable_at M0 means
:: PETRI_DF:def 11
for m being Nat holds m in M0.:*'{t} implies m > 0;
end;
notation
let PTN,M0,t;
antonym t is_not_firable_at M0 for t is_firable_at M0;
end;
definition
let PTN,M0,t;
func Firing(t, M0) -> marking of PTN means
:: 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;
end;
definition
let PTN,M0,Q;
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 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;
notation
let PTN,M0,Q;
antonym Q is_not_firable_at M0 for Q is_firable_at M0;
end;
definition
let PTN,M0,Q;
func Firing(Q, M0) -> marking of PTN means
:: 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 st i < len Q & i > 0 holds M/.(i+1) = Firing(Q/.(i+1),M/.i);
end;
theorem :: PETRI_DF:11
Firing(t, M0) = Firing(<*t*>, M0);
theorem :: PETRI_DF:12
t is_firable_at M0 iff <*t*> is_firable_at M0;
theorem :: PETRI_DF:13
Firing(Q^Q1, M0) = Firing(Q1, Firing(Q,M0));
theorem :: PETRI_DF:14
Q^Q1 is_firable_at M0
implies Q1 is_firable_at Firing(Q, M0) & Q is_firable_at M0;
begin
:: The theorem stating that the number of tokens in a circuit
:: remains the same after any firing sequence
theorem :: PETRI_DF:15
for Dftn being With_directed_path Petri decision_free_like Petri_net,
dct being directed_path_like FinSequence of places_and_trans_of Dftn,
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;
definition
mode Decision_free_PT is
With_directed_circuit Petri decision_free_like Petri_net;
end;
registration
let Dftn be With_directed_circuit Petri_net;
cluster directed_path_like circular almost-one-to-one
for FinSequence of places_and_trans_of Dftn;
end;
definition
let Dftn be With_directed_circuit Petri_net;
mode Circuit_of_places_and_trans of Dftn is
directed_path_like circular almost-one-to-one
FinSequence of places_and_trans_of Dftn;
end;
theorem :: PETRI_DF:16
for Dftn being Decision_free_PT,
dct being Circuit_of_places_and_trans of Dftn,
M0 being marking of Dftn, t being transition of Dftn
holds num_marks(places_of dct, M0) = num_marks(places_of dct, Firing(t, M0));
theorem :: PETRI_DF:17
for Dftn being Decision_free_PT,
dct being Circuit_of_places_and_trans of Dftn,
M0 being marking of Dftn, Q being FinSequence of the carrier' of Dftn holds
num_marks(places_of dct, M0) = num_marks(places_of dct, Firing(Q, M0));