[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

creating a specification from another one and eliminating some variables


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