----------------------------- MODULE Increment -----------------------------
(***************************************************************************)
(* This file contains the abstract program Increment in Figure 3.5 of the  *)
(* book "A Science of Concurrent Programs".                                *)
(***************************************************************************)

EXTENDS Integers, FiniteSets,  TLAPS
   (************************************************************************)
   (* The module FiniteSets defines the operator Cardinality, which is     *)
   (* written # in the book.                                               *)
   (************************************************************************)
CONSTANT Procs
N == Cardinality(Procs)

VARIABLES x, pc, t

Init == /\ x = 0
        /\ t = [p \in Procs |-> 0]
        /\ pc = [p \in Procs |-> "a"]

aStep(p) == /\ pc[p] = "a"
            /\ x' = x
            /\ t' = [t EXCEPT ![p] = x]
            /\ pc' = [pc EXCEPT ![p] = "b"]

bStep(p) == /\ pc[p] = "b"
            /\ x' = t[p] + 1
            /\ t' = t
            /\ pc' = [pc EXCEPT ![p] = "done"]
            
PgmStep == \E p \in Procs : aStep(p) \/ bStep(p)            

Stutter == /\ \A p \in Procs: pc[p] = "done"
           /\ UNCHANGED <<x, t, pc>>
              (*************************************************************)
              (* UNCHANGED exp is defined to equals exp', so               *)
              (*                                                           *)
              (*     UNCHANGED <<x, t, pc>>                                *)
              (*                                                           *)
              (* is equivalent to                                          *)
              (*                                                           *)
              (*   <<x', t', pc'>> = <<x, t, pc>>.                         *)
              (*                                                           *)
              (* However, when evaluating a next-state action, the first   *)
              (* time TLC encounters a primed variable like x' must        *)
              (* normally be in an expression of the form x' = ...  .  So, *)
              (* we would have to write it as                              *)
              (*                                                           *)
              (*    (x' = x) /\ (t' = t) /\ (pc' = pc)                     *)
              (*                                                           *)
              (* But since this is a common idiom, TLC will accept the     *)
              (* version written with UNCHANGED.                           *)
              (*                                                           *)
              (*************************************************************)

Next == PgmStep \/ Stutter
------------------------------------------------------------------------------
(***************************************************************************)
(* The definitions of TypeOK, NumberDone, and Inv are the same as in the   *)
(* book.                                                                   *)
(***************************************************************************)
TypeOK == /\ x \in 0..N
          /\ t \in [Procs -> 0..N]
          /\ pc \in [Procs -> {"a","b","done"}]
          
NumberDone == Cardinality({i \in Procs : pc[i] = "done"})

Inv == /\ TypeOK
       /\ \A i \in Procs : (pc[i] = "b") => (t[i] =< NumberDone)
       /\ x \leq NumberDone   
----------------------------------------------------------------------------

 INSTANCE FiniteSetTheorems
 INSTANCE Functions
 
 (**************************************************************************)
 (*  We assume that Procs is a finite non-empty set.  An AXIOM is a        *)
 (*  THEOREM that has no proof.                                            *)
 (**************************************************************************)
 AXIOM ProcsFinite == IsFiniteSet(Procs) /\ (Procs # {})
 vars == <<x, t, pc>>
 
THEOREM Next /\ Inv => Inv' 
  <1>1.  ASSUME NEW p \in Procs, aStep(p), Inv
         PROVE  Inv'
   
\*   BY <1>1 DEF aStep, Inv, TypeOK, NumberDone


  (*************************************************************************)
  (* The proof is split into four steps, one for each conjunct Q in the    *)
  (* definition of Inv.  The step for conjunct Q asserts that for an       *)
  (* arbitrary process `p', aStep(p) /\ Inv implies Q'.  The proof of    *)
  (* the second conjunct is the only one that needs to be further          *)
  (* decomposed.                                                           *)
  (*************************************************************************)
  <2>1. TypeOK'
    BY <1>1 DEF aStep, Inv, TypeOK
  <2>2. \A i \in Procs : (pc'[i] = "b") => (t'[i] =< NumberDone')
   
    BY <1>1 DEF aStep, Inv, TypeOK,  NumberDone   
(*************** 
    <3>1. SUFFICES ASSUME NEW i \in Procs, pc'[i] = "b"
                   PROVE  t'[i] =< NumberDone'
      OBVIOUS
    <3>2. NumberDone' = NumberDone
      (*********************************************************************)
      (* aStep(p) implies (i) pc'[j]=pc[j] for all j\in Procs except j =    *)
      (* p, and (ii) pc[p] and pc'[p] are both # "done".          *)
      (*********************************************************************)
      (*********************************************************************)
      (* TLAPS doesn't need the following proof.  It can prove it by:      *)
      (*    BY <1>1 DEF aStep, Inv, TypeOK, Procs, NumberDone                *)
      (*********************************************************************)
    <3>3. CASE i = p
    <3>4. CASE i # p
      <4>1. (t'[i] = t[i] /\ pc'[i] = pc[i])
        BY <1>1, <3>4  DEF aStep, Inv,  TypeOK
      <4>2. pc[i] = "b"
        BY <4>1, <3>1
      <4>3. t[i] =< NumberDone
        BY <4>2, <1>1 DEF Inv
      <4>4. QED
        BY <4>1, <4>3, <3>2 
    <3>5. QED
      BY <3>3, <3>4    
 ******************)                           
  <2>3. x' \leq NumberDone'
    BY <1>1 DEF aStep, Inv, NumberDone
  <2>4. QED
    BY <2>1, <2>2, <2>3  DEF Inv 

      
<1>2. ASSUME NEW p \in Procs, bStep(p), Inv
      PROVE  Inv'
<1>3. ASSUME Stutter, Inv
      PROVE Inv'
  BY <1>3 DEF Stutter, Inv, TypeOK, NumberDone, vars
  
<1>4. QED
  BY <1>1, <1>2, <1>3 DEF Next, PgmStep
(***************************************************************************)
(* We need the following two simple properties of the cardinality of       *)
(* finite sets.  I expect they can be proved from theorems in the standard *)
(* TLAPS module FiniteSetTheorems.  Since we're interested in the          *)
(* algorithm, not in proving this kind of simple property, I haven't done  *)
(* that.                                                                   *)
(***************************************************************************)
THEOREM Lemma1 == ASSUME NEW S, IsFiniteSet(S),
                         NEW T, T \subseteq S 
                  PROVE  /\ Cardinality(S) \in Nat
                         /\ IsFiniteSet(T)
                         /\ Cardinality(T) \in 0..Cardinality(S)
                         /\ (T # S) => (Cardinality(T) < Cardinality(S))
  BY   FS_Subset, FS_CardinalityType

THEOREM Lemma2 == ASSUME NEW S, IsFiniteSet(S),
                         NEW e, e \notin S
                  PROVE  Cardinality(S \cup {e}) = Cardinality(S) + 1

BY FS_AddElement

(***************************************************************************)
(* Here is a proof of the second assertion of (3.10) of the book, which is *)
(* condition I2 for the Increment program.  This is the proof that I       *)
(* originally wrote.  What happens very often when writing a proof is that *)
(* the proof of a step fails, so I decompose it into simpler steps.  The   *)
(* decomposed proof succeeds and everything is fine.  However, I may not   *)
(* notice that the decomposed proof uses one or more facts or definitions  *)
(* that I didn't use when trying to write the original proof of the step.  *)
(* And often, the decomposition isn't necessary because TLAPS can prove    *)
(* the step with those additional facts or definitions.                    *)
(*                                                                         *)
(* The proof here is the one I originally wrote.  However, I checked       *)
(* whether each decomposition was needed.  A comment such as               *)
(*                                                                         *)
(*     \**** BY <1>2, <2>1 DEF b, Inv, TypeOK, Procs                     *)
(*                                                                         *)
(* after a proof step indicates that TLAPS proves that step with that BY   *)
(* statement, and that the following lower-level proof is unnecessary.     *)
(* For example, the comment after step <1>1 indicates that the proof will  *)
(* still work if that BY is uncommented and everything between it and step *)
(* <1>2 is be removed.  Also, as mentioned in a comment, most of the proof *)
(* of step <1>2 can also be removed.                                       *)
\*(***************************************************************************)
THEOREM Next /\ Inv => Inv'
<1>1. ASSUME NEW p \in Procs, aStep(p), Inv
      PROVE  Inv'
   \**** BY <1>1 DEF aStep, Inv, TypeOK, Procs, NumberDone
  (*************************************************************************)
  (* The proof is split into four steps, one for each conjunct Q in the    *)
  (* definition of Inv.  The step for conjunct Q asserts that for an       *)
  (* arbitrary process `p', aStep(p) /\ Inv implies Q'.  The proof of    *)
  (* the second conjunct is the only one that needs to be further          *)
  (* decomposed.                                                           *)
  (*************************************************************************)
  <2>1. TypeOK'
    BY <1>1 DEF aStep, Inv, TypeOK
  <2>2. \A i \in Procs : (pc'[i] = "b") => (t'[i] =< NumberDone')
    \****    BY <1>1 DEF aStep, Inv, TypeOK, Procs, NumberDone   
    <3>1. SUFFICES ASSUME NEW i \in Procs, pc'[i] = "b"
                   PROVE  t'[i] =< NumberDone'
      OBVIOUS
    <3>2. NumberDone' = NumberDone
      (*********************************************************************)
      (* aStep(p) implies (i) pc'[j]=pc[j] for all j\in Procs except j =    *)
      (* p, and (ii) pc[p] and pc'[p] are both # "done".          *)
      (*********************************************************************)
      (*********************************************************************)
      (* TLAPS doesn't need the following proof.  It can prove it by:      *)
      (*    BY <1>1 DEF aStep, Inv, TypeOK, Procs, NumberDone                *)
      (*********************************************************************)
      <4>1. SUFFICES ASSUME NEW j \in Procs 
                     PROVE  (pc'[j] = "done") \equiv (pc[j] = "done")
        BY DEF NumberDone
      <4>2. (j = p) => (pc[j] = "a")  /\ (pc'[j] = "b")
        BY <1>1  DEF aStep, TypeOK, Inv
      <4>3. (j # p) => (pc'[j] = pc[j]) 
        BY <1>1 DEF aStep,  TypeOK
      <4>4. QED
        BY <4>2, <4>3 DEF NumberDone  
    <3>3. CASE i = p
      <4>1. t'[i] = x
        BY <3>3, <1>1 DEF aStep, Inv, TypeOK
      <4>2. QED
        BY <4>1, <3>2, <1>1 DEF Inv  
    <3>4. CASE i # p
      <4>1. (t'[i] = t[i] /\ pc'[i] = pc[i])
        BY <1>1, <3>4  DEF aStep, Inv,  TypeOK
      <4>2. pc[i] = "b"
        BY <4>1, <3>1
      <4>3. t[i] =< NumberDone
        BY <4>2, <1>1 DEF Inv
      <4>4. QED
        BY <4>1, <4>3, <3>2 
    <3>5. QED
      BY <3>3, <3>4                          
  <2>3. x' \leq NumberDone'
    BY <1>1 DEF aStep, Inv, NumberDone
  <2>4. QED
    BY <2>1, <2>2, <2>3  DEF Inv   

<1>2. ASSUME NEW p \in Procs, bStep(p), Inv
      PROVE  Inv'
  <2>1. N \in Nat /\  NumberDone \in 0..N /\ NumberDone < N
    BY ProcsFinite, Lemma1, <1>2 DEF NumberDone, N, bStep
  <2>2. NumberDone' = NumberDone + 1
    \**** BY <1>2, Inv, ProcsFinite,   Lemma1, Lemma2 
    \**** DEF b, Inv, TypeOK, Procs, NumberDone  
    <3>1. p \notin {i \in Procs : pc[i] = "done"}
      BY <1>2 DEF bStep
    <3>2. {i \in Procs : pc[i] = "done"}' =
              {i \in Procs : pc[i] = "done"} \cup {p}
       BY <1>2, Inv DEF bStep, Inv, TypeOK
    <3>3. IsFiniteSet({i \in Procs : pc[i] = "done"})
       BY  ProcsFinite, Lemma1
    <3>4. QED
       BY <1>2, <3>1, <3>2, <3>3, Lemma2  DEF NumberDone 
  (*************************************************************************)
  (* The rest of the step <1>2 proof proves each conjunct of Inv' as a     *)
  (* separate step.  Stephan Merz observed that this is unnecessary.       *)
  (* TLAPS can at this point prove <1>2 with this step                     *)
  (*                                                                       *)
  (*    <2>3. QED                                                          *)
  (*      BY <1>2, <2>1, <2>2 DEF Inv, b, Procs, TypeOK                  *)
  (*                                                                       *)
  (* I had already observed that it was unnecessary to decompose the       *)
  (* proofs of the remaining level 2 steps, so I left the comments         *)
  (* indicating how each of those steps can be proved with a BY step.      *)
  (*************************************************************************)
  <2>3. TypeOK'
    \**** BY <1>2, <2>1 DEF bStep, Inv, TypeOK, Procs       
    <3>1. /\ t' \in [Procs -> 0..N]
          /\ pc' \in [Procs -> {"a","b","done"}]
      BY <1>2 DEF bStep, Inv, TypeOK
    <3>2. x' \in 0..N
     \**** BY <1>2, <2>1 DEF bStep, Inv, TypeOK, Procs 
      <4>1. t[p] =< NumberDone
        BY <1>2 DEF Inv, bStep
      <4>2. x' = t[p] + 1
        BY <1>2 DEF bStep
      <4>3. QED
        BY <1>2, <2>1, <4>1,  <4>2  DEF Inv, TypeOK
    <3>3. QED
      BY <3>1, <3>2 DEF TypeOK
  <2>4. \A i \in Procs : (pc'[i] = "b") => (t'[i] =< NumberDone')
    \**** BY <1>2, <2>1, <2>2 DEF bStep, Inv, TypeOK
    <3>1. SUFFICES ASSUME NEW i \in Procs, pc[i]' = "b"
                   PROVE  t'[i] =< NumberDone'
      OBVIOUS
    <3>2. CASE i # p
      <4>1. t'[i] = t[i] /\ (pc'[i] = pc[i])
        BY <3>2, <1>2 DEF bStep, Inv, TypeOK
      <4>2. t[i] \in Nat
        BY <1>2, <2>1 DEF Inv, TypeOK
      <4>3. t[i] =< NumberDone
        BY <3>1, <4>1, Inv  DEF Inv
      <4>4. QED
         BY <4>1, <4>2, <4>3, Inv, <2>1, <2>2
    <3>3. CASE i = p
      \*** BY <3>1, <3>3, <1>2 DEF bStep, Inv, TypeOK, Procs
      <4>1. pc'[i] = "done"
       BY <3>3, <1>2 DEF bStep, Inv, TypeOK
      <4>2. QED
         BY <4>1, <3>1
    <3>4. QED
      BY <3>2, <3>3
  <2>5. x' \leq NumberDone'
    \**** BY <1>2, <2>1, <2>2 DEF Inv, bStep, Procs, TypeOK
    <3>1. (t[p] \in Nat) /\ (t[p] =< NumberDone)
      BY <1>2, <2>1 DEF Inv, bStep, TypeOK 
    <3>2. x' = t[p]+1
      BY <1>2 DEF bStep
    <3>3. QED 
       BY <3>1, <3>2, <2>1, <2>2  
  <2>6. QED
    BY <2>3, <2>4, <2>5 DEF Inv

<1>3. ASSUME Stutter, Inv
      PROVE Inv'
  BY <1>3 DEF Stutter, Inv, TypeOK, NumberDone, vars
  
<1>4. QED
  BY <1>1, <1>2, <1>3 DEF Next, PgmStep
=============================================================================
\* Modification History
\* Last modified Mon Oct 07 17:59:03 CEST 2024 by lamport
\* Last modified Mon Oct 07 09:54:41 CEST 2024 by lblam
\* Created Thu May 12 09:39:37 PDT 2022 by lamport
