From d28f9e9e2293836261e1dfc38fd86a16aacc6568 Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <github.com@lemmster.de>
Date: Wed, 18 Dec 2024 12:13:15 -0800
Subject: [PATCH] Gather statistics on the number of log entries committed due
 to fast path:

1. Without the fast path
2. With the unanimous fast path
3. With the transitive unanimous fast path.

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
---
 SIMpirateship.cfg |  5 ++---
 SIMpirateship.tla | 39 +++++++++++++++++----------------------
 2 files changed, 19 insertions(+), 25 deletions(-)

diff --git a/SIMpirateship.cfg b/SIMpirateship.cfg
index ee23f5a..f0dfa83 100644
--- a/SIMpirateship.cfg
+++ b/SIMpirateship.cfg
@@ -51,9 +51,8 @@ _PERIODIC
 
 \* CONSTANT
 \*     HighestUnanimity <- StatsHighestUnanimity
-
-\* CONSTRAINT 
-\*     StatsConstraint
+\*     ReceiveVote <- StatsReceiveVote
+\*     ReceiveEntries  <- StatsReceiveEntries
 
 \* POSTCONDITION 
 \*     StatsPostcondition
diff --git a/SIMpirateship.tla b/SIMpirateship.tla
index ff3ef02..3eab9db 100644
--- a/SIMpirateship.tla
+++ b/SIMpirateship.tla
@@ -1,5 +1,5 @@
 ----- MODULE SIMpirateship -----
-EXTENDS TLCpirateship, TLC, TLCExt, CSV, IOUtils
+EXTENDS TLCpirateship, TLC, TLCExt, IOUtils
 
 SIMTimeout(r) ==
     /\ \/ 1 = RandomElement(1..((TLCGet("duration") % 300)+1)) \* Adjust probability of timeouts as a function of the duration of the simulation.
@@ -36,28 +36,23 @@ StatsHighestUnanimity(l, i, r) ==
     \* Transitive fast path, i.e., combined votes from all applicable QCs.
     ELSE HighestUnanimity(l, i, r)
 
-StatsConstraint ==
-    \* Average the number of uncommitted (byzantine) transactions accross all replicas. 
-    LET Sum == FoldFunction(+, 0, [ r \in R |-> Len(log[r]) - byzCommitIndex[r] ])
-    \* When done with the current behavior...
-    IN (TLCGet("level") = TLCGet("config").depth) => 
-            TLCGetAndSet(StatsFastPath, 
-                        LAMBDA old, val:
-                            \* Update the average (sum/observations) of uncommitted transactions.
-                            [ sum |-> old.sum + val, obs |-> old.obs + 1 ], 
-                        Sum, [sum |-> 0, obs |-> 0])
-                            \in [sum : Nat, obs : Nat] \* Always evaluate/equal to TRUE.
+StatsCollect(r, bci) ==
+    TLCGetAndSet(StatsFastPath, 
+            LAMBDA old, val: [ sum |-> old.sum + val, obs |-> old.obs + 1 ], 
+            byzCommitIndex'[r] - Max2(byzCommitIndex[r], bci), 
+            [sum |-> 0, obs |-> 0]
+    ) \in [sum : Nat, obs : Nat] \* Always evaluate/equal to TRUE.
+
+StatsReceiveVote(p, r) ==
+    /\ ReceiveVote(p, r)
+    /\ StatsCollect(p, HighestByzQC(SubSeq(log[p], 1, MaxQuorum(BQ, log[p], prepareQC'[p], 0))))
+
+StatsReceiveEntries(r, p) ==
+    /\ ReceiveEntries(r, p)
+    /\ StatsCollect(r, HighestQCOverQC(log'[r]))
 
 StatsPostcondition ==
-    \* Merge the average of each fastPath value accross all TLC workers.
-    /\ LET CSVFile == "StatsSIMpirateship.csv"
-           v ==[ key \in DOMAIN TLCGet("all") |-> 
-            FoldFunction(
-                    LAMBDA val, acc: [sum|->acc.sum+val.sum, obs|->acc.obs+val.obs], 
-                    [sum |-> 0, obs |-> 0], TLCGet("all")[key]) ] IN
-        /\ PrintT([ key \in DOMAIN v |-> <<key, v[key].sum \div v[key].obs>>])
-        /\ CSVRecords(CSVFile) = 0 => CSVWrite("fastPath#sum#observations", <<>>, CSVFile)
-        /\ \A key \in DOMAIN v:
-                CSVWrite("%1$s#%2$s#%3$s", <<key, v[key].sum, v[key].obs>>, CSVFile)
+    /\ PrintT(<<"FastPath", TLCGet(2)>>)
+    /\ PrintT(<<"FastPath (transitive)", TLCGet(3)>>)
 
 ====
\ No newline at end of file