Wrangling monotonic systems in TLA⁺

------------------------------- MODULE CRDT --------------------------------- EXTENDS Naturals CONSTANT Node VARIABLE counter TypeOK ≜ counter ∈ [ Node → [ Node → ℕ]] Init ≜ counter = [ n ∈ Node ↦ [ o ∈ Node ↦ 0 ]] Increment ( n ) ≜ counter' = [ counter EXCEPT ! Gossip ( n, o ) ∧ UNCHANGED converge Converge ≜ ∧ converge' = TRUE ∧ UNCHANGED counter Next ≜ ∨ ∃ n ∈ Node : Increment ( n ) ∨ ∃ n, o ∈ Node : Gossip ( n, o ) ∨ Converge Fairness ≜ ∀ n, o ∈ Node : WF_vars ( Gossip ( n, o )) Spec ≜ ∧ Init ∧ □[Next]_vars ∧ Fairness ============================================================================= Gossip ( n, o ) ∧ UNCHANGED converge Converge ≜ ∧ converge' = TRUE ∧ UNCHANGED counter GarbageCollect ≜ LET SetMin ( s ) ≜ CHOOSE e ∈ s : ∀ o ∈ s : e ≤ o IN LET Transpose ≜ SetMin ({ counter [ n…