Examples icon indicating copy to clipboard operation
Examples copied to clipboard
verified publisher icon tlaplus

Finite Monotonic

Open lemmy opened this issue 1 year ago • 1 comments

Related to https://github.com/tlaplus/Examples/pull/97

  • Violations of Convergence are missed without GarbageCollect (regardless of state constraint or conjunct to disable Increment)
  • Conjunct to disable Increment causes spurious liveness violation that ends in stuttering (see bottom)
-> % tlc -note SCCRDT.tla -config SCCRDT.tla                     
TLC2 Version 2.20 of Day Month 20?? (rev: 2360829)
Running breadth-first search Model-Checking with fp 55 and seed 1802278425399457922 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 41282] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.24 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /Users/markus/src/TLA/_specs/examples/specifications/FiniteMonotonic/SCCRDT.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11431439590268313249/TLC.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11431439590268313249/Naturals.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11431439590268313249/Sequences.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11431439590268313249/IOUtils.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/IOUtils.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11431439590268313249/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-11431439590268313249/Integers.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module Integers
Semantic processing of module IOUtils
Semantic processing of module SCCRDT
Starting... (2024-10-17 06:45:34)
<<"conf", [D |-> 0, F |-> 0, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 0, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 0, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 0, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 1, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 1, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 1, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 1, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 2, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 2, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 2, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 2, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 3, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 3, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 3, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 3, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 4, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 4, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 4, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 4, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 5, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 5, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 5, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 5, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 6, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 6, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 0, F |-> 6, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 0, F |-> 6, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 1, F |-> 0, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 1, F |-> 0, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 1, F |-> 0, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 1, F |-> 0, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 1, F |-> 1, G |-> FALSE, C |-> FALSE], 13>>
<<"conf", [D |-> 1, F |-> 1, G |-> FALSE, C |-> TRUE], 13>>
<<"conf", [D |-> 1, F |-> 1, G |-> TRUE, C |-> FALSE], 13>>
<<"conf", [D |-> 1, F |-> 1, G |-> TRUE, C |-> TRUE], 13>>
<<"conf", [D |-> 1, F |-> 2, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 1, F |-> 2, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 1, F |-> 2, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 1, F |-> 2, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 1, F |-> 3, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 1, F |-> 3, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 1, F |-> 3, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 1, F |-> 3, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 1, F |-> 4, G |-> FALSE, C |-> FALSE], 13>>
<<"conf", [D |-> 1, F |-> 4, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 1, F |-> 4, G |-> TRUE, C |-> FALSE], 13>>
<<"conf", [D |-> 1, F |-> 4, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 1, F |-> 5, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 1, F |-> 5, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 1, F |-> 5, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 1, F |-> 5, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 1, F |-> 6, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 1, F |-> 6, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 1, F |-> 6, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 1, F |-> 6, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 2, F |-> 0, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 2, F |-> 0, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 2, F |-> 0, G |-> TRUE, C |-> FALSE], 13>>
<<"conf", [D |-> 2, F |-> 0, G |-> TRUE, C |-> TRUE], 13>>
<<"conf", [D |-> 2, F |-> 1, G |-> FALSE, C |-> FALSE], 13>>
<<"conf", [D |-> 2, F |-> 1, G |-> FALSE, C |-> TRUE], 13>>
<<"conf", [D |-> 2, F |-> 1, G |-> TRUE, C |-> FALSE], 13>>
<<"conf", [D |-> 2, F |-> 1, G |-> TRUE, C |-> TRUE], 13>>
<<"conf", [D |-> 2, F |-> 2, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 2, F |-> 2, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 2, F |-> 2, G |-> TRUE, C |-> FALSE], 13>>
<<"conf", [D |-> 2, F |-> 2, G |-> TRUE, C |-> TRUE], 13>>
<<"conf", [D |-> 2, F |-> 3, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 2, F |-> 3, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 2, F |-> 3, G |-> TRUE, C |-> FALSE], 13>>
<<"conf", [D |-> 2, F |-> 3, G |-> TRUE, C |-> TRUE], 13>>
<<"conf", [D |-> 2, F |-> 4, G |-> FALSE, C |-> FALSE], 13>>
<<"conf", [D |-> 2, F |-> 4, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 2, F |-> 4, G |-> TRUE, C |-> FALSE], 13>>
<<"conf", [D |-> 2, F |-> 4, G |-> TRUE, C |-> TRUE], 13>>
<<"conf", [D |-> 2, F |-> 5, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 2, F |-> 5, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 2, F |-> 5, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 2, F |-> 5, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 2, F |-> 6, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 2, F |-> 6, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 2, F |-> 6, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 2, F |-> 6, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 3, F |-> 0, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 3, F |-> 0, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 3, F |-> 0, G |-> TRUE, C |-> FALSE], 13>>
<<"conf", [D |-> 3, F |-> 0, G |-> TRUE, C |-> TRUE], 13>>
<<"conf", [D |-> 3, F |-> 1, G |-> FALSE, C |-> FALSE], 13>>
<<"conf", [D |-> 3, F |-> 1, G |-> FALSE, C |-> TRUE], 13>>
<<"conf", [D |-> 3, F |-> 1, G |-> TRUE, C |-> FALSE], 13>>
<<"conf", [D |-> 3, F |-> 1, G |-> TRUE, C |-> TRUE], 13>>
<<"conf", [D |-> 3, F |-> 2, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 3, F |-> 2, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 3, F |-> 2, G |-> TRUE, C |-> FALSE], 13>>
<<"conf", [D |-> 3, F |-> 2, G |-> TRUE, C |-> TRUE], 13>>
<<"conf", [D |-> 3, F |-> 3, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 3, F |-> 3, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 3, F |-> 3, G |-> TRUE, C |-> FALSE], 13>>
<<"conf", [D |-> 3, F |-> 3, G |-> TRUE, C |-> TRUE], 13>>
<<"conf", [D |-> 3, F |-> 4, G |-> FALSE, C |-> FALSE], 13>>
<<"conf", [D |-> 3, F |-> 4, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 3, F |-> 4, G |-> TRUE, C |-> FALSE], 13>>
<<"conf", [D |-> 3, F |-> 4, G |-> TRUE, C |-> TRUE], 13>>
<<"conf", [D |-> 3, F |-> 5, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 3, F |-> 5, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 3, F |-> 5, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 3, F |-> 5, G |-> TRUE, C |-> TRUE], 0>>
<<"conf", [D |-> 3, F |-> 6, G |-> FALSE, C |-> FALSE], 0>>
<<"conf", [D |-> 3, F |-> 6, G |-> FALSE, C |-> TRUE], 0>>
<<"conf", [D |-> 3, F |-> 6, G |-> TRUE, C |-> FALSE], 0>>
<<"conf", [D |-> 3, F |-> 6, G |-> TRUE, C |-> TRUE], 0>>
Computing initial states...
Finished computing initial states: 0 distinct states generated at 2024-10-17 06:47:24.
Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
  calculated (optimistic):  val = 0.0
0 states generated, 0 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 0.
Finished in 01min 50s at (2024-10-17 06:47:24)

Better exit values: https://github.com/tlaplus/tlaplus/issues/1041

-> % D=3 F=4 G=TRUE C=FALSE tlc -note MCCRDT.tla -config MCCRDT.cfg
TLC2 Version 2.20 of Day Month 20?? (rev: 2360829)
Running breadth-first search Model-Checking with fp 130 and seed 4584290592961789553 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 42208] (Mac OS X 15.0.1 aarch64, Homebrew 11.0.24 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /Users/markus/src/TLA/_specs/examples/specifications/FiniteMonotonic/MCCRDT.tla
Parsing file /Users/markus/src/TLA/_specs/examples/specifications/FiniteMonotonic/CRDT.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14565095515634353915/IOUtils.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/IOUtils.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14565095515634353915/TLC.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14565095515634353915/Naturals.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14565095515634353915/Integers.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14565095515634353915/Sequences.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-14565095515634353915/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Semantic processing of module Naturals
Semantic processing of module CRDT
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module Integers
Semantic processing of module IOUtils
Semantic processing of module MCCRDT
Starting... (2024-10-17 06:52:34)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2024-10-17 06:52:34.
Progress(9) at 2024-10-17 06:52:34: 621 states generated, 100 distinct states found, 0 states left on queue.
Checking temporal properties for the complete state space with 100 total distinct states at (2024-10-17 06:52:34)
Error: Temporal properties were violated.

Error: The following behavior constitutes a counter-example:

State 1: <Initial predicate>
counter = (n1 :> (n1 :> 0 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))

State 2: <S!Next line 34, col 1 to line 34, col 18 of module MCCRDT>
counter = (n1 :> (n1 :> 1 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 0))

State 3: <S!Next line 34, col 1 to line 34, col 18 of module MCCRDT>
counter = (n1 :> (n1 :> 1 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 1))

State 4: <S!Next line 34, col 1 to line 34, col 18 of module MCCRDT>
counter = (n1 :> (n1 :> 1 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 2))

State 5: <S!Next line 34, col 1 to line 34, col 18 of module MCCRDT>
counter = (n1 :> (n1 :> 1 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 3))

State 6: <S!Next line 34, col 1 to line 34, col 18 of module MCCRDT>
counter = (n1 :> (n1 :> 2 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 3))

State 7: <S!Next line 34, col 1 to line 34, col 18 of module MCCRDT>
counter = (n1 :> (n1 :> 3 @@ n2 :> 0) @@ n2 :> (n1 :> 0 @@ n2 :> 3))

State 8: <S!Next line 34, col 1 to line 34, col 18 of module MCCRDT>
counter = (n1 :> (n1 :> 3 @@ n2 :> 3) @@ n2 :> (n1 :> 0 @@ n2 :> 3))

State 9: Stuttering
Finished checking temporal properties in 00s at 2024-10-17 06:52:34
621 states generated, 100 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 9.
Finished in 00s at (2024-10-17 06:52:34)

lemmy avatar Oct 17 '24 13:10 lemmy

@muenchnerkindl What's your feeling? Can TLAPS (with the enablement branch) prove the liveness property Convergence given the specified fairness constraint?

https://github.com/tlaplus/Examples/blob/3debf309d1d1afe33baca0f20f93821737b0307c/specifications/FiniteMonotonic/CRDT.tla

lemmy avatar Oct 17 '24 18:10 lemmy

@muenchnerkindl What's your feeling? Can TLAPS (with the enablement branch) prove the liveness property Convergence given the specified fairness constraint?

https://github.com/tlaplus/Examples/blob/3debf309d1d1afe33baca0f20f93821737b0307c/specifications/FiniteMonotonic/CRDT.tla

lemmy avatar Jan 06 '25 17:01 lemmy

Interesting challenge! I believe that TLAPS should be able to prove the property but I think the specification is not the one you want. Since <<Increment(n)>>_vars is always enabled, so is <<Next>>_vars, and therefore the spec implies that there must be infinitely many non-stuttering steps. On the other hand the conjunct \A n,o \in Node : <>[][Gossip(n,o)]_vars implies eventual stuttering, so the spec is just equivalent to FALSE. (Ah, yes, the joy of not machine-closed specifications!) I think you want the fairness condition

/\ \A n,o \in Node : WF_vars(Gossip(n,o))
/\ <>[][\E n,o \in Node : Gossip(n,o)]_vars

(Alternatively, you can leave the second conjunct as it is, but I find the above a little easier to understand.)

I'll try to find some time to prove the property for the modified spec.

muenchnerkindl avatar Jan 07 '25 20:01 muenchnerkindl

@muenchnerkindl wrote the following TLAPS proof:

------------------------------- MODULE CRDT ---------------------------------

EXTENDS Naturals, FiniteSets, NaturalsInduction, TLAPS

CONSTANT Node
ASSUME NodeAssumption == IsFiniteSet(Node)

VARIABLE counter
vars == counter

TypeOK == counter \in [Node -> [Node -> Nat]]

Safety == \A n, o \in Node : counter[n][n] >= counter[o][n]

Monotonic == \A n, o \in Node : counter'[n][o] >= counter[n][o]

Monotonicity == [][Monotonic]_counter

Convergence == []<>(\A n, o \in Node : counter[n] = counter[o])

Init == counter = [n \in Node |-> [o \in Node |-> 0]]

Increment(n) == counter' = [counter EXCEPT ![n][n] = @ + 1]

Gossip(n, o) ==
  LET Max(a, b) == IF a > b THEN a ELSE b IN
  counter' = [
    counter EXCEPT ![o] = [
      nodeView \in Node |->
        Max(counter[n][nodeView], counter[o][nodeView])
      ]
    ]

Next ==
  \/ \E n \in Node : Increment(n)
  \/ \E n, o \in Node : Gossip(n, o)

Spec ==
  /\ Init
  /\ [][Next]_counter

-----------------------------------------------------------------------------
(***************************************************************************)
(* Proofs of safety properties.                                            *)
(***************************************************************************)

THEOREM TypeCorrect == Spec => []TypeOK
<1>1. Init => TypeOK
  BY DEF Init, TypeOK
<1>2. TypeOK /\ [Next]_vars => TypeOK'
  BY DEF TypeOK, Next, Increment, Gossip, vars
<1>. QED  BY <1>1, <1>2, PTL DEF Spec, vars


THEOREM Safe == Spec => []Safety
<1>1. Init => Safety
  BY DEF Init, Safety
<1>2. TypeOK /\ Safety /\ [Next]_vars => Safety'
  BY DEF TypeOK, Safety, Next, Increment, Gossip, vars
<1>. QED  BY <1>1, <1>2, TypeCorrect, PTL DEF Spec, vars

THEOREM Spec => Monotonicity
<1>1. TypeOK /\ [Next]_vars => [Monotonic]_vars
  BY DEF TypeOK, Safety, Next, Increment, Gossip, vars, Monotonic
<1>. QED  BY <1>1, TypeCorrect, PTL DEF Spec, Monotonicity, vars

-----------------------------------------------------------------------------
(***************************************************************************)
(* Fairness and liveness assumptions.                                      *)
(* We assume that Gossip actions will eventually occur when enabled, and   *)
(* that from some point onwards, only Gossip actions will be performed.    *)
(* In other words, incrementation of counters happens only finitely often. *)
(* Note that the second conjunct is not a standard fairness condition,     *)
(* yet the overall specification is machine closed.                        *)
(***************************************************************************)
Fairness ==
    /\ \A n, o \in Node : WF_vars(Gossip(n,o))
    /\ <>[][\E n, o \in Node : Gossip(n,o)]_vars

FairSpec ==
  /\ Spec
  /\ Fairness  

-----------------------------------------------------------------------------
(***************************************************************************)
(* Auxiliary definitions in preparation for the liveness proof.            *)
(* Sum the values of a vector of natural numbers indexed by Node.          *)
(* This operator could be defined using a Fold, but since there is no      *)
(* library of theorems about Fold, we define it directly from scratch.     *)
(* We then state a few facts about Sum, without proof.                     *)
(***************************************************************************)
Sum(f) ==
  LET SumS[S \in SUBSET Node] == 
          IF S = {} THEN 0
          ELSE LET x == CHOOSE x \in S : TRUE
               IN  f[x] + SumS[S \ {x}]
  IN  SumS[Node]

LEMMA SumType ==
  ASSUME NEW f \in [Node -> Nat]
  PROVE  Sum(f) \in Nat
PROOF OMITTED

LEMMA SumIsZero ==
  ASSUME NEW f \in [Node -> Nat]
  PROVE  Sum(f) = 0 <=> \A x \in Node : f[x] = 0
PROOF OMITTED

LEMMA SumWeaklyMonotonic ==
  ASSUME NEW f \in [Node -> Nat], NEW g \in [Node -> Nat],
         \A x \in Node : f[x] <= g[x]
  PROVE  Sum(f) <= Sum(g)
PROOF OMITTED

LEMMA SumStronglyMonotonic ==
  ASSUME NEW f \in [Node -> Nat], NEW g \in [Node -> Nat],
         \A x \in Node : f[x] <= g[x],
         \E x \in Node : f[x] < g[x]
  PROVE  Sum(f) < Sum(g)
PROOF OMITTED

-----------------------------------------------------------------------------
(***************************************************************************)
(* Proof of the convergence property for the specification with fairness.  *)
(***************************************************************************)

\* First prove when <<Gossip(n,o)>>_vars is enabled.

LEMMA EnabledGossip ==
  ASSUME NEW n \in Node, NEW o \in Node, TypeOK
  PROVE  (ENABLED <<Gossip(n,o)>>_vars) <=>
         \E v \in Node : counter[o][v] < counter[n][v]
<1>. USE DEF TypeOK
<1>1. ASSUME ENABLED <<Gossip(n,o)>>_vars
             PROVE   \E v \in Node : counter[o][v] < counter[n][v]
  <2>. CASE <<Gossip(n,o)>>_counter
    BY DEF Gossip
  <2>. QED  BY <1>1, ExpandENABLED DEF Gossip, vars     
<1>2. ASSUME NEW v \in Node, counter[o][v] < counter[n][v]
      PROVE  ENABLED <<Gossip(n,o)>>_vars
  <2>. DEFINE Max(a, b) == IF a > b THEN a ELSE b
              ctr == [counter EXCEPT ![o] =
                        [nv \in Node |-> Max(counter[n][nv], counter[o][nv])]]
  <2>. ctr[o][v] # counter[o][v]
    BY <1>2
  <2>. QED  BY ExpandENABLED, Zenon DEF Gossip, vars
<1>. QED  BY <1>1, <1>2

(***************************************************************************)
(* Definition of the termination measure.                                  *)
(* Distance(o) sums the differences between node o's knowledge of the      *)
(* counters of other nodes and their true values.                          *)
(* Measure sums Distance(o), for all nodes o.                              *)
(* We prove elementary facts about the termination measure and in          *)
(* particular show how the Gossip action interacts with it.                *)
(***************************************************************************)
DistFun(o) == [n \in Node |-> counter[n][n] - counter[o][n]]

Distance(o) == Sum(DistFun(o))

Measure == Sum([o \in Node |-> Distance(o)])

LEMMA MeasureType ==
  ASSUME TypeOK, Safety
  PROVE  /\ \A o \in Node : DistFun(o) \in [Node -> Nat]
         /\ \A o \in Node : Distance(o) \in Nat
         /\ Measure \in Nat
<1>. ASSUME NEW o \in Node
     PROVE  DistFun(o) \in [Node -> Nat]
  BY DEF TypeOK, Safety, DistFun
<1>. QED  BY SumType, Zenon DEF Distance, Measure

\* We need a copy of the above theorem where all variables are primed.
\* One could derive this from MeasureType using PTL, but we just copy
\* and paste the proof.
LEMMA MeasureTypePrime ==
  ASSUME TypeOK', Safety'
  PROVE  /\ \A o \in Node : DistFun(o)' \in [Node -> Nat]
         /\ \A o \in Node : Distance(o)' \in Nat
         /\ Measure' \in Nat
<1>. ASSUME NEW o \in Node
     PROVE  DistFun(o)' \in [Node -> Nat]
  BY DEF TypeOK, Safety, DistFun
<1>. QED  BY SumType, Zenon DEF Distance, Measure

\* The termination measure is zero iff all nodes agree on the 
\* counter values of all nodes.
LEMMA MeasureIsZero ==
  ASSUME TypeOK, Safety
  PROVE  /\ \A o \in Node : Distance(o) = 0 
                 <=> \A n \in Node : counter[o][n] = counter[n][n]
         /\ Measure = 0
            <=> \A v,w,n \in Node : counter[v][n] = counter[w][n]
<1>1. ASSUME NEW o \in Node, Distance(o) = 0, NEW n \in Node
      PROVE  counter[o][n] = counter[n][n]
  BY <1>1, MeasureType, SumIsZero DEF Distance, DistFun, TypeOK, Safety
<1>2. ASSUME NEW o \in Node, \A n \in Node : counter[o][n] = counter[n][n]
      PROVE  Distance(o) = 0
  BY <1>2, MeasureType, SumIsZero DEF Distance, DistFun, TypeOK
<1>3. ASSUME Measure = 0, NEW v \in Node, NEW w \in Node, NEW n \in Node
      PROVE  counter[v][n] = counter[w][n]
  BY <1>1, <1>3, MeasureType, SumIsZero DEF Measure
<1>4. ASSUME \A v,w,n \in Node : counter[v][n] = counter[w][n]
      PROVE  Measure = 0
  BY <1>2, <1>4, MeasureType, SumIsZero DEF Measure
<1>. QED  BY <1>1, <1>2, <1>3, <1>4

\* A Gossip action will never increase the measure.
LEMMA GossipDoesntIncreaseMeasure ==
  ASSUME TypeOK, TypeOK', Safety, Safety',
         [\E n,o \in Node : Gossip(n,o)]_vars
  PROVE  /\ \A v,w \in Node : DistFun(v)'[w] <= DistFun(v)[w]
         /\ \A v \in Node : Distance(v)' <= Distance(v)
         /\ Measure' <= Measure
<1>1. CASE \E n,o \in Node : Gossip(n,o)
  <2>. ASSUME NEW v \in Node, NEW w \in Node
        PROVE  DistFun(v)'[w] <= DistFun(v)[w]
    BY <1>1 DEF Gossip, TypeOK, Safety, DistFun
  <2>. QED  
    BY SumWeaklyMonotonic, MeasureType, MeasureTypePrime, Zenon
       DEF Distance, Measure
<1>2. CASE UNCHANGED vars
  BY <1>2, MeasureType DEF DistFun, Distance, Measure, vars
<1>. QED  BY <1>1, <1>2

\* A non-stuttering Gossip action decreases the measure.
LEMMA GossipDecreasesMeasure ==
  ASSUME TypeOK, TypeOK', Safety, Safety',
         <<\E n,o \in Node : Gossip(n,o)>>_vars
  PROVE  Measure' < Measure
<1>. PICK n \in Node, o \in Node : <<Gossip(n,o)>>_vars
  OBVIOUS
<1>1. PICK v \in Node : counter[o][v] < counter[n][v]
  BY DEF Gossip, vars, TypeOK
<1>2. DistFun(o)'[v] < DistFun(o)[v]
  BY <1>1 DEF Gossip, vars, TypeOK, Safety, DistFun
<1>. QED
  BY <1>2, GossipDoesntIncreaseMeasure, SumStronglyMonotonic,
     MeasureType, MeasureTypePrime, Zenon 
     DEF Distance, Measure

(***************************************************************************)
(* We now prove convergence for the tail of the behavior in which only     *)
(* Gossip actions may occur. For convenience, we define a TLA+             *)
(* specification characterizing this eventual behavior.                    *)
(***************************************************************************)

OGSpec ==
  /\ [](TypeOK /\ Safety)
  /\ [][\E n, o \in Node : Gossip(n,o)]_vars
  /\ [](\A n, o \in Node : WF_vars(Gossip(n,o)))

\* The following is the main liveness theorem. Its proof is quite tedious
\* because of a delicate interplay of predicate and temporal logic reasoning.
THEOREM OGLiveness == OGSpec => <>(\A n, o \in Node : counter[n] = counter[o])
<1>. DEFINE Q == \A n, o \in Node : counter[n] = counter[o]
            P(m) == Measure = m
            L(m) == [](P(m) => <>Q)
<1>1. ASSUME NEW m \in Nat,
             \* must explicitly "box" the following assumption,
             \* otherwise PTL reasoning fails below.
             [](\A k \in 0 .. (m-1) : OGSpec => L(k))
      PROVE  [](OGSpec => L(m))
  <2>. DEFINE OGNext == \E n, o \in Node : Gossip(n,o)
  <2>1. CASE m = 0
    <3>1. TypeOK /\ Safety /\ P(m) => Q
      BY <2>1, MeasureIsZero DEF TypeOK
    <3>. QED  BY <3>1, PTL DEF OGSpec
  <2>2. CASE m > 0
    <3>1. OGSpec => [](P(m) => [](\E k \in 0 .. m : P(k)))
      <4>1. TypeOK /\ Safety /\ P(m) => \E k \in 0 .. m : P(k)
        BY MeasureType
      <4>2. /\ TypeOK /\ Safety /\ TypeOK' /\ Safety' 
            /\ \E k \in 0 .. m : P(k)
            /\ [OGNext]_vars
            => (\E k \in 0 .. m : P(k))'
        BY MeasureTypePrime, GossipDoesntIncreaseMeasure
      <4>. QED  BY <4>1, <4>2, PTL DEF OGSpec
    <3>5. OGSpec => [](P(m) /\ <><<OGNext>>_vars => <> \E k \in 0 .. (m-1) : P(k))
      <4>1. /\ TypeOK /\ Safety /\ TypeOK' /\ Safety'
            /\ \E k \in 0 .. m : P(k)
            /\ <<OGNext>>_vars
            => (\E k \in 0 .. (m-1) : P(k))'
        BY MeasureTypePrime, GossipDecreasesMeasure
      <4>. QED  BY <3>1, <4>1, PTL DEF OGSpec
    <3>6. OGSpec => [](P(m) /\ [][~OGNext]_vars => <> \E k \in 0 .. (m-1) : P(k))
      <4>. DEFINE C(n,o) == counter[o][n] < counter[n][n]
      <4>1. OGSpec /\ [][~OGNext]_vars /\ P(m) => \E u,v \in Node : []C(u,v)
        <5>1. TypeOK /\ Safety /\ P(m) => \E u,v \in Node : C(u,v)
          <6>. SUFFICES ASSUME TypeOK, Safety, P(m)
                        PROVE  \E n,o \in Node : C(n,o)
            OBVIOUS
          <6>1. PICK a,b,c \in Node : counter[a][c] # counter[b][c]
            BY <2>2, MeasureType, MeasureIsZero
          <6>2. CASE counter[a][c] < counter[b][c]
            BY <6>1, <6>2 DEF Safety, TypeOK
          <6>3. CASE counter[b][c] < counter[a][c]
            BY <6>1, <6>3 DEF Safety, TypeOK
          <6>. QED  BY <6>1, <6>2, <6>3 DEF TypeOK
        <5>2. OGSpec /\ [][~OGNext]_vars /\ P(m) => \E u,v \in Node : C(u,v)
          BY <5>1, PTL DEF OGSpec
        <5>3. OGSpec /\ [][~OGNext]_vars => \A u,v \in Node : C(u,v) => []C(u,v)
          <6>. SUFFICES ASSUME NEW u \in Node, NEW v \in Node
                        PROVE  C(u,v) /\ [][OGNext]_vars /\ [][~OGNext]_vars => []C(u,v)
            BY DEF OGSpec
          <6>. C(u,v) /\ [OGNext]_vars /\ [~OGNext]_vars => C(u,v)'
            BY DEF vars
          <6>. QED  BY PTL
        <5>. QED  BY <5>2, <5>3
      <4>2. OGSpec /\ [](\E k \in 0 .. m : P(k)) /\ (\E u,v \in Node : []C(u,v))
            => <> \E k \in 0 .. (m-1) : P(k)
        <5>. SUFFICES 
               ASSUME NEW u \in Node, NEW v \in Node
               PROVE  OGSpec /\ [](\E k \in 0 .. m : P(k)) /\ []C(u,v)
                      => <> \E k \in 0 .. (m-1) : P(k)
          OBVIOUS
        <5>1. TypeOK /\ C(u,v) => ENABLED <<Gossip(u,v)>>_vars
          BY EnabledGossip
        <5>2. /\ TypeOK /\ TypeOK' /\ Safety /\ Safety'
              /\ \E k \in 0 .. m : P(k)
              /\ <<Gossip(u,v)>>_vars
              => (\E k \in 0 .. (m-1) : P(k))'
          BY MeasureTypePrime, GossipDecreasesMeasure
        <5>3. OGSpec => WF_vars(Gossip(u,v))
          <6>1. (\A n,o \in Node : WF_vars(Gossip(n,o))) => WF_vars(Gossip(u,v))
            OBVIOUS
          <6>. QED  BY <6>1, PTL DEF OGSpec
        <5>. QED  BY <5>1, <5>2, <5>3, PTL DEF OGSpec
      <4>. HIDE DEF OGNext, P, C
      <4>3. OGSpec /\ [][~OGNext]_vars /\ P(m) /\ [](\E k \in 0 .. m : P(k))
            => <>(\E k \in 0 .. (m-1) : P(k))
         BY <4>1, <4>2
      <4>. QED  BY <3>1, <4>3, PTL DEF OGSpec
    <3>7. OGSpec => [](P(m) =>  <> \E k \in 0 .. (m-1) : P(k))
      BY <3>5, <3>6, PTL
    <3>8. OGSpec => []((\E k \in 0 .. (m-1) : P(k)) => <>Q)
      <4>1. (\A k \in 0 .. (m-1) : OGSpec => L(k)) 
            => (OGSpec => [](\A k \in 0 .. (m-1) : P(k) => <>Q))
        OBVIOUS
      <4>2. (\A k \in 0 .. (m-1) : P(k) => <>Q) 
            => ((\E k \in 0 .. (m-1) : P(k)) => <>Q)
        OBVIOUS
      <4>. QED  BY <1>1, <4>1, <4>2, PTL
    <3>. QED  BY <3>7, <3>8, PTL
  <2>. QED  BY <2>1, <2>2
<1>. DEFINE S(m) == [](OGSpec => L(m))
\* The following step just commutes [] and \A in the assumption of <1>1
\* so that we can apply the induction theorem in the following step.
<1>2. ASSUME NEW m \in Nat,
             \A k \in 0 .. (m-1) : S(k)
      PROVE  S(m)
  BY <1>1
<1>3. \A m \in Nat : S(m)
  <2>. HIDE DEF S
  <2>. QED  BY <1>2, GeneralNatInduction, Isa
\* Now turn the outermost universal quantifier into an existential quantifier
\* on the left-hand side of the consequent.
<1>4. OGSpec => []((\E m \in Nat : P(m)) => <>Q)
  <2>1. (\A m \in Nat : P(m) => <> Q) => ((\E m \in Nat : P(m)) => <>Q)
    OBVIOUS
  <2>2. [](\A m \in Nat : P(m) => <> Q) => []((\E m \in Nat : P(m)) => <>Q)
    BY <2>1, PTL
  <2>3. ASSUME NEW m \in Nat
        PROVE  OGSpec => L(m)
    <3>1. S(m)
      BY <1>3
    <3>. QED  BY <3>1, PTL
  <2>. QED  BY <1>3, <2>2, <2>3
\* Clearly P(m) must hold for some natural number initially.
<1>5. OGSpec => \E m \in Nat : P(m)
  <2>. TypeOK /\ Safety => \E m \in Nat : P(m)
    BY MeasureType
  <2>. QED  BY PTL DEF OGSpec
<1>. QED  BY <1>4, <1>5, PTL

\* The final theorem is a simple corollary.
THEOREM Liveness == FairSpec => Convergence
<1>1. (\A n,o \in Node : WF_vars(Gossip(n,o))) =>
      [](\A n,o \in Node : WF_vars(Gossip(n,o)))
  \* Tedious proof of an "obvious" fact, due to interplay of first-order 
  \* and temporal reasoning. Could this be proved automatically?
  <2>1. ASSUME NEW n \in Node, NEW o \in Node
        PROVE  WF_vars(Gossip(n,o)) => []WF_vars(Gossip(n,o))
    BY PTL
  <2>. QED  BY <2>1, Isa
<1>. QED
  BY <1>1, TypeCorrect, Safe, OGLiveness, PTL 
     DEF FairSpec, OGSpec, Fairness, Convergence

=============================================================================

lemmy avatar Feb 11 '25 00:02 lemmy

Closed in favor of https://github.com/tlaplus/Examples/pull/155

lemmy avatar Feb 12 '25 23:02 lemmy