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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Mon, 7 May 2018 06:44:55 -0700 (PDT)*References*: <b5e536f3-fbe0-4ce6-9f8a-d9b76930eb7a@googlegroups.com>

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

**Follow-Ups**:**Re: Use of primed variables in a temporal formula***From:*Giulio Salierno

**References**:**Use of primed variables in a temporal formula***From:*Giulio Salierno

- Prev by Date:
**Use of primed variables in a temporal formula** - Next by Date:
**Re: Use of primed variables in a temporal formula** - Previous by thread:
**Use of primed variables in a temporal formula** - Next by thread:
**Re: Use of primed variables in a temporal formula** - Index(es):