From e9cf852e8109019f7195f3ed9241c66c1441573b Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <tlaplus.net@lemmster.de>
Date: Wed, 24 Jun 2020 17:58:55 -0700
Subject: [PATCH] v30 (RefinementFair): Prove TypeInv is an inductive invariant
 of BlockingQueueFair.

---
 .github/workflows/main.yml |  4 ++-
 .gitignore                 |  1 +
 BlockingQueueFair.tla      | 61 ++++++++++++++++++++++++++++++++++++++
 README.md                  |  4 +++
 4 files changed, 69 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index c940b5c..f2a7551 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -15,6 +15,8 @@ jobs:
       with:
         path: tlaps/
         key: tlaps1.4.5
+    - name: Extract CommunityModules for TLAPS
+      run: unzip CommunityModules.jar -d CommunityModules/
     - name: Get TLAPS
       if: steps.cache.outputs.cache-hit != 'true' # see actions/cache above
       run: wget https://tla.msr-inria.inria.fr/tlaps/dist/current/tlaps-1.4.5-x86_64-linux-gnu-inst.bin
@@ -24,7 +26,7 @@ jobs:
         chmod +x tlaps-1.4.5-x86_64-linux-gnu-inst.bin
         ./tlaps-1.4.5-x86_64-linux-gnu-inst.bin -d tlaps
     - name: Run TLAPS
-      run: tlaps/bin/tlapm --cleanfp -I tlaps/ BlockingQueue.tla BlockingQueueSplit.tla
+      run: tlaps/bin/tlapm --cleanfp -I tlaps/ -I CommunityModules/ BlockingQueue.tla BlockingQueueSplit.tla BlockingQueueFair.tla
     - name: Get (nightly) TLC
       run: wget https://nightly.tlapl.us/dist/tla2tools.jar
     - name: Run TLC
diff --git a/.gitignore b/.gitignore
index 163662f..5738bac 100644
--- a/.gitignore
+++ b/.gitignore
@@ -11,3 +11,4 @@ build/
 .classpath
 .project
 impl/producer_consumer
+CommunityModules/
diff --git a/BlockingQueueFair.tla b/BlockingQueueFair.tla
index 2b820ef..2805cf4 100644
--- a/BlockingQueueFair.tla
+++ b/BlockingQueueFair.tla
@@ -85,4 +85,65 @@ BQSStarvation == BQS!A!Starvation
 THEOREM FairSpec => BQSStarvation
 -----------------------------------------------------------------------------
 
+TypeInv == /\ Len(buffer) \in 0..BufCapacity
+           \* Producers
+           /\ waitSeqP \in Seq(Producers)
+           /\ IsInjective(waitSeqP) \* no duplicates (thread is either asleep or not)!
+           \* Consumers
+           /\ waitSeqC \in Seq(Consumers)
+           /\ IsInjective(waitSeqC) \* no duplicates (thread is either asleep or not)!
+
+INSTANCE TLAPS
+
+(* Prove TypeInv inductive. *)
+THEOREM ITypeInv == Spec => []TypeInv
+<1> USE Assumption DEF Range, TypeInv
+<1>1. Init => TypeInv 
+    BY DEF Init, IsInjective
+<1>2. TypeInv /\ [Next]_vars => TypeInv'
+  <2> SUFFICES ASSUME TypeInv,
+                      [Next]_vars
+               PROVE  TypeInv'
+    OBVIOUS
+  <2>1. ASSUME NEW p \in Producers,
+               Put(p, p)
+        PROVE  TypeInv'
+    <3>1. CASE /\ Len(buffer) < BufCapacity
+               /\ buffer' = Append(buffer, p)
+               /\ NotifyOther(waitSeqC)
+               /\ UNCHANGED waitSeqP
+      BY <3>1, <2>1, TailTransitivityIsInjective
+      DEF NotifyOther, IsInjective
+    <3>2. CASE /\ Len(buffer) = BufCapacity
+               /\ Wait(waitSeqP, p)
+               /\ UNCHANGED waitSeqC
+      \* Put below so TLAPS knows about t \notin Range(waitSeqP)
+      BY <3>2, <2>1, AppendTransitivityIsInjective
+      DEF Wait, IsInjective, Put
+    <3>3. QED
+      BY <2>1, <3>1, <3>2 DEF Put
+  <2>2. ASSUME NEW c \in Consumers,
+               Get(c)
+        PROVE  TypeInv'
+    <3>1. CASE /\ buffer # <<>>
+               /\ buffer' = Tail(buffer)
+               /\ NotifyOther(waitSeqP)
+               /\ UNCHANGED waitSeqC
+      BY <3>1, <2>2, TailTransitivityIsInjective
+      DEF NotifyOther, IsInjective
+    <3>2. CASE /\ buffer = <<>>
+               /\ Wait(waitSeqC, c)
+               /\ UNCHANGED waitSeqP
+      \* Get below so TLAPS knows about t \notin Range(waitSeqC)
+      BY <3>2, <2>2, AppendTransitivityIsInjective
+      DEF Wait, IsInjective, Get
+    <3>3. QED
+      BY <2>2, <3>1, <3>2 DEF Get
+  <2>3. CASE UNCHANGED vars
+    BY <2>3 DEF vars
+  <2>4. QED
+    BY <2>1, <2>2, <2>3 DEF Next
+<1>3. QED BY <1>1, <1>2, PTL DEF Spec
+
+-----------------------------------------------------------------------------
 =============================================================================
diff --git a/README.md b/README.md
index 1e1b655..7413979 100644
--- a/README.md
+++ b/README.md
@@ -13,6 +13,10 @@ This tutorial is work in progress. More chapters will be added in the future. In
 
 --------------------------------------------------------------------------
 
+### v30 (Refinement Fair): Prove TypeInv is an inductive invariant of BlockingQueueFair.
+
+As a first step of proving that ```BlockingQueueFair``` refines ```BlockingQueueSplit```, we once again prove inductiveness of ```TypeInv```.
+
 ### v29 (Refinement Fair): Refine BlockingQueue with BlockingQueueFair spec.
 
 ```BlockingQueueFair``` refines ```BlockingQueueSplit``` by notifying the longest-waiting producer or consumer thread instead of any thread in ```waitC``` or ```waitP```. For that, it uses (ordered) sequences in place of the (unordered) sets.  The refinement mapping is straight forward: ```BlockingQueueSplit!waitC``` and ```waitP``` are refined by the sequences ```waitSeqC``` and ```waitSeqP``` respectively.  TLC checked the refinement mapping for the finite model with the configuration p4c3b3.