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

*From*: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>*Date*: Mon, 28 Jun 2021 12:33:14 -0700*Ironport-hdrordr*: A9a23:FADana1H01Jm6O6+N+o/QgqjBLkkLtp133Aq2lEZdPUnSL39qynIpoV/6faUskdyZJhOo7690cW7LU80sKQFgrX5Xo3DYOCFggSVxehZhOPfKn/bdhEWndQ36U4PScJD4ZHLbGRHsQ==*References*: <16569f5a-d5fe-01d9-196a-c5e76adaaaed@shuhaowu.com>

On 6/28/21 12:01 PM, Shuhao Wu wrote:

I've been trying to write a temporal property to check in TLC where Iwant to know that some condition F leads to G, and G remain true for therest of time. This lead me to using the temporal operators ~> and []together, in a statement in the form of F ~> []G. I'm likelymisunderstanding one of these operators, as when I used TLC to check thefollowing simple spec, the nothing was found to be violated:--fair algorithm leadstoalways variables i = 1; define \* This is the temporal property to check OneLeadsToTwo == (i = 1) ~> [](i = 2) end define; begin step1: i := 2; step2: i := 3; step3: i := 2; end algorithm;My understanding is that (i = 1) ~> (i = 2) would be true for the aboveprogram (which is true in TLC). In the same understanding, (i = 1) ~>[](i = 2) would not be true, as the variable i changed from 1 to 2, thenaway from 2, and then back to 2. This means that i = 2 is not alwaystrue following the initial transition from i = 1 to i = 2.What am I missing?

M. -- You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7668376b-91f4-1caa-18e2-186585cd4835%40lemmster.de.

**Follow-Ups**:

**References**:

- Prev by Date:
**[tlaplus] Temporal operator leads to always (F ~> []G): misunderstanding?** - Next by Date:
**Re: [tlaplus] Temporal operator leads to always (F ~> []G): misunderstanding?** - Previous by thread:
**[tlaplus] Temporal operator leads to always (F ~> []G): misunderstanding?** - Next by thread:
**Re: [tlaplus] Temporal operator leads to always (F ~> []G): misunderstanding?** - Index(es):