creating a specification from another one and eliminating some variables

[Amira Methni <methni...@xxxxxxxxx>]

Hi,

I have a specification S1 with two variables "x" and "y". And the value of "y" depends on "x".

I'm interested to create a specification S2 through S1, based only on the values of "y" with eliminating "x". So, the space state of S2 is based only on the values of "y". 

Is it possible to do this in TLA+?

Thank you