:: by Mitsuru Jitsukawa , Pauline N. Kawamoto and Yasunari Shidama

::

:: Received December 8, 2013

:: Copyright (c) 2013-2017 Association of Mizar Users

definition

let I be non empty set ;

let CPNTS be ManySortedSet of I;

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

for i being Element of I holds CPNTS . i is Colored-PT-net;

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

for I being non empty set

for CPNTS being ManySortedSet of I holds

( CPNTS is Colored-PT-net-Family-like iff for i being Element of I holds CPNTS . i is Colored-PT-net );

for I being non empty set

for CPNTS being ManySortedSet of I holds

( CPNTS is Colored-PT-net-Family-like iff for i being Element of I holds CPNTS . i is Colored-PT-net );

registration

let I be non empty set ;

ex b_{1} being ManySortedSet of I st b_{1} is Colored-PT-net-Family-like

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

existence ex b

proof 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;
mode Colored-PT-net-Family of I is Colored-PT-net-Family-like ManySortedSet of I;

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

coherence

CPNTS . i is Colored-PT-net;

by Def11a;

end;
let CPNTS be Colored-PT-net-Family of I;

let i be Element of I;

:: original: .

redefine func CPNTS . i -> Colored-PT-net;

correctness

coherence

CPNTS . i is Colored-PT-net;

by Def11a;

:: deftheorem defines disjoint_valued PETRI_3:def 2 :

for I being non empty set

for CPNT being Colored-PT-net-Family of I holds

( CPNT is disjoint_valued iff 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) ) );

for I being non empty set

for CPNT being Colored-PT-net-Family of I holds

( CPNT is disjoint_valued iff 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) ) );

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

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)

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)

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 ;

coherence

{ [i,j] where i, j is Element of I : i <> j } is non empty set ;

end;
func XorDelta I -> non empty set equals :: PETRI_3:def 3

{ [i,j] where i, j is Element of I : i <> j } ;

correctness { [i,j] where i, j is Element of I : i <> j } ;

coherence

{ [i,j] where i, j is Element of I : i <> j } is non empty set ;

proof end;

:: deftheorem defines XorDelta PETRI_3:def 3 :

for I being non trivial set holds XorDelta I = { [i,j] where i, j is Element of I : i <> j } ;

for I being non trivial set holds XorDelta I = { [i,j] where i, j is Element of I : i <> j } ;

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

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;

ex b_{1} being ManySortedSet of XorDelta I st

( rng b_{1} 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

b_{1} . [i,j] is Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ) )

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

ex b

( rng b

b

proof end;

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

for I being non trivial finite set

for CPNT being Colored-PT-net-Family of I

for b_{3} being ManySortedSet of XorDelta I holds

( b_{3} is connecting-mapping of CPNT iff ( rng b_{3} 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

b_{3} . [i,j] is Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ) ) );

for I being non trivial finite set

for CPNT being Colored-PT-net-Family of I

for b

( b

b

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

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;

ex b_{1} being ManySortedSet of XorDelta I st

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 = b_{1} . [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)))) ) )

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

ex b

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

qij . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) )

proof end;

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

for I being non trivial finite set

for CPNT being Colored-PT-net-Family of I

for O being connecting-mapping of CPNT

for b_{4} being ManySortedSet of XorDelta I holds

( b_{4} is connecting-firing-rule of O iff 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 = b_{4} . [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)))) ) ) );

for I being non trivial finite set

for CPNT being Colored-PT-net-Family of I

for O being connecting-mapping of CPNT

for b

( b

ex Oij being Function of (Outbds (CPNT . i)), the carrier of (CPNT . j) ex qij being Function st

( qij = b

qij . t01 is Function of (thin_cylinders ( the ColoredSet of (CPNT . i),(*' {t01}))),(thin_cylinders ( the ColoredSet of (CPNT . i),(Im (Oij,t01)))) ) ) );

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

ex b_{1} being strict Colored-PT-net 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 b_{1} = union (rng P) & the carrier' of b_{1} = union (rng T) & the S-T_Arcs of b_{1} = union (rng ST) & the T-S_Arcs of b_{1} = (union (rng TS)) \/ (union (rng O)) & the ColoredSet of b_{1} = union (rng CS) & the firing-rule of b_{1} = UF +* UQ )

for b_{1}, b_{2} being strict Colored-PT-net st 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 b_{1} = union (rng P) & the carrier' of b_{1} = union (rng T) & the S-T_Arcs of b_{1} = union (rng ST) & the T-S_Arcs of b_{1} = (union (rng TS)) \/ (union (rng O)) & the ColoredSet of b_{1} = union (rng CS) & the firing-rule of b_{1} = UF +* UQ ) & 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 b_{2} = union (rng P) & the carrier' of b_{2} = union (rng T) & the S-T_Arcs of b_{2} = union (rng ST) & the T-S_Arcs of b_{2} = (union (rng TS)) \/ (union (rng O)) & the ColoredSet of b_{2} = union (rng CS) & the firing-rule of b_{2} = UF +* UQ ) holds

b_{1} = b_{2}

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

ex b

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

proof end;

uniqueness for b

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

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

b

proof end;

:: deftheorem defines synthesis PETRI_3:def 6 :

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 st 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 ) holds

for b_{5} being strict Colored-PT-net holds

( b_{5} = synthesis q iff 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 b_{5} = union (rng P) & the carrier' of b_{5} = union (rng T) & the S-T_Arcs of b_{5} = union (rng ST) & the T-S_Arcs of b_{5} = (union (rng TS)) \/ (union (rng O)) & the ColoredSet of b_{5} = union (rng CS) & the firing-rule of b_{5} = UF +* UQ ) );

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 st 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 ) holds

for b

( b

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

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

for I being non empty finite set

for CPNT being Colored-PT-net-Family of I holds

( CPNT is Cell-Petri-nets iff 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 } );

for I being non empty finite set

for CPNT being Colored-PT-net-Family of I holds

( CPNT is Cell-Petri-nets iff 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 } );

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;

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

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

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 holds

( N,O is_Cell-Petri-nets iff 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] ) } );

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 holds

( N,O is_Cell-Petri-nets iff 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] ) } );

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

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 ;

end;
attr CPN is with-nontrivial-ColoredSet means :defnontrivial: :: PETRI_3:def 9

not the ColoredSet of CPN is trivial ;

not the ColoredSet of CPN is trivial ;

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

for CPN being Colored_PT_net_Str holds

( CPN is with-nontrivial-ColoredSet iff not the ColoredSet of CPN is trivial );

for CPN being Colored_PT_net_Str holds

( CPN is with-nontrivial-ColoredSet iff not the ColoredSet of CPN is trivial );

registration

ex b_{1} being strict Colored-PT-net-like Colored_Petri_net st b_{1} is with-nontrivial-ColoredSet
end;

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

proof end;

registration

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

correctness

coherence

not the ColoredSet of CPNT is trivial ;

by defnontrivial;

end;
correctness

coherence

not the ColoredSet of CPNT is trivial ;

by defnontrivial;

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

:: color-count of CPN

definition
end;

:: Colored-states of CPN

definition

let CPN be Colored-PT-net;

{ e where e is color-count of CPN : verum } is non empty set

end;
func Colored-states CPN -> non empty set equals :: PETRI_3:def 10

{ e where e is color-count of CPN : verum } ;

coherence { e where e is color-count of CPN : verum } ;

{ e where e is color-count of CPN : verum } is non empty set

proof end;

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

for CPN being Colored-PT-net holds Colored-states CPN = { e where e is color-count of CPN : verum } ;

for CPN being Colored-PT-net holds Colored-states CPN = { e where e is color-count of CPN : verum } ;

:: colored-state of CPN

definition
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

coherence

m . p is color-count of CPN;

end;
let m be colored-state of CPN;

let p be place of CPN;

:: original: .

redefine func m . p -> color-count of CPN;

correctness

coherence

m . p is color-count of CPN;

proof 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

coherence

mp . x is Element of NAT ;

end;
let mp be color-count of CPN;

let x be object ;

:: original: .

redefine func mp . x -> Element of NAT ;

correctness

coherence

mp . x is Element of NAT ;

proof end;

:: q-firable on m

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;

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

:: :Def14:

:: deftheorem defines is_firable_on PETRI_3:def 11 :

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}

for ColD being color-threshold of D holds

( t is_firable_on m,ColD iff ( the firing-rule of CPN . [t,D] <> {} & ( for p being place of CPN st p in loc D holds

1 <= (m . p) . (ColD . p) ) ) );

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}

for ColD being color-threshold of D holds

( t is_firable_on m,ColD iff ( the firing-rule of CPN . [t,D] <> {} & ( for p being place of CPN st p in loc D holds

1 <= (m . p) . (ColD . p) ) ) );

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

{ 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 } is set ;

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

{ 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 } is set ;

:: deftheorem defines firable_set_on PETRI_3:def 12 :

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 holds firable_set_on (m,t) = { 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 } ;

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 holds firable_set_on (m,t) = { 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 } ;

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

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 ;

ex b_{1} being Function of the ColoredSet of CPN,NAT st

for x being Element of the ColoredSet of CPN holds

( ( p in loc D & x = ColD . p implies b_{1} . x = ((m . p) . x) - 1 ) & ( ( not p in loc D or not x = ColD . p ) implies b_{1} . x = (m . p) . x ) )

for b_{1}, b_{2} being Function of the ColoredSet of CPN,NAT st ( for x being Element of the ColoredSet of CPN holds

( ( p in loc D & x = ColD . p implies b_{1} . x = ((m . p) . x) - 1 ) & ( ( not p in loc D or not x = ColD . p ) implies b_{1} . x = (m . p) . x ) ) ) & ( for x being Element of the ColoredSet of CPN holds

( ( p in loc D & x = ColD . p implies b_{2} . x = ((m . p) . x) - 1 ) & ( ( not p in loc D or not x = ColD . p ) implies b_{2} . x = (m . p) . x ) ) ) holds

b_{1} = b_{2}

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

ex b

for x being Element of the ColoredSet of CPN holds

( ( p in loc D & x = ColD . p implies b

proof end;

uniqueness for b

( ( p in loc D & x = ColD . p implies b

( ( p in loc D & x = ColD . p implies b

b

proof end;

:: deftheorem Def16Sub defines Ptr_Sub PETRI_3:def 13 :

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}

for ColD being color-threshold of D

for p being Element of CPN st t is_firable_on m,ColD holds

for b_{7} being Function of the ColoredSet of CPN,NAT holds

( b_{7} = Ptr_Sub (ColD,m,p) iff for x being Element of the ColoredSet of CPN holds

( ( p in loc D & x = ColD . p implies b_{7} . x = ((m . p) . x) - 1 ) & ( ( not p in loc D or not x = ColD . p ) implies b_{7} . x = (m . p) . x ) ) );

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}

for ColD being color-threshold of D

for p being Element of CPN st t is_firable_on m,ColD holds

for b

( b

( ( p in loc D & x = ColD . p implies b

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

ex b_{1} being Function of the ColoredSet of CPN,NAT st

for x being Element of the ColoredSet of CPN holds

( ( p in loc D & x = ColD . p implies b_{1} . x = ((m . p) . x) + 1 ) & ( ( not p in loc D or not x = ColD . p ) implies b_{1} . x = (m . p) . x ) )

for b_{1}, b_{2} being Function of the ColoredSet of CPN,NAT st ( for x being Element of the ColoredSet of CPN holds

( ( p in loc D & x = ColD . p implies b_{1} . x = ((m . p) . x) + 1 ) & ( ( not p in loc D or not x = ColD . p ) implies b_{1} . x = (m . p) . x ) ) ) & ( for x being Element of the ColoredSet of CPN holds

( ( p in loc D & x = ColD . p implies b_{2} . x = ((m . p) . x) + 1 ) & ( ( not p in loc D or not x = ColD . p ) implies b_{2} . x = (m . p) . x ) ) ) holds

b_{1} = b_{2}

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

ex b

for x being Element of the ColoredSet of CPN holds

( ( p in loc D & x = ColD . p implies b

proof end;

uniqueness for b

( ( p in loc D & x = ColD . p implies b

( ( p in loc D & x = ColD . p implies b

b

proof end;

:: deftheorem Def16Add defines Ptr_Add PETRI_3:def 14 :

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} *'

for ColD being color-threshold of D

for p being Element of CPN

for b_{7} being Function of the ColoredSet of CPN,NAT holds

( b_{7} = Ptr_Add (ColD,m,p) iff for x being Element of the ColoredSet of CPN holds

( ( p in loc D & x = ColD . p implies b_{7} . x = ((m . p) . x) + 1 ) & ( ( not p in loc D or not x = ColD . p ) implies b_{7} . x = (m . p) . x ) ) );

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} *'

for ColD being color-threshold of D

for p being Element of CPN

for b

( b

( ( p in loc D & x = ColD . p implies b

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

( ( t is_firable_on m,ColD & p in (loc D) \ (loc E) implies Ptr_Sub (ColD,m,p) is Function of the ColoredSet of CPN,NAT ) & ( t is_firable_on m,ColD & p in (loc E) \ (loc D) implies Ptr_Add (ColE,m,p) is Function of the ColoredSet of CPN,NAT ) & ( ( not t is_firable_on m,ColD or not p in (loc D) \ (loc E) ) & ( not t is_firable_on m,ColD or not p in (loc E) \ (loc D) ) implies m . p is Function of the ColoredSet of CPN,NAT ) ) ;

consistency

for b_{1} being Function of the ColoredSet of CPN,NAT st t is_firable_on m,ColD & p in (loc D) \ (loc E) & t is_firable_on m,ColD & p in (loc E) \ (loc D) holds

( b_{1} = Ptr_Sub (ColD,m,p) iff b_{1} = Ptr_Add (ColE,m,p) )

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

( ( t is_firable_on m,ColD & p in (loc D) \ (loc E) implies Ptr_Sub (ColD,m,p) is Function of the ColoredSet of CPN,NAT ) & ( t is_firable_on m,ColD & p in (loc E) \ (loc D) implies Ptr_Add (ColE,m,p) is Function of the ColoredSet of CPN,NAT ) & ( ( not t is_firable_on m,ColD or not p in (loc D) \ (loc E) ) & ( not t is_firable_on m,ColD or not p in (loc E) \ (loc D) ) implies m . p is Function of the ColoredSet of CPN,NAT ) ) ;

consistency

for b

( b

proof end;

:: deftheorem Def16 defines firing_result PETRI_3:def 15 :

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}

for E being thin_cylinder of the ColoredSet of CPN,{t} *'

for ColD being color-threshold of D

for ColE being color-threshold of E

for p being Element of CPN holds

( ( t is_firable_on m,ColD & p in (loc D) \ (loc E) implies firing_result (ColD,ColE,m,p) = Ptr_Sub (ColD,m,p) ) & ( t is_firable_on m,ColD & p in (loc E) \ (loc D) implies firing_result (ColD,ColE,m,p) = Ptr_Add (ColE,m,p) ) & ( ( not t is_firable_on m,ColD or not p in (loc D) \ (loc E) ) & ( not t is_firable_on m,ColD or not p in (loc E) \ (loc D) ) implies firing_result (ColD,ColE,m,p) = m . p ) );

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}

for E being thin_cylinder of the ColoredSet of CPN,{t} *'

for ColD being color-threshold of D

for ColE being color-threshold of E

for p being Element of CPN holds

( ( t is_firable_on m,ColD & p in (loc D) \ (loc E) implies firing_result (ColD,ColE,m,p) = Ptr_Sub (ColD,m,p) ) & ( t is_firable_on m,ColD & p in (loc E) \ (loc D) implies firing_result (ColD,ColE,m,p) = Ptr_Add (ColE,m,p) ) & ( ( not t is_firable_on m,ColD or not p in (loc D) \ (loc E) ) & ( not t is_firable_on m,ColD or not p in (loc E) \ (loc D) ) implies firing_result (ColD,ColE,m,p) = m . p ) );

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

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 )

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;