From b3dfc3f45611bac60e16cb165c4ef19063fcd8d7 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 31 Oct 2024 11:28:55 -0700 Subject: [PATCH] Add a simpler variant of the MonotonicReduction that just drops the common prefix but leaves the Terms untouched. Signed-off-by: Markus Alexander Kuppe --- tla/consensus/MCabs.tla | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) diff --git a/tla/consensus/MCabs.tla b/tla/consensus/MCabs.tla index 1d9c95b4449d..e872bb922733 100644 --- a/tla/consensus/MCabs.tla +++ b/tla/consensus/MCabs.tla @@ -87,11 +87,20 @@ MaxDivergence == \A i, j \in Servers : Abs(Len(cLogs[i]) - Len(cLogs[j])) <= 2 -MonotonicReduction == - LET TailFrom(seq, idx) == SubSeq(seq, idx + 1, Len(seq)) - \* Find the longest common prefix of all logs and drop it from all logs. - \* We realign the terms in the remaining suffixes to start at StartTerm. - commonPrefixBound == Len(LongestCommonPrefix(Range(cLogs))) +----- + +TailFrom(seq, idx) == + SubSeq(seq, idx + 1, Len(seq)) + +MonotonicReductionLongestCommonPrefix == + \* Find the longest common prefix of all logs and drop it from all logs. + LET commonPrefixBound == Len(LongestCommonPrefix(Range(cLogs))) + IN [ s \in Servers |-> TailFrom(cLogs[s], commonPrefixBound) ] + +MonotonicReductionLongestCommonPrefixAndTerms == + \* Find the longest common prefix of all logs and drop it from all logs. + \* We also realign the terms in the remaining suffixes to start at StartTerm. + LET commonPrefixBound == Len(LongestCommonPrefix(Range(cLogs))) minTerm == \* 3) The minimum term out of all minima. Min({ @@ -103,6 +112,7 @@ MonotonicReduction == \cup {0}) : s \in Servers}) IN [ s \in Servers |-> [ i \in 1..Len(cLogs[s]) - commonPrefixBound |-> - cLogs[s][i + commonPrefixBound] - minTerm ] ] +MonotonicReduction == + MonotonicReductionLongestCommonPrefixAndTerms ==== \ No newline at end of file