Simple logic shows that your definition of UpdateCounter is
equivalent to
UpDateCounter(participant, newCounter) ==
/\ counters[participant] < newCounter
/\ counters' = [counters EXCEPT ![participant] = newCounter]
(For example FALSE /\ UNCHANGED << counters >> is equivalent to FALSE.)
I don't see how to do what you're trying to do. It's possible
that there's some clever way to express what you want to express.
However, I'm almost certain that TLC would not be able to handle the
resulting spec.
I suggest that you stop thinking in terms of programming language
constructs and start thinking in terms of two separate physical
components that are trying to cooperate, with each of them revealing
to the other as little about their state as possible.