demo how TLA+ model checking helps to find raft issue

joshuazh-x · Mar 26, 2024 · 6aefcc8 · serathius · Mar 26, 2024 · joshuazh-x
1 parent 7f35117
commit 6aefcc8
Show file tree

Hide file tree

Showing 3 changed files with 206 additions and 114 deletions.
diff --git a/tla/etcdraft.cfg b/tla/etcdraft.cfg
@@ -20,8 +20,11 @@ CONSTANTS
     s4 = 4
     s5 = 5
 
-    InitServer  = {s1, s2, s3}
-    Server      = {s1, s2, s3}
+    \* InitServer  = {s1, s2, s3}
+    \* Server      = {s1, s2, s3}
+
+    InitServer  = {s1}
+    Server      = {s1}
 
     Nil         = 0
 
@@ -52,3 +55,4 @@ INVARIANTS
     QuorumLogInv
     MoreUpToDateCorrectInv
     LeaderCompletenessInv
+    CommittedIsDurableInv