:: Formulation of Cell Petri Nets
:: by Mitsuru Jitsukawa , Pauline N. Kawamoto and Yasunari Shidama
::
:: Received December 8, 2013
:: Copyright (c) 2013-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 TARSKI, RELAT_1, ARYTM_3, PETRI, PETRI_2, FUNCT_7, FUNCT_1,
FINSET_1, FUNCOP_1, ZFMISC_1, SUBSET_1, BOOLMARK, NUMBERS, XBOOLE_0,
FUNCT_2, FUNCT_4, PBOOLE, SETLIM_2, XXREAL_0, PETRI_3, PROB_2, MCART_1,
CARD_1, CARD_3, STRUCT_0, ARYTM_1;
notations TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, XCMPLX_0, SUBSET_1, RELAT_1,
FUNCT_1, RELSET_1, FUNCT_2, DOMAIN_1, MSAFREE4, FUNCOP_1, FUNCT_4,
FINSET_1, NUMBERS, NAT_1, XXREAL_0, PBOOLE, RELSET_2, STRUCT_0, PETRI,
PETRI_2, CARD_3;
constructors RELSET_1, DOMAIN_1, VALUED_1, PETRI_2, RELSET_2, FUNCT_4,
MSAFREE4;
registrations SUBSET_1, ORDINAL1, RELAT_1, RELSET_1, XBOOLE_0, XREAL_0,
PBOOLE, NAT_1, FUNCT_2, FINSET_1, PETRI, PETRI_2, XTUPLE_0, STRUCT_0,
INT_1, CHAIN_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: Preliminaries
definition
let I be non empty set;
let CPNTS be ManySortedSet of I;
attr CPNTS is Colored-PT-net-Family-like means
:: PETRI_3:def 1
for i be Element of I holds CPNTS.i is Colored-PT-net;
end;
registration
let I be non empty set;
cluster Colored-PT-net-Family-like for ManySortedSet of I;
end;
definition
let I be non empty set;
mode Colored-PT-net-Family of I
is Colored-PT-net-Family-like ManySortedSet of I;
end;
definition
let I be non empty set;
let CPNTS be Colored-PT-net-Family of I;
let i be Element of I;
redefine func CPNTS.i -> Colored-PT-net;
end;
definition
let I be non empty set;
let CPNT be Colored-PT-net-Family of I;
attr CPNT is disjoint_valued means
:: PETRI_3:def 2
for i, j be Element of I st i <> j holds
the carrier of (CPNT.i) misses the carrier of (CPNT.j) &
the carrier' of (CPNT.i) misses the carrier' of (CPNT.j);
end;
theorem :: PETRI_3:1
for I be set, F, D, R be ManySortedSet of I st
(for i be object st i in I holds
ex f be Function st f = F.i & dom f = D.i & rng f = R.i) &
(for i,j be object, f,g be Function st i in I & j in I &
i <> j & f = F.i & g = F.j holds dom(f) misses dom(g)) holds
ex G be Function st G = union rng F &
dom G = union rng D & rng G = union rng R &
for i, x be object, f be Function st i in I &
f = F.i & x in dom f
holds G.x = f.x;
theorem :: PETRI_3:2
for I be set, Y, Z be ManySortedSet of I st
(for i, j be object st i in I & j in I &
i <> j holds Y. i /\ Z.j = {})
holds Union (Y (\) Z) = (Union Y) \ (Union Z);
theorem :: PETRI_3:3
for I be set, X, Y, Z be ManySortedSet of I st (X c= (Y (\) Z) &
(for i, j be object st i in I & j in I &
i <> j holds Y.i /\ Z.j = {}))
holds Union(X) c= (Union Y) \ (Union Z);
begin
definition
let I be non trivial set;
func XorDelta(I) -> non empty set equals
:: PETRI_3:def 3
{[i, j] where i,j is Element of I : i <> j};
end;
theorem :: PETRI_3:4
for I be non trivial finite set,
CPNT be Colored-PT-net-Family of I holds
union {Funcs(Outbds(CPNT.i), the carrier of CPNT.j)
where i, j is Element of I : i <> j} is non empty;
definition
let I be non trivial finite set;
let CPNT be Colored-PT-net-Family of I;
mode connecting-mapping of CPNT -> ManySortedSet of XorDelta(I) means
:: PETRI_3:def 4
rng it c= union
{Funcs(Outbds(CPNT.i), the carrier of CPNT.j)
where i, j is Element of I : i <> j} &
for i,j be Element of I st i <> j
holds it.[i, j] is Function of Outbds(CPNT.i), the carrier of CPNT.j;
end;
theorem :: PETRI_3:5
for CPNT1, CPNT2 be Colored-PT-net,
O12 be Function of Outbds(CPNT1), the carrier of CPNT2,
q12 be Function st
dom q12=Outbds(CPNT1) &
for t01 be transition of CPNT1 st t01 is outbound
holds q12.t01 is Function of thin_cylinders(the ColoredSet of CPNT1,
*'{t01}), thin_cylinders(the ColoredSet of CPNT1, Im(O12,t01)) holds
q12 in Funcs(Outbds(CPNT1),
union {Funcs(thin_cylinders(the ColoredSet of CPNT1,*'{t01}),
thin_cylinders(the ColoredSet of CPNT1, Im(O12,t01)))
where t01 is transition of CPNT1:t01 is outbound});
definition
let I be non trivial finite set;
let CPNT be Colored-PT-net-Family of I;
let O be connecting-mapping of CPNT;
mode connecting-firing-rule of O -> ManySortedSet of XorDelta(I) means
:: PETRI_3:def 5
for i, j be Element of I st i <> j holds
ex Oij be Function of Outbds(CPNT.i), the carrier of CPNT.j,
qij be Function st qij =it.[i, j] & Oij = O.[i, j] &
dom (qij)=Outbds(CPNT.i) &
for t01 be transition of CPNT.i
st t01 is outbound holds qij.t01 is
Function of thin_cylinders(the ColoredSet of CPNT.i,
*'{t01}), thin_cylinders(the ColoredSet of CPNT.i, Im(Oij,t01));
end;
begin :: Extension to a family of colored Petri nets
definition
let I be non trivial finite set;
let CPNT be Colored-PT-net-Family of I;
let O be connecting-mapping of CPNT;
let q be connecting-firing-rule of O;
assume
CPNT is disjoint_valued &
for i, j1, j2 be Element of I st i <> j1 & i <> j2 &
(ex x, y1, y2 be object st
[x, y1] in q.[i, j1] & [x, y2] in q.[i, j2]) holds j1 = j2;
func synthesis(q) -> strict Colored-PT-net means
:: PETRI_3:def 6
ex P, T, ST, TS, CS, F be ManySortedSet of I,
UF, UQ be Function st
( for i be Element of I holds
P.i = the carrier of CPNT.i &
T.i = the carrier' of CPNT.i &
ST.i = the S-T_Arcs of CPNT.i &
TS.i = the T-S_Arcs of CPNT.i &
CS.i = the ColoredSet of CPNT.i &
F.i = the firing-rule of CPNT.i ) &
UF = union rng F &
UQ = union rng q &
the carrier of it = union rng P &
the carrier' of it = union rng T &
the S-T_Arcs of it = union rng ST &
the T-S_Arcs of it = (union rng TS ) \/ (union rng O ) &
the ColoredSet of it = union rng CS &
the firing-rule of it = UF +* UQ;
end;
begin :: Definition of Cell Petri nets
definition
let I be non empty finite set;
let CPNT be Colored-PT-net-Family of I;
attr CPNT is Cell-Petri-nets means
:: PETRI_3:def 7
ex N be Function of I, bool rng CPNT st
for i be Element of I holds
N.i = {CPNT.j where j is Element of I:j <> i};
end;
definition
let I be non trivial finite set;
let CPNT be Colored-PT-net-Family of I;
let N be Function of I,bool (rng CPNT);
let O be connecting-mapping of CPNT;
pred N, O is_Cell-Petri-nets means
:: PETRI_3:def 8
for i be Element of I holds
N.i = {CPNT.j where j is Element of I:j <> i &
ex t be transition of CPNT.i,
s be object st [t, s] in O.[i, j]};
end;
theorem :: PETRI_3:6
::Th3:
for I be non trivial finite set,
CPNT be Colored-PT-net-Family of I,
N be Function of I, bool rng CPNT,
O be connecting-mapping of CPNT st CPNT is one-to-one &
N, O is_Cell-Petri-nets holds
for i be Element of I holds not CPNT.i in N.i;
begin :: Activation of Petri nets
:: non empty non void with_S-T_arc with_T-S_arc Colored_PT_net_Str;
definition let CPN be Colored_PT_net_Str;
attr CPN is with-nontrivial-ColoredSet means
:: PETRI_3:def 9
the ColoredSet of CPN is non trivial;
end;
registration
cluster with-nontrivial-ColoredSet for
strict Colored-PT-net-like Colored_Petri_net;
end;
registration
let CPNT be with-nontrivial-ColoredSet Colored-PT-net;
cluster the ColoredSet of CPNT -> non trivial;
end;
::Def13:: color-threshold
definition
let CPN be with-nontrivial-ColoredSet Colored-PT-net;
let S be Subset of the carrier of CPN;
let D be thin_cylinder of the ColoredSet of CPN, S;
mode color-threshold of D is Function of loc(D), the ColoredSet of CPN;
end;
:: color-count of CPN
definition
let CPN be Colored-PT-net;
mode color-count of CPN is Function of the ColoredSet of CPN, NAT;
end;
:: Colored-states of CPN
definition
let CPN be Colored-PT-net;
func Colored-states(CPN) -> non empty set equals
:: PETRI_3:def 10
the set of all e where e is color-count of CPN;
end;
:: colored-state of CPN
definition
let CPN be Colored-PT-net;
mode colored-state of CPN is Function of CPN, Colored-states(CPN);
end;
reserve CPN for with-nontrivial-ColoredSet Colored-PT-net;
reserve m for colored-state of CPN;
reserve t for Element of the carrier' of CPN;
definition
let CPN be with-nontrivial-ColoredSet Colored-PT-net,
m be colored-state of CPN;
let p be place of CPN;
redefine func m.p -> color-count of CPN;
end;
definition
let CPN be with-nontrivial-ColoredSet Colored-PT-net;
let mp be color-count of CPN;
let x be object;
redefine func mp.x -> Element of NAT;
end;
:: q-firable on m
definition
let CPN, m, t;
let D being thin_cylinder of the ColoredSet of CPN, *'{t};
let ColD being color-threshold of D;
pred t is_firable_on m,ColD means
:: PETRI_3:def 11
:: :Def14:
(the firing-rule of CPN). [t, D] <> {} &
for p being place of CPN st p in loc(D) holds 1 <= (m.p).(ColD.p);
end;
:: q-firable set on t
definition
let CPN,m,t;
func firable_set_on(m,t) -> set equals
:: PETRI_3:def 12
:: :Def15:
{D where D is thin_cylinder of the ColoredSet of CPN, *'{t}:
ex ColD being color-threshold of D st t is_firable_on m, ColD};
end;
:: t is q-firable on m iff q-firable set on t, m
theorem :: PETRI_3:7
:: Th4:
for D being thin_cylinder of the ColoredSet of CPN, *'{t} holds
(ex ColD being color-threshold of D st t is_firable_on m, ColD)
iff
D in firable_set_on(m, t);
:: The definition of mapping Ptr_Sub
definition
let CPN, m, t;
let D be thin_cylinder of the ColoredSet of CPN, *'{t};
let ColD be color-threshold of D;
let p be Element of CPN;
assume
t is_firable_on m, ColD;
func Ptr_Sub(ColD, m, p) ->
Function of the ColoredSet of CPN, NAT means
:: PETRI_3:def 13
for x be Element of the ColoredSet of CPN holds
((p in loc(D) & x = ColD.p) implies it.x = (m.p).x - 1) &
(not (p in loc(D) & x = ColD.p) implies it.x = (m.p).x);
end;
:: The definition of mapping Ptr_Add
definition
let CPN, m, t;
let D be thin_cylinder of the ColoredSet of CPN, {t}*';
let ColD be color-threshold of D;
let p be Element of CPN;
func Ptr_Add(ColD, m, p) -> Function of the ColoredSet of CPN, NAT means
:: PETRI_3:def 14
for x be Element of the ColoredSet of CPN holds
((p in loc(D) & x = ColD.p) implies it.x = (m.p).x + 1) &
(not (p in loc(D) & x = ColD.p) implies it.x = (m.p).x);
end;
:: The definition of firing_result
definition
let CPN, m, t;
let D be thin_cylinder of the ColoredSet of CPN, *'{t};
let E be thin_cylinder of the ColoredSet of CPN, {t}*';
let ColD be color-threshold of D;
let ColE be color-threshold of E;
let p be Element of CPN;
func firing_result(ColD, ColE, m, p) ->
Function of the ColoredSet of CPN, NAT equals
:: PETRI_3:def 15
Ptr_Sub(ColD,m,p) if t is_firable_on m,ColD &
p in loc(D) \ loc(E),
Ptr_Add(ColE,m,p) if t is_firable_on m,ColD &
p in loc(E)\loc(D)
otherwise m.p;
end;
:: The definition of the range of firing_result
theorem :: PETRI_3:8
:::Th5A:
for D0 being thin_cylinder of the ColoredSet of CPN, *'{t},
D1 being thin_cylinder of the ColoredSet of CPN, {t}*',
ColD0 be color-threshold of D0,
ColD1 be color-threshold of D1,
x be Element of the ColoredSet of CPN,
p be Element of CPN holds
(m.p).x - 1 <= (firing_result(ColD0, ColD1, m, p)).x &
(firing_result(ColD0, ColD1, m, p)).x <= (m.p).x + 1;
theorem :: PETRI_3:9
:: :Th5B:
for D0 being thin_cylinder of the ColoredSet of CPN, *'{t},
D1 being thin_cylinder of the ColoredSet of CPN, {t}*',
ColD0 be color-threshold of D0,
ColD1 be color-threshold of D1,
x be Element of the ColoredSet of CPN,
p be Element of CPN st
t is outbound holds
(m.p).x - 1 <= (firing_result(ColD0, ColD1, m, p)).x &
(firing_result(ColD0, ColD1, m, p)).x <= (m.p).x;