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.

[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 3f0847802bab27c4e57c3da11841a88d4ae07709. https://github.com/tlaplus/tlapm/commit/581ebd8afbe927b2b7d31c62ccec3a3409d9d8ce is the last commit with which TLAPS accepts the proof. :-(

Related: https://github.com/tlaplus/tlapm/issues/139