An invariant is a predicate that is true in all states.
In the context of state machines,
we usually care that an invariant is true
in all reachable states.
The statement of an invariant, 
, in full generality looks like:
where is a predicate over variables in s
and in is a predicate that says whether a state is in an execution.
Normally the universal quantification over all executions and the
condition that s be in e is omitted (it is understood):
Sometimes we also omit the universal quantification over s as well because it's also understood:
For example, here is an invariant for the Counter example given in State Machine Variations handout:
which says that in all states, x's value is greater than or equal to 0. We know this is true because initially x's value is 0 and because the inc action always increases x's value by 1. Since inc is Counter's only action, there's no other way to change x.