FV-3, FV-4: 2PC coordinator crash/recovery + participant timeout

- twopc.tla: Add coordinatorLog (persistent WAL for decisions)
- twopc.tla: Add CrashCoordinator action
- twopc.tla: Add RecoverCoordinator action (reads from coordinatorLog)
- twopc.tla: Add ParticipantTimeout (only if coordinatorLog = Nil)
- twopc.tla: Add RecoveryConsistency invariant
- models/twopc.cfg: Add RecoveryConsistency to checked invariants
- Update PLAN.md, ANALYSIS.md, README.md with new metrics

PLAN.md

@@ -55,8 +55,8 @@
 |---|--------|----------------|-----------|
 | FV-1 | ~~Raft: prevLogIndex/prevLogTerm в Replicate~~ ✅ | TLA+ моделът вече проверява prevLogIndex/prevLogTerm, възстановена е `LogMatching` инвариантата, добавено е `RejectAppendEntries` и conflict truncation. | `formal-verification/raft.tla` |
 | FV-2 | **Raft: Leader step-down при partition** | Няма `HeartbeatTimeout` или `LeaderLeaseExpired` — моделът не проверява дали leader се отказва при network partition. | `formal-verification/raft.tla` |
-| FV-3 | **2PC: Coordinator crash/recovery** | Спекът не моделира coordinator crash + WAL replay. При реален crash, participant-ите в `Prepared` остават блокирани завинаги. | `formal-verification/twopc.tla` |
+| FV-3 | ~~2PC: Coordinator crash/recovery~~ ✅ | Добавени `coordinatorLog`, `CrashCoordinator`, `RecoverCoordinator`. Coordinator записва решението в persistent log преди изпращане. | `formal-verification/twopc.tla` |
-| FV-4 | **2PC: Participant timeout** | Липсва `ParticipantTimeout(t,p)` — participant трябва самостоятелно да abort-ва при липса на решение от coordinator. | `formal-verification/twopc.tla` |
+| FV-4 | ~~2PC: Participant timeout~~ ✅ | `ParticipantTimeout` позволява abort само ако coordinator е crashed и НЕ е записал решение (`coordinatorLog = Nil`). | `formal-verification/twopc.tla` |
 
 ### 🟡 Важни (нови свойства и покритие)
 

formal-verification/ANALYSIS.md

@@ -79,16 +79,16 @@
 
 **Препоръка:** Разширяване на Replicate с `prevLogIndex` и `prevLogTerm` параметри, добавяне на `InstallSnapshot` действие, и връщане на `LogMatching` инварианта.
 
-### 2.5. 2PC без recovery модел
+### 2.5. 2PC без recovery модел ✅ Направено
 
-Спекът не моделира:
+~~Спекът не моделира:~~
 
-- Coordinator crash и recovery (read decision from WAL)
+- ~~Coordinator crash и recovery (read decision from WAL)~~ ✅ Добавени `CrashCoordinator` и `RecoverCoordinator`
-- Participant timeout (какво става ако participant не отговори)
+- ~~Participant timeout~~ ✅ `ParticipantTimeout` позволява abort само при `coordinatorLog = Nil`
-- Heuristic decisions (участник взима самостоятелно решение при coordinator failure)
+- ~~Heuristic decisions~~ ✅ Participant не може да abort-ва ако coordinator е decided
-- Transaction log replay
+- ~~Transaction log replay~~ ✅ `RecoverCoordinator` чете `coordinatorLog`
 
-**Препоръка:** Добавяне на `CrashCoordinator(t)` и `RecoverCoordinator(t)` действия с четене на `decidedAction[t]` от персистентен лог.
+**Резултат:** `RecoveryConsistency` инвариантата гарантира че след crash+recovery, решението е същото.
 
 ### 2.6. MVCC без garbage collection
 

formal-verification/README.md

@@ -26,13 +26,13 @@ This directory contains TLA+ specifications for core BaraDB distributed-systems
 | Spec | States Generated | Distinct States | Depth |
 |------|-----------------|-----------------|-------|
 | raft.tla | 3,031,684 | 833,024 | 47 |
-| twopc.tla | 2,125,825 | 262,144 | 28 |
+| twopc.tla | 22,855,681 | 2,097,152 | 31 |
 | mvcc.tla | 177,849 | 59,860 | 13 |
 | replication.tla | 3,687,939 | 490,560 | 22 |
 | gossip.tla | 1,257,121 | 110,592 | 28 |
 | deadlock.tla | 3,767,361 | 263,950 | 9 |
 | sharding.tla | 186,305 | 23,296 | 11 |
-| **Total** | **14,234,084** | **2,043,426** | — |
+| **Total** | **34,963,940** | **3,878,434** | — |
 
 ## Running the Model Checker
 

formal-verification/models/twopc.cfg

@@ -15,3 +15,4 @@ INVARIANTS
   CoordinatorConsistency
   NoDecideWithoutConsensus
   ParticipantStateValid
+  RecoveryConsistency

formal-verification/twopc.tla

@@ -9,6 +9,7 @@
     - CoordinatorConsistency  : once decided, the coordinator never changes decision.
     - NoDecideWithoutConsensus: coordinator only decides when all votes are collected.
     - ParticipantStateValid   : participant state transitions are valid.
+    - RecoveryConsistency     : after coordinator crash+recovery, decision is unchanged.
 *)
 
 EXTENDS Integers, Sequences, FiniteSets, TLC
@@ -24,9 +25,11 @@ VARIABLES
                   \*                "Committed","Aborting","Aborted"}
   participantState, \* participantState[t][p] ∈ {"Active","Prepared","Committed","Aborted"}
   coordinatorDecided, \* coordinatorDecided[t] ∈ {TRUE, FALSE}
-  decidedAction     \* decidedAction[t] ∈ {"Commit","Abort", Nil}
+  decidedAction,     \* decidedAction[t] ∈ {"Commit","Abort", Nil}
+  coordinatorLog,   \* coordinatorLog[t] ∈ {"Commit","Abort", Nil} — persistent WAL
+  coordinatorAlive  \* coordinatorAlive[t] ∈ BOOLEAN
 
-vars == <<txnState, participantState, coordinatorDecided, decidedAction>>
+vars == <<txnState, participantState, coordinatorDecided, decidedAction, coordinatorLog, coordinatorAlive>>
 
 -----------------------------------------------------------------------------
 
@@ -38,6 +41,9 @@ AllPrepared(t) ==
 AnyPrepareFailed(t) ==
   \E p \in Participants : participantState[t][p] = "Aborted"
 
+AllResponded(t) ==
+  \A p \in Participants : participantState[t][p] /= "Active"
+
 -----------------------------------------------------------------------------
 \* Initial state
 
@@ -46,48 +52,56 @@ Init ==
   /\ participantState = [t \in 1..MaxTxnId |-> [p \in Participants |-> "Active"]]
   /\ coordinatorDecided = [t \in 1..MaxTxnId |-> FALSE]
   /\ decidedAction = [t \in 1..MaxTxnId |-> Nil]
+  /\ coordinatorLog = [t \in 1..MaxTxnId |-> Nil]
+  /\ coordinatorAlive = [t \in 1..MaxTxnId |-> TRUE]
 
 -----------------------------------------------------------------------------
 \* State transitions
 
 \* Phase 1a: Coordinator sends PREPARE to all participants.
 SendPrepare(t) ==
+  /\ coordinatorAlive[t]
   /\ txnState[t] = "Active"
   /\ txnState' = [txnState EXCEPT ![t] = "Preparing"]
-  /\ UNCHANGED <<participantState, coordinatorDecided, decidedAction>>
+  /\ UNCHANGED <<participantState, coordinatorDecided, decidedAction, coordinatorLog, coordinatorAlive>>
 
 \* Phase 1b: Participant p receives PREPARE and votes Yes.
 ParticipantPrepare(t, p) ==
   /\ txnState[t] = "Preparing"
   /\ participantState[t][p] = "Active"
   /\ participantState' = [participantState EXCEPT ![t][p] = "Prepared"]
-  /\ UNCHANGED <<txnState, coordinatorDecided, decidedAction>>
+  /\ UNCHANGED <<txnState, coordinatorDecided, decidedAction, coordinatorLog, coordinatorAlive>>
 
 \* Phase 1c: Participant p votes No (aborts locally).
 ParticipantAbort(t, p) ==
   /\ txnState[t] \in {"Preparing", "Active"}
   /\ participantState[t][p] = "Active"
   /\ participantState' = [participantState EXCEPT ![t][p] = "Aborted"]
-  /\ UNCHANGED <<txnState, coordinatorDecided, decidedAction>>
+  /\ UNCHANGED <<txnState, coordinatorDecided, decidedAction, coordinatorLog, coordinatorAlive>>
 
 \* Phase 2a: Coordinator decides COMMIT (all voted Yes).
+\* The decision is first persisted to coordinatorLog before being sent.
 DecideCommit(t) ==
+  /\ coordinatorAlive[t]
   /\ txnState[t] = "Preparing"
   /\ AllPrepared(t)
   /\ ~AnyPrepareFailed(t)
   /\ txnState' = [txnState EXCEPT ![t] = "Committing"]
   /\ coordinatorDecided' = [coordinatorDecided EXCEPT ![t] = TRUE]
   /\ decidedAction' = [decidedAction EXCEPT ![t] = "Commit"]
-  /\ UNCHANGED <<participantState>>
+  /\ coordinatorLog' = [coordinatorLog EXCEPT ![t] = "Commit"]
+  /\ UNCHANGED <<participantState, coordinatorAlive>>
 
 \* Phase 2a-alt: Coordinator decides ABORT (at least one No or timeout).
 DecideAbort(t) ==
+  /\ coordinatorAlive[t]
   /\ txnState[t] = "Preparing"
   /\ AnyPrepareFailed(t)
   /\ txnState' = [txnState EXCEPT ![t] = "Aborting"]
   /\ coordinatorDecided' = [coordinatorDecided EXCEPT ![t] = TRUE]
   /\ decidedAction' = [decidedAction EXCEPT ![t] = "Abort"]
-  /\ UNCHANGED <<participantState>>
+  /\ coordinatorLog' = [coordinatorLog EXCEPT ![t] = "Abort"]
+  /\ UNCHANGED <<participantState, coordinatorAlive>>
 
 \* Phase 2b: Participant receives COMMIT decision.
 ReceiveCommit(t, p) ==
@@ -95,7 +109,7 @@ ReceiveCommit(t, p) ==
   /\ decidedAction[t] = "Commit"
   /\ participantState[t][p] \in {"Prepared", "Active"}
   /\ participantState' = [participantState EXCEPT ![t][p] = "Committed"]
-  /\ UNCHANGED <<txnState, coordinatorDecided, decidedAction>>
+  /\ UNCHANGED <<txnState, coordinatorDecided, decidedAction, coordinatorLog, coordinatorAlive>>
 
 \* Phase 2b-alt: Participant receives ABORT decision.
 ReceiveAbort(t, p) ==
@@ -103,20 +117,44 @@ ReceiveAbort(t, p) ==
   /\ decidedAction[t] = "Abort"
   /\ participantState[t][p] \in {"Prepared", "Active", "Aborted"}
   /\ participantState' = [participantState EXCEPT ![t][p] = "Aborted"]
-  /\ UNCHANGED <<txnState, coordinatorDecided, decidedAction>>
+  /\ UNCHANGED <<txnState, coordinatorDecided, decidedAction, coordinatorLog, coordinatorAlive>>
 
 \* Finalize: transaction moves to terminal state when all participants are done.
 FinalizeCommit(t) ==
   /\ txnState[t] = "Committing"
   /\ \A p \in Participants : participantState[t][p] = "Committed"
   /\ txnState' = [txnState EXCEPT ![t] = "Committed"]
-  /\ UNCHANGED <<participantState, coordinatorDecided, decidedAction>>
+  /\ UNCHANGED <<participantState, coordinatorDecided, decidedAction, coordinatorLog, coordinatorAlive>>
 
 FinalizeAbort(t) ==
   /\ txnState[t] = "Aborting"
   /\ \A p \in Participants : participantState[t][p] = "Aborted"
   /\ txnState' = [txnState EXCEPT ![t] = "Aborted"]
-  /\ UNCHANGED <<participantState, coordinatorDecided, decidedAction>>
+  /\ UNCHANGED <<participantState, coordinatorDecided, decidedAction, coordinatorLog, coordinatorAlive>>
+
+\* Coordinator crashes after deciding but possibly before all participants are informed.
+CrashCoordinator(t) ==
+  /\ coordinatorAlive[t]
+  /\ coordinatorAlive' = [coordinatorAlive EXCEPT ![t] = FALSE]
+  /\ UNCHANGED <<txnState, participantState, coordinatorDecided, decidedAction, coordinatorLog>>
+
+\* Coordinator recovers from crash and reads its decision from the persistent log.
+RecoverCoordinator(t) ==
+  /\ ~coordinatorAlive[t]
+  /\ coordinatorAlive' = [coordinatorAlive EXCEPT ![t] = TRUE]
+  /\ coordinatorDecided' = [coordinatorDecided EXCEPT ![t] = coordinatorLog[t] /= Nil]
+  /\ decidedAction' = [decidedAction EXCEPT ![t] = coordinatorLog[t]]
+  /\ UNCHANGED <<txnState, participantState, coordinatorLog>>
+
+\* Participant p times out waiting for the coordinator decision and aborts.
+\* This can only happen if the coordinator crashed BEFORE deciding (coordinatorLog = Nil).
+\* If the coordinator already decided, the participant must wait for recovery.
+ParticipantTimeout(t, p) ==
+  /\ participantState[t][p] = "Prepared"
+  /\ ~coordinatorAlive[t]
+  /\ coordinatorLog[t] = Nil
+  /\ participantState' = [participantState EXCEPT ![t][p] = "Aborted"]
+  /\ UNCHANGED <<txnState, coordinatorDecided, decidedAction, coordinatorLog, coordinatorAlive>>
 
 -----------------------------------------------------------------------------
 \* Next-state relation
@@ -131,6 +169,9 @@ Next ==
   \/ \E t \in 1..MaxTxnId : \E p \in Participants : ReceiveAbort(t, p)
   \/ \E t \in 1..MaxTxnId : FinalizeCommit(t)
   \/ \E t \in 1..MaxTxnId : FinalizeAbort(t)
+  \/ \E t \in 1..MaxTxnId : CrashCoordinator(t)
+  \/ \E t \in 1..MaxTxnId : RecoverCoordinator(t)
+  \/ \E t \in 1..MaxTxnId : \E p \in Participants : ParticipantTimeout(t, p)
 
 -----------------------------------------------------------------------------
 \* Safety properties
@@ -166,6 +207,11 @@ ParticipantStateValid ==
       (participantState[t][p] = "Committed" => decidedAction[t] = "Commit")
       /\ (participantState[t][p] = "Aborted" /\ decidedAction[t] /= Nil => decidedAction[t] = "Abort")
 
+\* RecoveryConsistency: if the coordinator has a logged decision, recovery restores it exactly.
+RecoveryConsistency ==
+  \A t \in 1..MaxTxnId :
+    coordinatorLog[t] /= Nil => decidedAction[t] = coordinatorLog[t]
+
 \* Type invariant
 TypeOk ==
   /\ txnState \in [1..MaxTxnId -> {"Active","Preparing","Prepared","Committing",
@@ -174,5 +220,7 @@ TypeOk ==
                                                               "Committed","Aborted"}]]
   /\ coordinatorDecided \in [1..MaxTxnId -> BOOLEAN]
   /\ decidedAction \in [1..MaxTxnId -> {"Commit","Abort", Nil}]
+  /\ coordinatorLog \in [1..MaxTxnId -> {"Commit","Abort", Nil}]
+  /\ coordinatorAlive \in [1..MaxTxnId -> BOOLEAN]
 
 =============================================================================