Examples are specified at: "Examples.Invariant".
An invariant is an inequation that specifies an upper bound on a clock, e.g., c < 2 or c <= 2 where c is a Clock. Invariants are assigned to generalized steps and are used to specify a time span in which this generalized step is allowed to be active.