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

*From*: Giulio Salierno <salier...@xxxxxxxxx>*Date*: Mon, 7 May 2018 09:09:26 -0700 (PDT)*References*: <b5e536f3-fbe0-4ce6-9f8a-d9b76930eb7a@googlegroups.com> <e51a5b46-2933-422c-94b6-ea89d81d5241@googlegroups.com>

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:

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

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

**Re: Use of primed variables in a temporal formula***From:*Leslie Lamport

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