:: Cell Petri Net Concepts
:: by Mitsuru Jitsukawa, Pauline N. Kawamoto, Yasunari Shidama,
:: and Yatsuka Nakamura
::
:: Received October 14, 2008
:: Copyright (c) 2008-2019 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, FUNCT_1, XBOOLE_0, TARSKI, SUBSET_1, FUNCT_2, RELAT_1,
FUNCOP_1, FUNCT_4, FINSET_1, SETFAM_1, ZFMISC_1, PARTFUN1, ARYTM_3,
CARD_1, PETRI_2, STRUCT_0;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ZFMISC_1, SETFAM_1, RELAT_1,
RELSET_1, DOMAIN_1, PETRI, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, RELSET_2,
FINSET_1, FUNCOP_1, ORDINAL1, CARD_1, PARTIT_2, STRUCT_0;
constructors RELSET_1, DOMAIN_1, PETRI, RELSET_2, FUNCT_4, PARTIT_2, FUNCOP_1;
registrations SUBSET_1, RELAT_1, PARTFUN1, RELSET_1, XBOOLE_0, FUNCT_2,
FINSET_1, STRUCT_0, FUNCT_1, PETRI, ZFMISC_1;
requirements SUBSET, BOOLE;
begin :: Preliminaries: thin cylinder, locus
definition
let A be non empty set, B be set;
let Bo be set, yo be Function of Bo,A;
assume
Bo c= B;
func cylinder0(A,B,Bo,yo) -> non empty Subset of Funcs(B,A) equals
:: PETRI_2:def 1
{ y where y is Function of B,A : y|Bo = yo };
end;
definition
let A be non empty set, B be set;
mode thin_cylinder of A,B -> non empty Subset of Funcs(B,A) means
:: PETRI_2:def 2
ex
Bo being Subset of B,yo being Function of Bo,A st Bo is finite & it = cylinder0
(A,B,Bo,yo);
end;
theorem :: PETRI_2:1
for A be non empty set, B be set, D be thin_cylinder of A,B holds
ex Bo being Subset of B,yo being Function of Bo,A st Bo is finite & D = { y
where y is Function of B,A : y|Bo = yo };
theorem :: PETRI_2:2
for A1,A2 be non empty set, B be set, D1 be thin_cylinder of A1,B st
A1 c= A2 ex D2 be thin_cylinder of A2,B st D1 c= D2;
definition
let A be non empty set, B be set;
func thin_cylinders(A,B) -> non empty Subset-Family of Funcs(B,A) equals
:: PETRI_2:def 3
{D
where D is Subset of Funcs(B,A) : D is thin_cylinder of A,B};
end;
theorem :: PETRI_2:3
for A be non trivial set, B be set, Bo1 be set, yo1 being
Function of Bo1,A, Bo2 be set, yo2 being Function of Bo2,A st Bo1 c= B & Bo2 c=
B & cylinder0(A,B,Bo1,yo1) = cylinder0(A,B,Bo2,yo2) holds Bo1=Bo2 & yo1=yo2;
theorem :: PETRI_2:4
for A1,A2 be non empty set, B1,B2 be set st A1 c= A2 & B1 c= B2
ex F be Function of thin_cylinders(A1,B1), thin_cylinders(A2,B2) st for x be
set st x in thin_cylinders(A1,B1) ex Bo being Subset of B1, yo1 being Function
of Bo,A1, yo2 being Function of Bo,A2 st Bo is finite & yo1=yo2 & x=cylinder0(
A1,B1,Bo,yo1) & F.x=cylinder0(A2,B2,Bo,yo2);
theorem :: PETRI_2:5
for A1,A2 be non empty set, B1,B2 be set ex G be Function of
thin_cylinders(A2,B2), thin_cylinders(A1,B1) st for x be set st x in
thin_cylinders(A2,B2) ex Bo2 being Subset of B2,Bo1 being Subset of B1, yo1
being Function of Bo1,A1, yo2 being Function of Bo2,A2 st Bo1 is finite & Bo2
is finite & Bo1=B1 /\ Bo2 /\ (yo2"A1) & yo1=yo2 | Bo1 & x= cylinder0(A2,B2,Bo2,
yo2) & G.x =cylinder0(A1,B1,Bo1,yo1);
definition
let A1,A2 be non trivial set, B1,B2 be set;
assume that
A1 c= A2 and
B1 c= B2;
func Extcylinders(A1,B1,A2,B2) -> Function of thin_cylinders(A1,B1),
thin_cylinders(A2,B2) means
:: PETRI_2:def 4
for x be set st x in thin_cylinders(A1,B1) ex Bo
being Subset of B1, yo1 being Function of Bo,A1, yo2 being Function of Bo,A2 st
Bo is finite & yo1=yo2 & x=cylinder0(A1,B1,Bo,yo1) & it.x=cylinder0(A2,B2,Bo,
yo2);
end;
definition
let A1 be non empty set, A2 be non trivial set, B1,B2 be set;
func Ristcylinders(A1,B1,A2,B2) -> Function of thin_cylinders(A2,B2),
thin_cylinders(A1,B1) means
:: PETRI_2:def 5
for x be set st x in thin_cylinders(A2,B2) ex Bo2
being Subset of B2,Bo1 being Subset of B1, yo1 being Function of Bo1,A1, yo2
being Function of Bo2,A2 st Bo1 is finite & Bo2 is finite & Bo1=B1 /\ Bo2 /\ (
yo2"A1) & yo1=yo2 | Bo1 & x = cylinder0(A2,B2,Bo2,yo2) & it.x =cylinder0(A1,B1,
Bo1,yo1);
end;
definition
let A be non trivial set,B be set;
let D be thin_cylinder of A,B;
func loc(D) -> finite Subset of B means
:: PETRI_2:def 6
ex Bo being Subset of B,yo being
Function of Bo,A st Bo is finite & D = { y where y is Function of B,A : y|Bo =
yo } & it = Bo;
end;
begin :: Colored Petri nets
definition
let A1,A2 be non trivial set, B1,B2 be set;
let C1,C2 be non trivial set, D1,D2 be set;
let F be Function of thin_cylinders(A1,B1), thin_cylinders(C1,D1);
func CylinderFunc(A1,B1,A2,B2,C1,D1,C2,D2,F) -> Function of thin_cylinders(
A2,B2), thin_cylinders(C2,D2) equals
:: PETRI_2:def 7
Extcylinders(C1,D1,C2,D2)*F*Ristcylinders(
A1,B1,A2,B2);
end;
definition
struct (PT_net_Str) Colored_PT_net_Str (# carrier, carrier' ->
set, S-T_Arcs -> Relation of the carrier,the carrier', T-S_Arcs ->
Relation of the carrier', the carrier, ColoredSet -> non empty
finite set, firing-rule -> Function #);
end;
definition
func TrivialColoredPetriNet -> Colored_PT_net_Str equals
:: PETRI_2:def 8
Colored_PT_net_Str (# {{}}, {{}}, [#]({{}},{{}}), [#]({{}},
{{}}), {{}}, {} #);
end;
registration
cluster TrivialColoredPetriNet
-> with_S-T_arc with_T-S_arc non empty non void;
end;
registration
cluster non empty non void with_S-T_arc with_T-S_arc for Colored_PT_net_Str;
end;
definition
mode Colored_Petri_net
is non empty non void with_S-T_arc with_T-S_arc Colored_PT_net_Str;
end;
definition
let CPNT be Colored_Petri_net;
let t0 be transition of CPNT;
attr t0 is outbound means
:: PETRI_2:def 9
{t0}*' = {};
end;
definition
let CPNT1 be Colored_Petri_net;
func Outbds(CPNT1) -> Subset of the carrier' of CPNT1 equals
:: PETRI_2:def 10
{x where x
is transition of CPNT1 : x is outbound };
end;
definition
let CPNT be Colored_Petri_net;
attr CPNT is Colored-PT-net-like means
:: PETRI_2:def 11
dom (the firing-rule of CPNT)
c= (the carrier' of CPNT) \ Outbds(CPNT) & for t being transition of CPNT st
t in dom (the firing-rule of CPNT) holds ex CS be non empty Subset of the
ColoredSet of CPNT, I be Subset of *'{t}, O be Subset of {t}*' st (the
firing-rule of CPNT ).t is Function of thin_cylinders(CS,I), thin_cylinders(CS,
O);
end;
theorem :: PETRI_2:6
for CPNT be Colored_Petri_net, t being transition of CPNT st CPNT is
Colored-PT-net-like & t in dom (the firing-rule of CPNT) holds ex CS be non
empty Subset of the ColoredSet of CPNT, I be Subset of *'{t}, O be Subset of {t
}*' st (the firing-rule of CPNT ).t is Function of thin_cylinders(CS,I),
thin_cylinders(CS,O);
theorem :: PETRI_2:7
for CPNT1,CPNT2 be Colored_Petri_net, t1 be transition of CPNT1,
t2 be transition of CPNT2 st the carrier of CPNT1 c= the carrier of CPNT2
& the
S-T_Arcs of CPNT1 c= the S-T_Arcs of CPNT2 & the T-S_Arcs of CPNT1 c= the
T-S_Arcs of CPNT2 & t1=t2 holds *'{t1} c= *'{t2} & {t1}*' c= {t2}*';
registration
cluster strict Colored-PT-net-like for Colored_Petri_net;
end;
definition
mode Colored-PT-net is Colored-PT-net-like Colored_Petri_net;
end;
begin :: Outbound transitions of CPNT
definition
let CPNT1, CPNT2 be Colored_Petri_net;
pred CPNT1 misses CPNT2 means
:: PETRI_2:def 12
(the carrier of CPNT1) /\ (the carrier
of CPNT2 ) = {} & (the carrier' of CPNT1) /\ (the carrier' of CPNT2) = {};
symmetry;
end;
begin :: Connecting mapping for CPNT1,CPNT2
definition
let CPNT1 be Colored_Petri_net;
let CPNT2 be Colored_Petri_net;
mode connecting-mapping of CPNT1,CPNT2 -> set means
:: PETRI_2:def 13
ex O12 be Function of
Outbds(CPNT1), the carrier of CPNT2, O21 be Function of Outbds(CPNT2), the
carrier of CPNT1 st it=[O12,O21];
end;
begin :: Connecting firing rule for CPNT1,CPNT2
definition
let CPNT1, CPNT2 be Colored-PT-net;
let O be connecting-mapping of CPNT1,CPNT2;
mode connecting-firing-rule of CPNT1,CPNT2,O -> set means
:: PETRI_2:def 14
ex q12,q21 be
Function, O12 be Function of Outbds(CPNT1), the carrier of CPNT2, O21 be
Function of Outbds(CPNT2), the carrier of CPNT1 st O=[O12,O21] &
dom q12=Outbds(
CPNT1) & dom q21=Outbds(CPNT2) & ( 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) ) ) & ( for t02
be transition of CPNT2 st t02 is outbound holds q21.t02 is Function of
thin_cylinders (the ColoredSet of CPNT2, *'{t02}), thin_cylinders (the
ColoredSet of CPNT2, Im(O21,t02) ) ) & it=[q12,q21];
end;
begin :: Synthesis of CPNT1,CPNT2
definition
let CPNT1, CPNT2 be Colored-PT-net;
let O be connecting-mapping of CPNT1,CPNT2;
let q be connecting-firing-rule of CPNT1,CPNT2,O;
assume
CPNT1 misses CPNT2;
func synthesis(CPNT1, CPNT2,O,q) -> strict Colored-PT-net means
:: PETRI_2:def 15
ex q12,q21
be Function, O12 be Function of Outbds(CPNT1), the carrier of CPNT2, O21 be
Function of Outbds(CPNT2), the carrier of CPNT1 st O=[O12,O21] &
dom q12=Outbds(
CPNT1) & dom q21=Outbds(CPNT2) & ( 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) ) ) & ( for t02
be transition of CPNT2 st t02 is outbound holds q21.t02 is Function of
thin_cylinders ( the ColoredSet of CPNT2, *'{t02}), thin_cylinders ( the
ColoredSet of CPNT2, Im(O21,t02) ) ) & q=[q12,q21] & the carrier of it = (the
carrier of CPNT1) \/ (the carrier of CPNT2) & the carrier' of it = (the
carrier' of CPNT1) \/ (the carrier' of CPNT2) & the S-T_Arcs of it = (the
S-T_Arcs of CPNT1) \/ (the S-T_Arcs of CPNT2) & the T-S_Arcs of it = (the
T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2) \/ O12 \/ O21 & the ColoredSet of
it = (the ColoredSet of CPNT1) \/ (the ColoredSet of CPNT2) & the firing-rule
of it = (the firing-rule of CPNT1) +* (the firing-rule of CPNT2) +* q12 +* q21;
end;