[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Temporal operator leads to always (F ~> G): misunderstanding?
- From: Shuhao Wu <shuhao@xxxxxxxxxxxx>
- Date: Mon, 28 Jun 2021 16:06:54 -0400
- Ironport-hdrordr: A9a23:4p0JqaFpqxcykTwjpLqF6pHXdLJyesId70hD6qkvc3AlCvBwxvrC7Y0mPEHP4kd2ZJhSo6HNBEDmewKSyXcV2/hdAV7GZmbbUQSTXchfBOfZskrd8mjFh6RgPUkJSdknNDXfZWIK1PoSozPIVurJ+bG8geaVbJ7lvixQpGJRGupdB7ITMHfYLqQVfngxOXNjLuve2iMvnVPJEgVyH7/Lewh4Lpv+SsXw5ejbiFw9dmoaAW+1/HOVAZHBciRwtS1uIQ+nr41ShFQt3zaJrplKcpmAu3rhPqzoj6i+WuGO9jPyb/b8zfT95g+c6TqAVcBEd/m6pzYlsIiUmSYXueiJhztlBt90+mOUVGmouxeF4XiQ7B8er1vPjWSVi3fivsD1LQhKdfZptMZ8Xl/i500ssMoU6tM144qV3KAnTC8pbE/Glpb1vthR5yjExkYKoKoolnRaFaEeZLVSoYFa3EQQPowHADuS0vFiLNVT
- References: <email@example.com> <firstname.lastname@example.org>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.11.0
Thanks! Looking at the book a bit more, it says that F ~> G is
equivalent to saying that exists a behavior following of F that
satisfies G. I'm can kind of see that F ~> G doesn't quite work, but
my intuition is still a bit fuzzy.
That said, from Specifying Systems (page 89) I can see that if I want to
check that G remains true after the initial transition, I can add a
separate temporal property:
TwoRemainsTwo == ((i = 2) => (i = 2))
I added this to the temporal properties and TLC indeed finds a
violation. However, when I combined the two conditions:
(i = 1) ~> (i = 2) /\ ((i = 2) => (i = 2))
and checked this in TLC, it appears to find no violations again? Am I
doing something wrong again?
On 2021-06-28 3:33 p.m., Markus Kuppe wrote:
On 6/28/21 12:01 PM, Shuhao Wu wrote:
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)
step1: i := 2;
step2: i := 3;
step3: i := 2;
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?
Leads-to (P ~> Q) is "syntactic sugar" for (P => <>Q) (see page 91
of Specifying Systems).
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/4fc36b77-e942-2301-1beb-6c175725c88e%40shuhaowu.com.