fix MC_SIB_SNAPSHOT comments

s12f · Dec 8, 2024 · c501ff8 · c501ff8
1 parent 4b05e53
commit c501ff8
Showing 1 changed file with 1 addition and 2 deletions.
diff --git 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)
 
 ============================================================================