From c501ff8514f3e5de1fe86bc4ef0d1a65f6bdf6a0 Mon Sep 17 00:00:00 2001
From: s12f <s12f.hs@gmail.com>
Date: Sun, 8 Dec 2024 17:16:32 +0800
Subject: [PATCH] fix MC_SIB_SNAPSHOT comments

---
 percolator/MC_SIB_SNAPSHOT.tla | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/percolator/MC_SIB_SNAPSHOT.tla b/percolator/MC_SIB_SNAPSHOT.tla
index f92032a..5671d37 100644
--- a/percolator/MC_SIB_SNAPSHOT.tla
+++ b/percolator/MC_SIB_SNAPSHOT.tla
@@ -40,8 +40,7 @@ AllTxsDone ≜ ∀tx ∈ Tx: txs[tx].status ∈ { "committed", "aborted" }
 SnapshotInv ≜ AllTxsDone ⇒
     ∧ SI!SnapshotIsolation(InitState, MappedTxs)
     ∧ SI!ReadCommittedIsolation(InitState, MappedTxs)
-    \* SerializableIsolation Will failed,
-    \* Because exists write skew executions
+    \* SerializableIsolation will fail, Because exists write skew executions
     \* ∧ SI!SerializableIsolation(InitState, MappedTxs)
 
 ============================================================================