Token-based replay conformance checking against a Ex4pm.Engine.Discovery.InductiveMiner.ProcessTree, with superfluous-token freezing so repeated activities in a trace do not flood the produced/ consumed counters.

Token-replay model

Each process-tree leaf owns a single conceptual place. Replaying a real trace against the tree:

• produces a token at the tree's start each time an execution begins,
• consumes a token at each leaf the trace visits in an order consistent with the tree structure (sequence enforces left-to-right; exclusive choice enforces exactly one live branch),
• counts a missing token whenever the trace visits a leaf that has no token available to consume (the model expected something else first),
• counts a remaining token whenever a leaf that received a token was never visited by the trace (log ends early / skips a branch).

Superfluous-token freezing

Without freezing, an activity that repeats in a trace but appears only once in the tree (e.g. trace [a, a, b] against tree seq(a, b)) would either flood extra tokens into a's place (inflating produced) or silently double-consume. This implementation freezes a leaf's place after its single token is legitimately consumed: any further trace visit to an already-frozen leaf is counted as missing (an unexpected repeat) rather than manufacturing a new token — this is the freezing behavior the task asks for, scoped to the single-token-per-leaf-visit case this module actually implements (not a general marking/Petri-net multiset replay).