Regression in BlockingQueue proof

[lemmy]

Proof at https://github.com/lemmy/BlockingQueue/blob/main/BlockingQueue.tla

-> % ~/.opam/5.1.0/bin/tlapm --nofp --cleanfp BlockingQueue.tla
(* fingerprints file ".tlacache/BlockingQueue.tlaps/fingerprints" removed *)
(* created new ".tlacache/BlockingQueue.tlaps/BlockingQueue.thy" *)
(* fingerprints written in ".tlacache/BlockingQueue.tlaps/fingerprints" *)
File "./BlockingQueue.tla", line 108, characters 36-37:
[ERROR]: Could not prove or check:
           ASSUME NEW CONSTANT Producers,
                  NEW CONSTANT Consumers,
                  NEW CONSTANT BufCapacity,
                  Assumption ==
                    /\ Producers # {}
                    /\ Consumers # {}
                    /\ Producers \cap Consumers = {}
                    /\ BufCapacity \in Nat \ {0},
                  NEW VARIABLE buffer,
                  NEW VARIABLE waitSet,
                  vars == <<buffer, waitSet>>,
                  RunningThreads == (Producers \cup Consumers) \ waitSet,
                  NotifyOther(Others) ==
                    IF waitSet \cap Others # {}
                      THEN \E t \in waitSet \cap Others :
                              waitSet' = waitSet \ {t}
                      ELSE UNCHANGED waitSet,
                  Wait(t) ==
                    /\ waitSet' = waitSet \cup {t}
                    /\ UNCHANGED <<buffer>>,
                  Put(t, d) ==
                    /\ t \notin waitSet
                    /\ \/ /\ Len(buffer) < BufCapacity
                          /\ buffer' = Append(buffer, d)
                          /\ NotifyOther(Consumers)
                       \/ /\ Len(buffer) = BufCapacity
                          /\ Wait(t),
                  Get(t) ==
                    /\ t \notin waitSet
                    /\ \/ /\ buffer # <<>>
                          /\ buffer' = Tail(buffer)
                          /\ NotifyOther(Producers)
                       \/ /\ buffer = <<>>
                          /\ Wait(t),
                  Init == /\ buffer = <<>>
                          /\ waitSet = {},
                  Next ==
                    \/ \E p \in Producers : Put(p, p)
                    \/ \E c \in Consumers : Get(c),
                  TypeInv ==
                    /\ buffer \in Seq(Producers)
                    /\ Len(buffer) \in 0..BufCapacity
                    /\ waitSet \in SUBSET (Producers \cup Consumers),
                  Invariant == waitSet # Producers \cup Consumers,
                  Spec == Init /\ [][Next]_vars,
                  Assumption ,
                  IInv ==
                    /\ Len(buffer) \in 0..BufCapacity
                    /\ waitSet \in SUBSET (Producers \cup Consumers)
                    /\ Invariant
                    /\ buffer = <<>>
                       => (\E p \in Producers : p \notin waitSet)
                    /\ Len(buffer) = BufCapacity
                       => (\E c \in Consumers : c \notin waitSet)
           PROVE  IInv /\ [Next]_vars => IInv'
File "./BlockingQueue.tla", line 1, character 1 to line 152, character 77:
[ERROR]: 1/18 obligations failed.
There were backend errors processing module `"BlockingQueue"`.
 tlapm ending abnormally with Failure("backend errors: there are unproved obligations")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from Tlapm_lib.process_module in file "src/tlapm_lib.ml", line 446, characters 12-77
Called from Tlapm_lib.main.f in file "src/tlapm_lib.ml", line 574, characters 23-43
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
Called from Tlapm_lib.main in file "src/tlapm_lib.ml", line 577, characters 13-40
Called from Tlapm_lib.init in file "src/tlapm_lib.ml", line 589, characters 8-33

-> % ~/.opam/5.1.0/bin/tlapm --version
6acb3cb

-> % tlapm --nofp --cleanfp BlockingQueue.tla
(* fingerprints file ".tlacache/FiniteSets.tlaps/fingerprints" removed *)
(* created new ".tlacache/FiniteSets.tlaps/FiniteSets.thy" *)
(* fingerprints written in ".tlacache/FiniteSets.tlaps/fingerprints" *)
File "/usr/local/lib/tlaps/FiniteSets.tla", line 1, character 1 to line 23, character 77:
[INFO]: All 0 obligation proved.
(* fingerprints file ".tlacache/TLAPS.tlaps/fingerprints" removed *)
(* created new ".tlacache/TLAPS.tlaps/TLAPS.thy" *)
(* fingerprints written in ".tlacache/TLAPS.tlaps/fingerprints" *)
File "./TLAPS.tla", line 1, character 1 to line 311, character 77:
[INFO]: All 0 obligation proved.
(* fingerprints file ".tlacache/BlockingQueue.tlaps/fingerprints" removed *)
** Unexpanded symbols: ---

** Unexpanded symbols: ---

** Unexpanded symbols: ---

** Unexpanded symbols: ---

** Unexpanded symbols: ---

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

-> % tlapm --version
1.5.0

[kape1395]

This proof works:

THEOREM DeadlockFreedom == Spec => []Invariant
<1>1. Init => IInv BY SMT DEF IInv
<1>2. TypeInv /\ IInv /\ [Next]_vars => IInv' BY DEF IInv
<1>3. IInv => Invariant  BY DEF IInv
<1>4. QED BY TypeCorrect, <1>1,<1>2,<1>3,PTL

Here, I added the use of TypeCorrect. Maybe @muenchnerkindl could comment on whether that's a regression or proof that has to be updated.

[lemmy]

This proof works:

THEOREM DeadlockFreedom == Spec => []Invariant
<1>1. Init => IInv BY SMT DEF IInv
<1>2. TypeInv /\ IInv /\ [Next]_vars => IInv' BY DEF IInv
<1>3. IInv => Invariant  BY DEF IInv
<1>4. QED BY TypeCorrect, <1>1,<1>2,<1>3,PTL

Apparently, it also suffices to "just" add TypeInv!1 to IInv (see below). This is interesting because when I first wrote the proof, I intentionally removed TypeInv!1, as you can see in https://github.com/lemmy/BlockingQueue/commit/dc3b3aabbfa6c2f5e9445548b5b17f97b228c4fc.

diff --git a/BlockingQueue.tla b/BlockingQueue.tla
index 29be666..b8ea33e 100644
--- a/BlockingQueue.tla
+++ b/BlockingQueue.tla
@@ -92,7 +92,8 @@ LEMMA TypeCorrect == Spec => []TypeInv

 \* The naive thing to do is to check if the conjunct of TypeInv /\ Invariant
 \* is inductive.
-IInv == /\ TypeInv!2
+IInv == /\ TypeInv!1
+        /\ TypeInv!2
         /\ TypeInv!3
         /\ Invariant
         \* When the buffer is empty, a consumer will be added to the waitSet.