Invariants
==========

Similar to an ``init`` block, which constrains the initial states of a model, an
``invariant`` block constrains the set of reachable states (this includes the
initial states). Consider the following example::

   invariant
       mod(my_feature.x, 2) = 0;
   endinvariant

   feature my_feature
       modules my_module;
   endfeature

   module my_module
       x : [0..4];

       [] x < 4 -> (x' = x + 1);
       [] x < 3 -> (x' = x + 2);
   endmodule

In this example, the first command of ``my_module`` will never be executed, since
adding 1 to ``x`` would violate the invariant. However, the second command is
not affected, as it does not lead to a violation of the invariant.