First read Section 2.2 of "Specifying Systems" to see if you really want to write the temporal formula you are trying to write. If you do, see Section 8.1 for an explanation of the temporal formulas you can write in TLA+.
Leslie
On Monday, May 7, 2018 at 6:00:12 AM UTC-7, Giulio Salierno wrote:
Dear All,
I'm a little bit confused on how to properly use primed variables in a temporal formula. I want to verify a simple statement A ~> A' so if A becomes true, A' must be true in the next state.
Can someone explain me which is the correct way to build such formula?
Cheers,
Giulio