Petri Net Models
places can be occupied by tokens
directed arcs connect places and transitions
transitions are enabled if all its input arcs come from places occupied by tokens
enabled transitions can fire removing all incoming tokens and placing tokens at all places connected to it by output arcs