Make SimpleEventually proof a bit less simple.

[lemmy]

Two actions, A and B, allow for the discussion of the non-distributiveness of (weak) fairness.

Happy to remove Equiv again.

[muenchnerkindl]

See individual comments. In particular, this uncovers a big problem with the old SMT backend.

[lemmy]

See individual comments. In particular, this uncovers a big problem with the old SMT backend.

Please take another look at this PR. I will open an issue for the Equiv proof.

[kape1395]

It fails (line 63) for me with the tlapm from the main branch. Maybe another branch is assumed here?

[lemmy]

Confirmed to be rejected by HEAD@main on a Codespace (Linux):

@lemmy ➜ /workspaces/tlapm/examples (mku-LessSimpleEventually) $ tlapm --version
102637f-dirty
@lemmy ➜ /workspaces/tlapm/examples (mku-LessSimpleEventually) $ tlapm SimpleEventually.tla 
(* created new ".tlacache/TLAPS.tlaps/TLAPS.thy" *)
(* fingerprints written in ".tlacache/TLAPS.tlaps/fingerprints" *)
File "/usr/local/lib/tlapm/stdlib/TLAPS.tla", line 1, character 1 to line 362, character 77:
[INFO]: All 0 obligation proved.
Zenon error: exhausted search space without finding a proof
(* created new ".tlacache/SimpleEventually.tlaps/SimpleEventually.thy" *)
(* fingerprints written in ".tlacache/SimpleEventually.tlaps/fingerprints" *)
File "./SimpleEventually.tla", line 63, characters 3-4:
[ERROR]: Could not prove or check:
           ASSUME NEW VARIABLE x,
                  NEW VARIABLE y,
                  NEW VARIABLE flip,
                  vars == <<x, y, flip>>,
                  A == /\ x = FALSE
                       /\ x' = TRUE
                       /\ UNCHANGED <<y, flip>>,
                  B ==
                    /\ y = FALSE
                    /\ y' = TRUE
                    /\ flip' = (~flip)
                    /\ UNCHANGED x,
                  C ==
                    /\ y = FALSE
                    /\ y' = TRUE
                    /\ flip' = (~flip)
                    /\ UNCHANGED x,
                  Next == A \/ B \/ C,
                  ExpandENABLED 
           PROVE  TypeOK /\ ~x = TRUE => ENABLED <<Next>>_vars
File "./SimpleEventually.tla", line 1, character 1 to line 73, character 80:
[ERROR]: 1/18 obligations failed.
There were backend errors processing module `"SimpleEventually"`.
 tlapm ending abnormally with (Failure "backend errors: there are unproved obligations")
Raised at file "stdlib.ml", line 29, characters 17-33
Called from file "src/tlapm_lib.ml", line 435, characters 12-77
Called from file "src/tlapm_lib.ml", line 543, characters 23-43
Called from file "list.ml", line 121, characters 24-34
Called from file "src/tlapm_lib.ml", line 546, characters 13-40
Called from file "src/tlapm_lib.ml", line 558, characters 8-33

Accepted by https://github.com/tlaplus/tlapm/releases/tag/202210041448 on macOS:

markus@avocado [11:49:01] [~/src/TLA/_tlaps/tlapm] [mku-LessSimpleEventually]
-> % tlapm --version
1.5.0

markus@avocado [11:49:06] [~/src/TLA/_tlaps/tlapm] [mku-LessSimpleEventually]
-> % tlapm examples/SimpleEventually.tla
(* created new ".tlacache/TLAPS.tlaps/TLAPS.thy" *)
(* fingerprints written in ".tlacache/TLAPS.tlaps/fingerprints" *)
File "/usr/local/lib/tlaps/TLAPS.tla", line 1, character 1 to line 362, character 77:
[INFO]: All 0 obligation proved.
The operation couldn’t be completed. Unable to locate a Java Runtime.
Please visit http://www.java.com for information on installing Java.

** Unexpanded symbols: ---

** Unexpanded symbols: ---

** Unexpanded symbols: STATE_TypeOK_

** Unexpanded symbols: ---

** Unexpanded symbols: ---

** Unexpanded symbols: ---

(* created new ".tlacache/SimpleEventually.tlaps/SimpleEventually.thy" *)
(* fingerprints written in ".tlacache/SimpleEventually.tlaps/fingerprints" *)
File "./examples/SimpleEventually.tla", line 1, character 1 to line 73, character 80:
[INFO]: All 18 obligations proved.

[lemmy]

Stephan's proposed proof already rejected by HEAD@main:

@lemmy ➜ /workspaces/tlapm/examples (mku-LessSimpleEventually) $ tlapm SimpleEventually.tla 
(* created new ".tlacache/TLAPS.tlaps/TLAPS.thy" *)
(* fingerprints written in ".tlacache/TLAPS.tlaps/fingerprints" *)
File "/usr/local/lib/tlapm/stdlib/TLAPS.tla", line 1, character 1 to line 362, character 77:
[INFO]: All 0 obligation proved.
(* loading fingerprints in ".tlacache/SimpleEventually.tlaps/fingerprints" *)
Zenon error: exhausted search space without finding a proof
(* created new ".tlacache/SimpleEventually.tlaps/SimpleEventually.thy" *)
(* fingerprints written in ".tlacache/SimpleEventually.tlaps/fingerprints" *)
File "./SimpleEventually.tla", line 54, characters 3-4:
[ERROR]: Could not prove or check:
           ASSUME NEW VARIABLE x,
                  NEW VARIABLE y,
                  vars == <<x, y>>,
                  A == /\ x = FALSE
                       /\ x' = TRUE
                       /\ UNCHANGED y,
                  B == /\ y = FALSE
                       /\ y' = TRUE
                       /\ UNCHANGED x,
                  Next == A \/ B,
                  ExpandENABLED 
           PROVE  TypeOK /\ ~x = TRUE => ENABLED <<Next>>_vars
File "./SimpleEventually.tla", line 1, character 1 to line 64, character 80:
[ERROR]: 1/18 obligations failed.
There were backend errors processing module `"SimpleEventually"`.
 tlapm ending abnormally with (Failure "backend errors: there are unproved obligations")
Raised at file "stdlib.ml", line 29, characters 17-33
Called from file "src/tlapm_lib.ml", line 435, characters 12-77
Called from file "src/tlapm_lib.ml", line 543, characters 23-43
Called from file "list.ml", line 121, characters 24-34
Called from file "src/tlapm_lib.ml", line 546, characters 13-40
Called from file "src/tlapm_lib.ml", line 558, characters 8-33

[lemmy]

TLAPS starts to reject Stephan's proposed proof as well as my extension with the introduction of the new SMT encoding in 3f08478. 581ebd8 is the last commit with which TLAPS accepts the proof. :-(

Related: #139

[damiendoligez]

TLAPS starts to reject Stephan's proposed proof

Stephan's proof goes through if you simply add , TypeOK at the end of line 54 : the prover now needs x \in BOOLEAN to prove that x # FALSE implies x = TRUE.

as well as my extension

The same fix (on line 63) works for your version.

[muenchnerkindl]

Nice, thanks for fixing this proof!

[muenchnerkindl]

LGTM.