Assumptions
We assume the cost of running the matcher for the same data sent/produced to a channel is the same (negligible) regardless of what the pattern is on the corresponding for/consumewe have a static checker that determines whether a match has a constant cost - for example, matching for true or a plain integer. For those matches that do not have a constant cost, we assign a global constant C as the cost and prohibit any matches that are more costly than this. We also assume that the (not tight) upper bound cost of running the matcher to get a single successful match on a channel will be as if all the produces on that channel that eventually reduced according to the current replay log already existed in the replay rspace, and we ran the matcher over all of them.
...