v32 (RefinementFair): Prove TypeInv is an inductive invariant of Bloc…

…kingQueueFair.

.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://github.com/tlaplus/tlapm/releases/download/v1.4.5/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

BlockingQueueFair.tla

@@ -1,5 +1,5 @@
 ------------------------- MODULE BlockingQueueFair -------------------------
-EXTENDS Naturals, Sequences, FiniteSets, Functions, SequencesExt
+EXTENDS Naturals, Sequences, FiniteSets, Functions, SequencesExt, SequencesExtTheorems
 
 CONSTANTS Producers,   (* the (nonempty) set of producers                       *)
           Consumers,   (* the (nonempty) set of consumers                       *)
@@ -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
+
+-----------------------------------------------------------------------------
 =============================================================================

README.md

@@ -13,6 +13,10 @@ This tutorial is work in progress. More chapters will be added in the future. In
 
 --------------------------------------------------------------------------
 
+### v32 (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```.
+
 ### v31 (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.