An invariant is supposed to be true of every state of every execution of a state machine. You might ask is there a corresponding notion for state transitions? The answer is ``yes,'' though because it is not as commonly discussed in the literature, there is no common term for such a property. Some people might simply call it another kind of invariant, one over state transitions rather than states. To avoid confusion with state invariants, I'm going to call it a constraint. This word is not standard; also, others may use ``constraint'' to mean something different.
Consider any execution of a state machine:
A constraint is a predicate that is true in all pairs of states,
and 
, in every execution, where
follows , but need not immediately follow it ( does not have
to be 
).
The statement of a constraint, 
, in full generality looks like:
As for statements of invariants, we omit (because it's
understood) the
universal
quantification over executions and states; the condition about
and both being states in the execution; and the condition that
precedes in the execution.
A constraint that holds for the Counter example is that its value always strictly increases:
s'(x) > s(x)
Does this constraint (appropriately restated) hold for SimpleCounter? BigCounter (careful!)? FatCounter? RandomCounter?