diff --git a/PessimisticTransaction/Test2.cfg b/PessimisticTransaction/Test2.cfg
new file mode 100644
index 0000000..780fc44
--- /dev/null
+++ b/PessimisticTransaction/Test2.cfg
@@ -0,0 +1,33 @@
+\* See Test2.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/Test2.tla b/PessimisticTransaction/Test2.tla
new file mode 100644
index 0000000..f781c24
--- /dev/null
+++ b/PessimisticTransaction/Test2.tla
@@ -0,0 +1,20 @@
+--------------------------------- MODULE Test2 ---------------------------------
+
+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
+c3 == 3
+
+Key == {k1, k2}
+OptimistiicClient == {c2, c3}
+PessimisticClient == {c1}
+ClientKey == c1 :> {k1, k2} @@ c2 :> {k1} @@ c3 :> {k2}
+ClientPrimary == c1 :> k1 @@ c2 :> k1 @@ c3 :> k2
+
+================================================================================