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

[tlaplus] Temporal operator leads to always (F ~> []G): misunderstanding?

Hello all:

I've been trying to write a temporal property to check in TLC where I want to know that some condition F leads to G, and G remain true for the rest of time. This lead me to using the temporal operators ~> and [] together, in a statement in the form of F ~> []G. I'm likely misunderstanding one of these operators, as when I used TLC to check the following simple spec, the nothing was found to be violated:

--fair algorithm leadstoalways
variables i = 1;

 \* This is the temporal property to check
 OneLeadsToTwo == (i = 1) ~> [](i = 2)
end define;


 step1: i := 2;
 step2: i := 3;
 step3: i := 2;

end algorithm;

My understanding is that (i = 1) ~> (i = 2) would be true for the above program (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, then away from 2, and then back to 2. This means that i = 2 is not always true following the initial transition from i = 1 to i = 2.

What am I missing?


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.