CIF to CIF elim def/inst transformation may produce invalid models for assignments with algebraic parameters.
group def X(alg int y): automaton A: disc int[0..0] x; event e; location: initial; edge e do x := y; end end x: X(1);
Is transformed into:
group x: alg int y = 1; automaton A: disc int[0..0] x; event e; location: initial; edge e do x := y; end end
x := y gives the following error:
The type "int[1..1]" of the value of the assignment is incompatible with type "int[0..0]" of the addressable.
The problem is that we go from a rangeless int to an (implicit) ranged int.
My understanding is that CIF to CIF transformations should not generate invalid models if the input model is valid.