[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Use of primed variables in a temporal formula
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+.
On Monday, May 7, 2018 at 6:00:12 AM UTC-7, Giulio Salierno wrote:
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?