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

Re: Use of primed variables in a temporal formula



Thank You Mr. Lamport, both the HourClock example and Section 8.1 helped me a lot.

Cheers,

Giulio

Il giorno lunedì 7 maggio 2018 15:44:55 UTC+2, Leslie Lamport ha scritto:
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