Add CIF to CIF transformation to eliminate state invariants

We already have a CIF to CIF transformation to eliminate state/event exclusion invariants, but not for state invariants.

I think we can make a syntactic transformation. For an edge 'e' with guard 'g' and update 'x := E' and a state invariant 'i', we can change 'g' to 'g and i[x := E]'. That is, for each edge 'e', compute the expression that indicates the new value for each assigned variable. We can reuse what we do in the CIF to CIF transformation for elimination of 'if' updates for that. Then in the invariant, replace each updated variable by the expression that indicates its new variable, and add the result of that as an extra guard. We could optimize this to only add new guards for invariants that contain the updated variable.

As an example, the following model:

event e;
automaton a:
  disc int x;
  invariant x < 9;
  location:
    initial;
    edge e when x < 10 do x := x + 1;
end

Would be translated to:

event e;
automaton a:
  disc int x;
  location:
    initial;
    edge e when x < 10, x + 1 < 9 do x := x + 1;
end

I think we want different variants of the transformation for all invariants, only plant invariants, only requirements invariants, and only supervisor invariants. Although I'm not sure about supervisor invariants, as this would not do the same as synthesis does. The variant for only plant invariants is what we need for a paper that is a follow-up to the CASE'24 paper "Validation of supervisory control synthesis tool CIF using model checker mCRL2" by Michel Reniers and Jeroen Keiren.