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