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

*From*: Shuhao Wu <shuhao@xxxxxxxxxxxx>*Date*: Mon, 28 Jun 2021 15:01:07 -0400*Ironport-hdrordr*: A9a23:v1CL266gCJsh8UWqxgPXwPDXdLJyesId70hD6qkRc20zTiT7//rFoB1/73LJYVkqNE3I9eruBED4ex3hHP1OkO0s1MmZPTUO0VHAROpfBLfZsl/d8kbFh4tgPMlbAstDIey1B15/lM7E0TLQKbYd/OU=*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.11.0

Hello all:

--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;

What am I missing? Thanks, Shuhao -- 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/16569f5a-d5fe-01d9-196a-c5e76adaaaed%40shuhaowu.com.

**Follow-Ups**:

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