PETRI_3: Formulation of Cell Petri Nets

:: Formulation of Cell Petri Nets
:: by Mitsuru Jitsukawa , Pauline N. Kawamoto and Yasunari Shidama
::
:: Received December 8, 2013
:: Copyright (c) 2013-2021 Association of Mizar Users

definition

let I be non empty set ;
let CPNTS be ManySortedSet of I;

attr CPNTS is Colored-PT-net-Family-like means :Def11a: :: PETRI_3:def 1
for i being Element of I holds CPNTS . i is Colored-PT-net;

end;

:: deftheorem Def11a defines Colored-PT-net-Family-like PETRI_3:def 1 :

registration

let I be non empty set ;

cluster non empty Relation-like I -defined Function-like V17(I) Colored-PT-net-Family-like for set ;

existence

proof end;

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;
:: original: .
redefine func CPNTS . i -> Colored-PT-net;
correctness by Def11a;

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

:: deftheorem defines disjoint_valued PETRI_3:def 2 :

theorem LM01: :: PETRI_3:1

for I being set
for F, D, R being ManySortedSet of I st ( for i being object st i in I holds
ex f being Function st
( f = F . i & dom f = D . i & rng f = R . i ) ) & ( for i, j being object
for f, g being 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 being Function st
( G = union (rng F) & dom G = union (rng D) & rng G = union (rng R) & ( for i, x being object
for f being Function st i in I & f = F . i & x in dom f holds
G . x = f . x ) )

proof end;

theorem LM03: :: PETRI_3:2

for I being set
for Y, Z being ManySortedSet of I st ( for i, j being object st i in I & j in I & i <> j holds
(Y . i) /\ (Z . j) = {} ) holds
Union (Y (\) Z) = (Union Y) \ (Union Z)

proof end;

theorem LM04: :: PETRI_3:3

for I being set
for X, Y, Z being ManySortedSet of I st X c= Y (\) Z & ( for i, j being object st i in I & j in I & i <> j holds
(Y . i) /\ (Z . j) = {} ) holds
Union X c= (Union Y) \ (Union Z)

proof end;

LMXorDelta: for I being non trivial set ex i, j being Element of I st i <> j

proof end;

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

correctness

proof end;

end;

:: deftheorem defines XorDelta PETRI_3:def 3 :

theorem SYLM2: :: PETRI_3:4

for I being non trivial finite set
for CPNT being Colored-PT-net-Family of I holds not union { (Funcs ((Outbds (CPNT . i)), the carrier of (CPNT . j))) where i, j is Element of I : i <> j } is empty

proof end;

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 :Defcntmap: :: 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 being Element of I st i <> j holds
it . [i,j] is Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ) );

existence

proof end;

end;

:: deftheorem Defcntmap defines connecting-mapping PETRI_3:def 4 :

theorem SYLM3: :: PETRI_3:5

for CPNT1, CPNT2 being Colored-PT-net
for O12 being Function of (Outbds CPNT1), the carrier of CPNT2
for q12 being Function st dom q12 = Outbds CPNT1 & ( for t01 being 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 } ))

proof end;

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 :Defcntfir: :: PETRI_3:def 5
for i, j being Element of I st i <> j holds
ex Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ex qij being Function st
( qij = it . [i,j] & Oij = O . [i,j] & dom qij = Outbds (CPNT . i) & ( for t01 being 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)))) ) );

existence

proof end;

end;

:: deftheorem Defcntfir defines connecting-firing-rule PETRI_3:def 5 :

LMQ1: for I being non trivial finite set
for CPNT being Colored-PT-net-Family of I st CPNT is disjoint_valued holds
for O being connecting-mapping of CPNT
for q being connecting-firing-rule of O st ( for i, j1, j2 being Element of I st i <> j1 & i <> j2 & ex x, y1, y2 being object st
( [x,y1] in q . [i,j1] & [x,y2] in q . [i,j2] ) holds
j1 = j2 ) holds
( union (rng q) is Function & ( for z being object st z in union (rng q) holds
ex i, j being Element of I ex q12 being Function ex O12 being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) st
( i <> j & ( for t01 being transition of (CPNT . i) st t01 is outbound holds
q12 . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))) ) & q12 in Funcs ((Outbds (CPNT . i)),(union { (Funcs ((thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (O12,t01)))))) where t01 is transition of (CPNT . i) : t01 is outbound } )) & q12 = q . [i,j] & O12 = O . [i,j] & z in q12 ) ) )

proof end;

LMQ1A: for I being non trivial finite set
for CPNT being Colored-PT-net-Family of I
for O being connecting-mapping of CPNT
for q being connecting-firing-rule of O
for F being Function st F = union (rng q) holds
for g being Function
for x being object
for i, j being Element of I st i <> j & g = q . [i,j] & x in dom g holds
F . x = g . x

proof end;

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 AS: ( CPNT is disjoint_valued & ( for i, j1, j2 being Element of I st i <> j1 & i <> j2 & ex x, y1, y2 being 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 being ManySortedSet of I ex UF, UQ being Function st
( ( for i being 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 );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines synthesis PETRI_3:def 6 :

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 being Function of I,(bool (rng CPNT)) st
for i being Element of I holds N . i = { (CPNT . j) where j is Element of I : j <> i } ;

end;

:: deftheorem defines Cell-Petri-nets PETRI_3:def 7 :

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 being Element of I holds N . i = { (CPNT . j) where j is Element of I : ( j <> i & ex t being transition of (CPNT . i) ex s being object st [t,s] in O . [i,j] ) } ;

end;

:: deftheorem defines is_Cell-Petri-nets PETRI_3:def 8 :

theorem :: PETRI_3:6

for I being non trivial finite set
for CPNT being Colored-PT-net-Family of I
for N being Function of I,(bool (rng CPNT))
for O being connecting-mapping of CPNT st CPNT is one-to-one & N,O is_Cell-Petri-nets holds
for i being Element of I holds not CPNT . i in N . i

proof end;

:: non empty non void with_S-T_arc with_T-S_arc Colored_PT_net_Str;

definition

let CPN be Colored_PT_net_Str ;

:: non empty non void with_S-T_arc with_T-S_arc Colored_PT_net_Str;

attr CPN is with-nontrivial-ColoredSet means :defnontrivial: :: PETRI_3:def 9
not the ColoredSet of CPN is trivial ;

end;

:: deftheorem defnontrivial defines with-nontrivial-ColoredSet PETRI_3:def 9 :

registration

cluster non empty non void V84() with_S-T_arc with_T-S_arc strict Colored-PT-net-like with-nontrivial-ColoredSet for Colored_PT_net_Str ;

existence

proof end;

end;

registration

let CPNT be with-nontrivial-ColoredSet Colored-PT-net;

cluster the ColoredSet of CPNT -> non trivial ;

correctness by defnontrivial;

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
{ e where e is color-count of CPN : verum } ;

coherence

proof end;

end;

:: deftheorem defines Colored-states PETRI_3:def 10 :

:: colored-state of CPN

definition

let CPN be Colored-PT-net;
mode colored-state of CPN is Function of CPN,(Colored-states CPN);

end;

definition

let CPN be with-nontrivial-ColoredSet Colored-PT-net;
let m be colored-state of CPN;
let p be place of CPN;
:: original: .
redefine func m . p -> color-count of CPN;
correctness

proof end;

end;

definition

let CPN be with-nontrivial-ColoredSet Colored-PT-net;
let mp be color-count of CPN;
let x be object ;
:: original: .
redefine func mp . x -> Element of NAT ;
correctness

proof end;

end;

:: q-firable on m

definition

:: :Def14:

pred t is_firable_on m,ColD means :: PETRI_3:def 11
( 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;

:: deftheorem defines is_firable_on PETRI_3:def 11 :

:: q-firable set on t

definition

let CPN be with-nontrivial-ColoredSet Colored-PT-net;
let m be colored-state of CPN;
let t be Element of the carrier' of CPN;

:: :Def15:

func firable_set_on (m,t) -> set equals :: PETRI_3:def 12
{ 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 } ;

coherence ;

end;

:: deftheorem defines firable_set_on PETRI_3:def 12 :

:: t is q-firable on m iff q-firable set on t, m

theorem :: PETRI_3:7

for CPN being with-nontrivial-ColoredSet Colored-PT-net
for m being colored-state of CPN
for t being Element of the carrier' of CPN
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) )

proof end;

:: The definition of mapping Ptr_Sub

definition

let CPN be with-nontrivial-ColoredSet Colored-PT-net;
let m be colored-state of CPN;
let t be Element of the carrier' of CPN;
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 AS1: t is_firable_on m,ColD ;

func Ptr_Sub (ColD,m,p) -> Function of the ColoredSet of CPN,NAT means :Def16Sub: :: PETRI_3:def 13
for x being 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 or not x = ColD . p ) implies it . x = (m . p) . x ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16Sub defines Ptr_Sub PETRI_3:def 13 :

:: The definition of mapping Ptr_Add

definition

let CPN be with-nontrivial-ColoredSet Colored-PT-net;
let m be colored-state of CPN;
let t be Element of the carrier' of CPN;
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 :Def16Add: :: PETRI_3:def 14
for x being 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 or not x = ColD . p ) implies it . x = (m . p) . x ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16Add defines Ptr_Add PETRI_3:def 14 :

:: The definition of firing_result

definition

let CPN be with-nontrivial-ColoredSet Colored-PT-net;
let m be colored-state of CPN;
let t be Element of the carrier' of CPN;
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 :Def16: :: 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;

coherence ;
consistency

proof end;

end;

:: deftheorem Def16 defines firing_result PETRI_3:def 15 :

:: The definition of the range of firing_result

theorem :: PETRI_3:8

for CPN being with-nontrivial-ColoredSet Colored-PT-net
for m being colored-state of CPN
for t being Element of the carrier' of CPN
for D0 being thin_cylinder of the ColoredSet of CPN, *' {t}
for D1 being thin_cylinder of the ColoredSet of CPN,{t} *'
for ColD0 being color-threshold of D0
for ColD1 being color-threshold of D1
for x being Element of the ColoredSet of CPN
for p being 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 )

proof end;

theorem :: PETRI_3:9

for CPN being with-nontrivial-ColoredSet Colored-PT-net
for m being colored-state of CPN
for t being Element of the carrier' of CPN
for D0 being thin_cylinder of the ColoredSet of CPN, *' {t}
for D1 being thin_cylinder of the ColoredSet of CPN,{t} *'
for ColD0 being color-threshold of D0
for ColD1 being color-threshold of D1
for x being Element of the ColoredSet of CPN
for p being 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 )

proof end;