:: deftheorem defines synthesis PETRI_2:def 15 :
for CPNT1, CPNT2 being Colored-PT-net
for O being connecting-mapping of CPNT1,CPNT2
for q being connecting-firing-rule of CPNT1,CPNT2,O st CPNT1 misses CPNT2 holds
for b₅ being strict Colored-PT-net holds
( b₅ = synthesis (CPNT1,CPNT2,O,q) iff ex q12, q21 being Function ex O12 being Function of (Outbds CPNT1), the carrier of CPNT2 ex O21 being Function of (Outbds CPNT2), the carrier of CPNT1 st
( O = [O12,O21] & dom q12 = Outbds CPNT1 & dom q21 = Outbds CPNT2 & ( 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)))) ) & ( for t02 being 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 b₅ = the carrier of CPNT1 \/ the carrier of CPNT2 & the carrier' of b₅ = the carrier' of CPNT1 \/ the carrier' of CPNT2 & the S-T_Arcs of b₅ = the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 & the T-S_Arcs of b₅ = (( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21 & the ColoredSet of b₅ = the ColoredSet of CPNT1 \/ the ColoredSet of CPNT2 & the firing-rule of b₅ = (( the firing-rule of CPNT1 +* the firing-rule of CPNT2) +* q12) +* q21 ) );