diff --git a/isolation-models/ALL_TESTS.tla b/isolation-models/ALL_TESTS.tla
index 4827b37..ac4ad71 100644
--- a/isolation-models/ALL_TESTS.tla
+++ b/isolation-models/ALL_TESTS.tla
@@ -2,4 +2,4 @@
 
 EXTENDS SIB_TESTS
 
-======================================================
\ No newline at end of file
+======================================================
diff --git a/isolation-models/SIB_ISOLATION.tla b/isolation-models/SIB_ISOLATION.tla
index 6c6f205..183b2ab 100644
--- a/isolation-models/SIB_ISOLATION.tla
+++ b/isolation-models/SIB_ISOLATION.tla
@@ -19,6 +19,7 @@ SetToSeqs(S) ≜
 SeqToSet(S) ≜ { S[x] : x ∈ S}
 
 Max(S) ≜ CHOOSE x ∈ S: ∀ y ∈ S: x ≥ y
+Min(S) ≜ CHOOSE x ∈ S: ∀ y ∈ S: x ≤ y
 
 ----------------------------------------------------
 \* States
@@ -132,6 +133,22 @@ PSI_CT(t, txs, states) ≜
        IN ∧ ∀ t1 ∈ ps, ok ∈ ops:
             ok ∈ DOMAIN txs[t1].write ⇒ t1 + 1 ≤ slo(ok)
 
+(* Read Atomic Isolation Commit Test:
+ Intuitively, if an operation o1 observes the writes of a transaction Ti ’s,
+ all subsequent operations that read a key included in Ti ’s write set must
+ read from a state that includes Ti ’s effects.
+*)
+RA_CT(t, txs, states) ≜
+    ∧ RC_CT(t, txs, states)
+    ∧ LET read ≜ txs[t].read
+          sf(k) ≜ Min({ x ∈ 1 ‥ t : read[k] = states[x][k] })
+      IN ∀k1, k2 ∈ DOMAIN read:
+            LET sfr1 ≜ sf(k1)
+                sfr2 ≜ sf(k2)
+                tw_sfr1 ≜ IF sfr1 = 1 THEN {} ELSE DOMAIN txs[sfr1 - 1].write
+            IN k2 ∈ tw_sfr1 ⇒ sfr1 ≤ sfr2
+
+
 ----------------------------------------------------
 \* Isolation Executions
 
@@ -146,6 +163,7 @@ ReadCommittedExecution(e) ≜ IsolationExecution(e, RC_CT)
 ReadUncommittedExecution(e) ≜ IsolationExecution(e, RU_CT)
 ParallelSnapshotExecution(e) ≜ IsolationExecution(e, PSI_CT)
 StrictSerializableExecution(e) ≜ IsolationExecution(e, SSER_CT)
+ReadAtomicExecution(e) ≜ IsolationExecution(e, RA_CT)
 
 ----------------------------------------------------
 \* Isolation Levels
@@ -160,5 +178,6 @@ ReadCommittedIsolation(init, transactions) ≜ Isolation(init, transactions, Rea
 ReadUncommittedIsolation(init, transactions) ≜ Isolation(init, transactions, ReadUncommittedExecution)
 ParallelSnapshotIsolation(init, transactions) ≜ Isolation(init, transactions, ParallelSnapshotExecution)
 StrictSerializableIsolation(init, transactions) ≜ Isolation(init, transactions, StrictSerializableExecution)
+ReadAtomicIsolation(init, transactions) ≜ Isolation(init, transactions, ReadAtomicExecution)
 
-================================================
\ No newline at end of file
+================================================
diff --git a/isolation-models/SIB_TESTS.tla b/isolation-models/SIB_TESTS.tla
index 4a732bf..cf0cb4a 100644
--- a/isolation-models/SIB_TESTS.tla
+++ b/isolation-models/SIB_TESTS.tla
@@ -25,4 +25,13 @@ failed_sser_txs ≜
 ASSUME SI!SerializableIsolation(init, failed_sser_txs)
 ASSUME ¬ SI!StrictSerializableIsolation(init, failed_sser_txs)
 
-======================================================
\ No newline at end of file
+\* Partial Read
+pr_txs ≜
+    { [ tid ↦ "t1", read ↦ ⟨⟩, write ↦ [k1 ↦ 1, k2 ↦ 1]]
+    , [ tid ↦ "t2", read ↦ [k1 ↦ 1, k2 ↦ 0], write ↦ ⟨⟩]
+    }
+
+ASSUME SI!ReadCommittedIsolation(init, pr_txs)
+ASSUME ¬ SI!ReadAtomicIsolation(init, pr_txs)
+
+======================================================
diff --git a/multi-paxos-eb0/MultiPaxos.tla b/multi-paxos-eb0/MultiPaxos.tla
index 30186ec..2e3078d 100644
--- a/multi-paxos-eb0/MultiPaxos.tla
+++ b/multi-paxos-eb0/MultiPaxos.tla
@@ -188,4 +188,4 @@ Spec ≜ Init ∧ □[Next]_vars
 Inv ≜ ∧ TypeOK
       ∧ ∀c1, c2 ∈ committed:
             c1.seq = c2.seq ⇒ c1.val = c2.val
-============================================================================
\ No newline at end of file
+============================================================================
diff --git a/paxos-eb0/PaxosEb0.tla b/paxos-eb0/PaxosEb0.tla
index fa7fae9..7ccd100 100644
--- a/paxos-eb0/PaxosEb0.tla
+++ b/paxos-eb0/PaxosEb0.tla
@@ -108,4 +108,4 @@ Spec ≜ Init ∧ □[Next]_vars
 
 Inv ≜ ∧ TypeOK
       ∧ ∀ v1 ∈ committed, v2 ∈ committed: v1 = v2
-============================================================================
\ No newline at end of file
+============================================================================
diff --git a/percolator/MC_SIB_SNAPSHOT.tla b/percolator/MC_SIB_SNAPSHOT.tla
index f0a49c0..5671d37 100644
--- a/percolator/MC_SIB_SNAPSHOT.tla
+++ b/percolator/MC_SIB_SNAPSHOT.tla
@@ -43,4 +43,4 @@ SnapshotInv ≜ AllTxsDone ⇒
     \* SerializableIsolation will fail, Because exists write skew executions
     \* ∧ SI!SerializableIsolation(InitState, MappedTxs)
 
-============================================================================
\ No newline at end of file
+============================================================================
diff --git a/percolator/Percolator.tla b/percolator/Percolator.tla
index a3a7e4d..a3fc251 100644
--- a/percolator/Percolator.tla
+++ b/percolator/Percolator.tla
@@ -215,4 +215,4 @@ TypeOK ≜
 
 Inv ≜ TypeOK
 
-============================================================================
\ No newline at end of file
+============================================================================
diff --git a/percolator/SnapshotRead.tla b/percolator/SnapshotRead.tla
index d9c11ab..67c27eb 100644
--- a/percolator/SnapshotRead.tla
+++ b/percolator/SnapshotRead.tla
@@ -40,4 +40,4 @@ SnapshotReadInv ≜
     ∨ LET r ≜ txs["t2"].read
       IN 20 = r["k1"] + r["k2"]
 
-============================================================================
\ No newline at end of file
+============================================================================
diff --git a/percolator/Transfer.tla b/percolator/Transfer.tla
index 88c4243..ee2102d 100644
--- a/percolator/Transfer.tla
+++ b/percolator/Transfer.tla
@@ -37,4 +37,4 @@ AtomicRead ≜
 
 TransferInv ≜ Inv ∧ AtomicRead
 
-============================================================================
\ No newline at end of file
+============================================================================
diff --git a/sequencer/MCSequencer.tla b/sequencer/MCSequencer.tla
index f642615..784d9bf 100644
--- a/sequencer/MCSequencer.tla
+++ b/sequencer/MCSequencer.tla
@@ -15,4 +15,4 @@ Constraint ≜
     ∧ nextRid < 7
     ∧ storage < 7
 
-====
\ No newline at end of file
+====
diff --git a/sequencer/Sequencer.tla b/sequencer/Sequencer.tla
index 41e7b7c..13cd415 100644
--- a/sequencer/Sequencer.tla
+++ b/sequencer/Sequencer.tla
@@ -128,4 +128,4 @@ LinearizableHistory ≜
 
 Inv ≜ LinearizableHistory
 
-============================================================================
\ No newline at end of file
+============================================================================
diff --git a/simplified-fast-paxos/SimplifiedFastPaxos.tla b/simplified-fast-paxos/SimplifiedFastPaxos.tla
index 0ca00ec..8d687e2 100644
--- a/simplified-fast-paxos/SimplifiedFastPaxos.tla
+++ b/simplified-fast-paxos/SimplifiedFastPaxos.tla
@@ -123,4 +123,4 @@ Spec ≜ Init ∧ □[Next]_vars
 
 Inv ≜ ∧ TypeOK
       ∧ ∀ v1 ∈ committed, v2 ∈ committed: v1 = v2
-============================================================================
\ No newline at end of file
+============================================================================