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