[tlaplus] Re: Does TLC handle <> and ~[]~ differently?

[Samyon Ristov <samyon.ristov@xxxxxxxxx>]

I was able to reproduce it.

I've also added, just in case, a smaller transition from Prop1 to Prop2.
Also, I added many parentheses - it didn't help. Prop1, Prop1a, and Prop2 succeed, while Prop3 fails.

What's weird is that the coverage statistics are also different, depending on the liveness property checked.
Really weird. Worth opening an issue here: https://github.com/tlaplus/tlaplus

Here are my attempts with various variations, but basically I got the same results as you did:

----------------------------- MODULE testing -----------------------------

VARIABLE s

vars == << s >>

Init == s = "a"

Next == \/ /\ s = "a"
           /\ s' = "b"
        \/ /\ s = "b"
           /\ s' = "c1"
        \/ /\ s = "b"
           /\ s' = "c2"
        \/ /\ s = "c2"
           /\ s' = "c1"
        \/ /\ s = "c1"
           /\ s' = "c2"
        \/ /\ s = "c1"
           /\ s' = "a"

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

\* Succeeds
Prop1 == (s = "b") ~> ((s = "a") \/ ([](s \in {"c1", "c2"} /\ <>(s = "c2"))))
\* Should be equivalent to Prop1. Succeeds.
Prop1a == []((s = "b") => (<>((s = "a") \/ [](s \in {"c1", "c2"} /\ <>(s = "c2")))))
\* Should be equivalent to Prop1a. Succeeds.
Prop2 == []((s # "b") \/ <>((s = "a") \/ [](s \in {"c1", "c2"} /\ <>(s = "c2"))))
\* Should be equivalent to Prop1 and Prop2. Fails.
Prop3 == []((s # "b") \/ ~([](~((s = "a") \/ [](s \in {"c1", "c2"} /\ <>(s = "c2"))))))

(*
Error trace for Prop3:

1: Initial predicate, s = "a"
2: Next in TestBug, s = "b"
3: Next in TestBug, s = "c2"
4: Next in TestBug, s = "c1"
4: Back to state (links to s = "c2")

*)

==========================================================================

On Monday, December 11, 2023 at 6:41:09 PM UTC+2 Ramon Snir wrote:

I have a module below, which is a much-simplified example of a real model I'm trying to check.

The three properties defined should be logically equivalent, but the last one gets an error in TLC. The only difference between Prop2 and Prop3 is the usage of ~[]~ vs <>, which I believe should not matter.

Is this expected TLC behavior? Should I change something in my configuration file? I would prefer not to modify the module itself, as the real one is machine-generated, and I would hate to have to implement LTL formula rewriting just to work around this specific issue.

The configuration file is very minimal:

SPECIFICATION Spec

CHECK_DEADLOCK FALSE

PROPERTIES

Prop1

Prop2

Prop3

And here is the module:

----------------------------- MODULE TestBug -----------------------------

VARIABLE s

Init == s = "a"

Next == \/ /\ s = "a"

/\ s' = "b"

\/ /\ s = "b"

/\ s' = "c1"

\/ /\ s = "b"

/\ s' = "c2"

\/ /\ s = "c2"

/\ s' = "c1"

\/ /\ s = "c1"

/\ s' = "c2"

\/ /\ s = "c1"

/\ s' = "a"

Spec == Init /\ [][Next]_s /\ WF_s(Next)

\* Succeeds

Prop1 == (s = "b") ~> ((s = "a") \/ [](s \in {"c1", "c2"} /\ <>(s = "c2")))

\* Should be equivalent to Prop1. Succeeds.

Prop2 == []((s # "b") \/ <>((s = "a") \/ [](s \in {"c1", "c2"} /\ <>(s = "c2"))))

\* Should be equivalent to Prop1 and Prop2. Fails.

Prop3 == []((s # "b") \/ ~[]~((s = "a") \/ [](s \in {"c1", "c2"} /\ <>(s = "c2"))))

(*

Error trace for Prop3:

1: Initial predicate, s = "a"

2: Next in TestBug, s = "b"

3: Next in TestBug, s = "c2"

4: Next in TestBug, s = "c1"

4: Back to state (links to s = "c2")

*)

==========================================================================

-- 
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/ada61691-a613-42ce-9619-67e9691eb75an%40googlegroups.com.