From 79137382e751c4d907aeb65be8ecda83b0896f40 Mon Sep 17 00:00:00 2001 From: Arseny Sher Date: Thu, 7 Nov 2024 13:04:47 +0300 Subject: [PATCH] note on fig8 --- safekeeper/spec/ProposerAcceptorStatic.tla | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/safekeeper/spec/ProposerAcceptorStatic.tla b/safekeeper/spec/ProposerAcceptorStatic.tla index 7de8a0cbd3..6a6f16fd5d 100644 --- a/safekeeper/spec/ProposerAcceptorStatic.tla +++ b/safekeeper/spec/ProposerAcceptorStatic.tla @@ -20,7 +20,8 @@ \* Some ideas how to break it to play around to get a feeling: \* - replace Quorums with BadQuorums. \* - remove 'don't commit entries from previous terms separately' rule in -\* CommitEntries and observe figure 8 from the raft paper. +\* CommitEntries and observe figure 8 from the raft paper. +\* With p2a3t4l4 32 steps error was found in 1h on 80 cores. EXTENDS Integers, Sequences, FiniteSets, TLC