Re: [tlaplus] Why does this liveness property not work?

[Igor Konnov <igor.konnov@xxxxxxxxx>]

It does not report any liveness violation in the TLA+ Toolbox for me
(using the ASCII version).

-- 
Igor

On Thu, Oct 3, 2024 at 4:47 PM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:
>
> Interesting observation. I notice that TLC (correctly) verifies the following variants of the property:
>
> Liveness == <>[](x = 5)
> Liveness == (x = 1) /\ <>[](x = 5)
> Liveness == (x = 0) => <>[](x = 0)
>
> Stephan
>
> On 3 Oct 2024, at 16:17, Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:
>
> Here's a simple spec with a variable x that counts from 1 to 5 then stutters at 5 forever:
>
> ---- MODULE Test ----
> EXTENDS Naturals
> VARIABLE x
> Init ≜ x = 1
> Next ≜
>   IF x = 5 THEN UNCHANGED x
>   ELSE x' = x + 1
> Spec ≜ Init ∧ □[Next]_x ∧ WF_x(Next)
> Liveness ≜ (x = 1) ⇒ ◇□(x = 5)
> ====
>
> However, when I try to check property Liveness with TLC I get this error:
>
> Starting... (2024-10-03 10:15:19)
> Implied-temporal checking--satisfiability problem has 1 branches.
> Computing initial states...
> Finished computing initial states: 1 distinct state generated at 2024-10-03 10:15:19.
> Error: Temporal properties were violated.
>
> Error: The following behavior constitutes a counter-example:
>
> State 1: <Initial predicate>
> x = 1
>
> 2 states generated, 2 distinct states found, 1 states left on queue.
> The depth of the complete state graph search is 2.
> Finished in 00s at (2024-10-03 10:15:19)
>
> Why is this?
>
> Andrew
>
> --
> 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/42b3b918-e70a-4506-911f-b7b282fcc6acn%40googlegroups.com.
>
>
> --
> 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/67B1C8A4-AEEA-4FDE-AE4F-476CCEEFB2BE%40gmail.com.

-- 
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/CACooHMBzA_DXohgiQom4DHbPLtWz-%2BrjneHWwdoU98-wvQ0DAQ%40mail.gmail.com.