diff --git a/.gitignore b/.gitignore
index 3fc9e3a..6c3cb85 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,5 +1,5 @@
 states/
-
+*.out
 **/*.toolbox/*/
 **/*.toolbox/*___*_SnapShot_*.launch
 **/*.toolbox/.project
diff --git a/PessimisticTransaction/PessimisticTransaction.tla b/PessimisticTransaction/PessimisticTransaction.tla
index 282d6ef..d98af48 100644
--- a/PessimisticTransaction/PessimisticTransaction.tla
+++ b/PessimisticTransaction/PessimisticTransaction.tla
@@ -4,7 +4,7 @@ EXTENDS Integers, FiniteSets, TLC
 
 \* The set of transaction keys.
 CONSTANTS KEY
-ASSUME KEY # {} \* Keys cannot be empty.
+ASSUME KEY /= {} \* Keys cannot be empty.
 
 \* The set of pessimistic clients
 CONSTANTS PESSIMISTIC_CLIENT
@@ -77,7 +77,7 @@ vars == <<next_ts, client_vars, key_vars, msg>>
 
 -----------------------------------------------------------------------------
 
-Pos == {x \in Nat : x > 0}
+Pos == Nat \ {0}
 
 -----------------------------------------------------------------------------
 
@@ -99,6 +99,7 @@ rollback(k, ts) ==
   LET
     \* rollback the primary key of a pessimistic transaction needs be protected from being collapsed
     protected == \E l \in key_lock[k] : l.for_update_ts > 0 /\ k = l.primary
+    latest_write == latestHistoryWrite(k, ts)
   IN
     \* If the existing lock has the same ts, unlock it.
     /\ IF \E l \in key_lock[k] : l.ts = ts
@@ -107,8 +108,11 @@ rollback(k, ts) ==
     /\ key_data' = [key_data EXCEPT ![k] = @ \ {[ts |-> ts]}]
     \* Write a rollback in the write column.
     /\ key_write' = [key_write EXCEPT
-         ![k] = (@ \ {w \in latestHistoryWrite(k, ts) : w.type = "rollback" /\ ~w.protected }) \* collapse rollback
-                   \union {[ts |-> ts, type |-> "rollback", start_ts |-> ts, protected |-> protected]}]
+          ![k] = IF ~ \E w \in latest_write: w.ts = ts
+                 THEN (@ \ {w \in latest_write: w.type = "rollback" /\ ~w.protected }) \* collapse rollback
+                         \union {[ts |-> ts, type |-> "rollback", start_ts |-> ts, protected |-> protected]}
+                 ELSE @
+       ]
 
 \* Commit key k       
 commit(k, start_ts, commit_ts) ==
@@ -118,6 +122,7 @@ commit(k, start_ts, commit_ts) ==
        /\ key_lock' = [key_lock EXCEPT ![k] = {}]
        /\ key_write' = [key_write EXCEPT ![k] = @ \union {[ts |-> commit_ts, type |-> "write", start_ts |-> start_ts]}]
        \* Assert we don't violate snapshot isolation
+       \* TODO
        /\ Assert(key_last_read_ts[k] < commit_ts, <<key_last_read_ts[k], commit_ts>>)
      ELSE
        UNCHANGED <<key_lock, key_write>>
@@ -125,14 +130,9 @@ commit(k, start_ts, commit_ts) ==
 
 \* Change the state of client c to aborted
 abortTxn(c) ==
-  /\ ~ client_state[c] \in {"committed", "undetermined"}
+  /\ client_state[c] /= "committed"
   /\ client_state' = [client_state EXCEPT ![c] = "aborted"]
 
-\* Change the state of client c to undetermined due to lost commit RPC.
-undetermine(c) ==
-  /\ client_state[c] = "committing"
-  /\ client_state' = [client_state EXCEPT ![c] = "undetermined"]
-  
 -----------------------------------------------------------------------------
 
 StartOptimistic(c) ==
@@ -258,7 +258,7 @@ DoCleanup ==
           lock == {l \in key_lock[k] : l.ts = ts}
           committed == {w \in key_write[k] : w.start_ts = ts /\ w.type = "write"}
         IN
-          IF committed # {}
+          IF committed /= {}
           \* The transaction is already committed, so resolve locks using its commit_ts
           THEN
             /\ msg' = msg \union
@@ -345,7 +345,7 @@ DoLockKey ==
           LET
             l == CHOOSE l \in key_lock[k] : TRUE
           IN
-            IF l.ts # ts
+            IF l.ts /= ts
             \* If there is a lock from another transaction, the client may cleanup the lock.
             \* Response loss causes no state change.
             THEN                        
@@ -367,13 +367,13 @@ DoOptimisticPrewrite ==
         k == cmd.key
         primary == cmd.primary
         ts == cmd.start_ts
-        lock == { l \in key_lock[k] : l.ts # ts }
+        lock == { l \in key_lock[k] : l.ts /= ts }
       IN
         IF \E w \in key_write[k] : w.ts >= ts
         THEN
           /\ abortTxn(c)
           /\ UNCHANGED <<client_ts, client_key, next_ts, key_vars, msg>>
-        ELSE IF lock # {}
+        ELSE IF lock /= {}
         THEN
           \* When there is another transaction's lock, the client may resolve the lock by cleanup.
           /\ msg' = msg \union
@@ -403,7 +403,7 @@ DoPessimisticPrewrite ==
       IN
         IF
           \/ key_lock[k] = {}
-          \/ \E l \in key_lock[k] : l.ts # ts
+          \/ \E l \in key_lock[k] : l.ts /= ts
         THEN
           \* Abort the transaction when its lock doesn't exist
           /\ abortTxn(c)
@@ -433,16 +433,12 @@ DoCommit ==
         THEN
           /\ commit(k, start_ts, commit_ts)
           \* Change client state to committed.
-          /\ \/ client_state' = [client_state EXCEPT ![c] = "committed"]
-             \* Commit response is lost
-             \/ undetermine(c)
+          /\ client_state' = [client_state EXCEPT ![c] = "committed"]
           /\ UNCHANGED <<client_ts, client_key, next_ts, key_last_read_ts, msg>>
         ELSE
           \* The lock doesn't exist and the key is not committed, so commit fails.
-          /\ \/ /\ Assert(client_state[c] # "committed", client_state[c])
-                /\ abortTxn(c)
-             \* Commit response is lost
-             \/ undetermine(c)
+          /\ Assert(client_state[c] /= "committed", client_state[c])
+          /\ abortTxn(c)
           /\ UNCHANGED <<client_ts, client_key, next_ts, key_vars, msg>>
 
 ServerOp ==
@@ -483,19 +479,19 @@ PessimisticSpec == Init /\ [][Next]_vars
 
 -----------------------------------------------------------------------------
 
-NextTsTypeInv == next_ts \in Pos
+NextTsTypeOK == next_ts \in Pos
 
-ClientStateTypeInv ==
+ClientStateTypeOK ==
   client_state \in [
     CLIENT -> {"init", "working", "prewriting",
-               "committing", "committed", "aborted", "undetermined"}
+               "committing", "committed", "aborted"}
   ]
 
-ClientTsTypeInv ==
+ClientTsTypeOK ==
   client_ts \in
   [CLIENT -> [start_ts : Nat, for_update_ts : Nat, commit_ts : Nat]]
 
-ClientKeyTypeInv ==
+ClientKeyTypeOK ==
   \A c \in CLIENT :
     \/ client_state[c] = "init"
     \/ client_key[c] \in [primary : KEY,
@@ -503,20 +499,20 @@ ClientKeyTypeInv ==
                           pessimistic : SUBSET KEY,
                           pending : SUBSET KEY]
 
-KeyDataTypeInv ==
+KeyDataTypeOK ==
   key_data \in [KEY -> SUBSET [ts : Pos]]
 
-KeyLockTypeInv ==
+KeyLockTypeOK ==
   key_lock \in [KEY -> SUBSET [ts : Pos, for_update_ts : Nat, primary : KEY, pessimistic : BOOLEAN]]
 
-KeyWriteTypeInv ==
-  key_write \in [KEY -> SUBSET [ts : Pos, type : {"write"}, start_ts : Pos]] \union
-      [KEY -> SUBSET [ts : Pos, type : {"rollback"}, start_ts : Pos, protected : BOOLEAN]]
+KeyWriteTypeOK ==
+  key_write \in [KEY -> SUBSET ([ts : Pos, type : {"write"}, start_ts : Pos] \union 
+                                [ts : Pos, type : {"rollback"}, start_ts : Pos, protected : BOOLEAN])] 
 
-KeyLastReadTsTypeInv ==
+KeyLastReadTsTypeOK ==
   key_last_read_ts \in [KEY -> Nat]
 
-MsgTypeInv ==
+MsgTypeOK ==
   msg \subseteq (
     [c : CLIENT, type : {"lock", "prewrite"}, key : KEY, primary: KEY,
      start_ts : Pos, for_update_ts : Nat] \union
@@ -526,16 +522,16 @@ MsgTypeInv ==
     [type : {"resolve"}, primary : KEY, start_ts : Pos, commit_ts : Nat]
   )
 
-TypeInvariant ==
-  /\ NextTsTypeInv
-  /\ ClientStateTypeInv
-  /\ ClientTsTypeInv
-  /\ ClientKeyTypeInv
-  /\ KeyDataTypeInv
-  /\ KeyLockTypeInv
-  /\ KeyWriteTypeInv
-  /\ KeyLastReadTsTypeInv
-  /\ MsgTypeInv
+TypeOK ==
+  /\ NextTsTypeOK
+  /\ ClientStateTypeOK
+  /\ ClientTsTypeOK
+  /\ ClientKeyTypeOK
+  /\ KeyDataTypeOK
+  /\ KeyLockTypeOK
+  /\ KeyWriteTypeOK
+  /\ KeyLastReadTsTypeOK
+  /\ MsgTypeOK
   
 -----------------------------------------------------------------------------
 
@@ -583,7 +579,7 @@ AbortedClientConsistency ==
 
 CommittedTxnConsistency ==
   \A c \in CLIENT :
-    client_state[c] # "init" =>
+    client_state[c] /= "init" =>
       LET
         primary == client_key[c].primary
         secondary == client_key[c].secondary
@@ -614,7 +610,7 @@ UniqueWrite ==
 -----------------------------------------------------------------------------
 
 THEOREM Safety ==
-  PessimisticSpec => [](/\ TypeInvariant
+  PessimisticSpec => [](/\ TypeOK
                         /\ WriteConsistency
                         /\ LockConsistency
                         /\ CommittedTxnConsistency
diff --git a/PessimisticTransaction/PessimisticTransaction.toolbox/PessimisticTransaction___Test1.launch b/PessimisticTransaction/PessimisticTransaction.toolbox/PessimisticTransaction___Test1.launch
index 2348680..8a37459 100644
--- a/PessimisticTransaction/PessimisticTransaction.toolbox/PessimisticTransaction___Test1.launch
+++ b/PessimisticTransaction/PessimisticTransaction.toolbox/PessimisticTransaction___Test1.launch
@@ -1,31 +1,69 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
 <launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
+    <stringAttribute key="TLCCmdLineParameters" value=""/>
+    <intAttribute key="collectCoverage" value="1"/>
     <stringAttribute key="configurationName" value="Test1"/>
+    <booleanAttribute key="deferLiveness" value="false"/>
+    <intAttribute key="dfidDepth" value="100"/>
+    <booleanAttribute key="dfidMode" value="false"/>
     <intAttribute key="distributedFPSetCount" value="0"/>
-    <stringAttribute key="distributedNetworkInterface" value="192.168.220.40"/>
+    <stringAttribute key="distributedNetworkInterface" value="10.0.75.1"/>
     <intAttribute key="distributedNodesCount" value="1"/>
     <stringAttribute key="distributedTLC" value="off"/>
-    <intAttribute key="fpIndex" value="68"/>
-    <intAttribute key="maxHeapSize" value="25"/>
+    <stringAttribute key="distributedTLCVMArgs" value=""/>
+    <intAttribute key="fpBits" value="1"/>
+    <intAttribute key="fpIndex" value="3"/>
+    <booleanAttribute key="fpIndexRandom" value="true"/>
+    <intAttribute key="maxHeapSize" value="63"/>
+    <intAttribute key="maxSetSize" value="1000000"/>
+    <booleanAttribute key="mcMode" value="true"/>
     <stringAttribute key="modelBehaviorInit" value="Init"/>
     <stringAttribute key="modelBehaviorNext" value="Next"/>
     <stringAttribute key="modelBehaviorSpec" value=""/>
     <intAttribute key="modelBehaviorSpecType" value="2"/>
     <stringAttribute key="modelBehaviorVars" value="msg, key_data, key_lock, next_ts, client_state, key_last_read_ts, client_key, client_ts, key_write"/>
     <stringAttribute key="modelComments" value=""/>
-    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
-    <listAttribute key="modelCorrectnessInvariants"/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="false"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="0TypeOK"/>
+        <listEntry value="1WriteConsistency"/>
+        <listEntry value="1LockConsistency"/>
+        <listEntry value="1CommittedTxnConsistency"/>
+        <listEntry value="1AbortedClientConsistency"/>
+        <listEntry value="1RollbackConsistency"/>
+        <listEntry value="1NextTsTypeOK"/>
+        <listEntry value="1&#13;&#10;ClientStateTypeOK"/>
+        <listEntry value="1&#13;&#10;ClientTsTypeOK"/>
+        <listEntry value="1&#13;&#10;ClientKeyTypeOK"/>
+        <listEntry value="1&#13;&#10;KeyDataTypeOK"/>
+        <listEntry value="1&#13;&#10;KeyLockTypeOK"/>
+        <listEntry value="1&#13;&#10;KeyWriteTypeOK"/>
+        <listEntry value="1UniqueWrite"/>
+    </listAttribute>
     <listAttribute key="modelCorrectnessProperties"/>
+    <intAttribute key="modelEditorOpenTabs" value="14"/>
     <stringAttribute key="modelExpressionEval" value=""/>
+    <stringAttribute key="modelParameterActionConstraint" value=""/>
     <listAttribute key="modelParameterConstants">
         <listEntry value="KEY;;{k1, k2};1;1"/>
         <listEntry value="CLIENT_KEY;;c1 :&gt; {k1, k2} @@ c2 :&gt; {k2};0;0"/>
-        <listEntry value="PESSIMISTIC_CLIENT;;{c1, c2};1;0"/>
+        <listEntry value="PESSIMISTIC_CLIENT;;{c1, c2};1;1"/>
         <listEntry value="OPTIMISTIC_CLIENT;;{};0;0"/>
         <listEntry value="CLIENT_PRIMARY;;c1 :&gt; k1 @@ c2 :&gt; k2;0;0"/>
     </listAttribute>
-    <intAttribute key="numberOfWorkers" value="6"/>
+    <stringAttribute key="modelParameterContraint" value=""/>
+    <listAttribute key="modelParameterDefinitions"/>
+    <stringAttribute key="modelParameterModelValues" value="{}"/>
+    <stringAttribute key="modelParameterNewDefinitions" value=""/>
+    <intAttribute key="modelVersion" value="20191005"/>
+    <intAttribute key="numberOfWorkers" value="10"/>
+    <booleanAttribute key="recover" value="false"/>
     <stringAttribute key="result.mail.address" value=""/>
+    <intAttribute key="simuAril" value="-1"/>
+    <intAttribute key="simuDepth" value="100"/>
+    <intAttribute key="simuSeed" value="-1"/>
     <stringAttribute key="specName" value="PessimisticTransaction"/>
     <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <stringAttribute key="view" value=""/>
+    <booleanAttribute key="visualizeStateGraph" value="false"/>
 </launchConfiguration>
diff --git a/PessimisticTransaction/Test1.cfg b/PessimisticTransaction/Test1.cfg
new file mode 100644
index 0000000..1f1ac6f
--- /dev/null
+++ b/PessimisticTransaction/Test1.cfg
@@ -0,0 +1,33 @@
+\* See Test1.tla.
+
+CONSTANT
+  KEY <- Key
+  OPTIMISTIC_CLIENT <- OptimistiicClient
+  PESSIMISTIC_CLIENT <- PessimisticClient
+  CLIENT_KEY <- ClientKey
+  CLIENT_PRIMARY <- ClientPrimary
+
+INIT
+  Init
+
+NEXT
+  Next
+
+INVARIANT
+  NextTsTypeOK
+  ClientStateTypeOK
+  ClientTsTypeOK
+  ClientKeyTypeOK
+  KeyDataTypeOK
+  KeyLockTypeOK
+  KeyWriteTypeOK
+  KeyLastReadTsTypeOK
+  MsgTypeOK
+
+INVARIANT
+  WriteConsistency
+  LockConsistency
+  CommittedTxnConsistency
+  AbortedClientConsistency
+  RollbackConsistency
+  UniqueWrite
diff --git a/PessimisticTransaction/Test1.tla b/PessimisticTransaction/Test1.tla
new file mode 100644
index 0000000..01e79f1
--- /dev/null
+++ b/PessimisticTransaction/Test1.tla
@@ -0,0 +1,19 @@
+--------------------------------- MODULE Test1 ---------------------------------
+
+EXTENDS PessimisticTransaction, TLC
+
+\* Model value is not used to avoid unnecessary state space 
+\* checked by TLC. Symmetry should not be used if we are supposed
+\* to check liveness.
+k1 == 1
+k2 == 2
+c1 == 1
+c2 == 2
+
+Key == {k1, k2}
+OptimistiicClient == {}
+PessimisticClient == {c1, c2}
+ClientKey == c1 :> {k1, k2} @@ c2 :> {k2}
+ClientPrimary == c1 :> k1 @@ c2 :> k2
+
+================================================================================