CIF to CIF transformation to eliminate state invariants incorrect for synchronizing events
Consider the following CIF model in which automata `A` anb `B` synchronize over event `a`, thereby update their own local variables `A.x` and `B.x`, and a state plant invariant to keep the local variables equal:
```
event a;
automaton A:
disc bool x = false;
location:
initial;
edge a do x := true;
end
automaton B:
disc bool x = false;
location:
initial;
edge a do x := not x;
end
plant invariant A.x = B.x;
```
The state space of this CIF model is
```
event a;
automaton statespace:
alphabet a;
@state(A: "*", A.x: false, B: "*", B.x: false)
location loc1:
initial;
edge a goto loc2;
@state(A: "*", A.x: true, B: "*", B.x: true)
location loc2;
end
```
Now, if we apply the CIF to CIF transformation to eliminate state invariants, we obtain the model
```
event a;
automaton A:
disc bool x = false;
location:
initial;
edge a when true = B.x do x := true;
end
automaton B:
disc bool x = false;
location:
initial;
edge a when A.x = not x do x := not x;
end
```
which has the following *different* state space:
```
event a;
automaton statespace:
alphabet a;
@state(A: "*", A.x: false, B: "*", B.x: false)
location loc1:
initial;
end
```
As you can see, the transformed model where the state invariant has been eliminated does not consider the update of 'other' local variable: for edge `a` in `A`, the invariant `A.x = B.x` is translated to `true = B.x` where the update on `A.x` has been considered, but the update of `B.x` is not.
issue