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