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) ============================================================================