diff --git a/ClientCentric2PLBug_MC.cfg b/ClientCentric2PLBug_MC.cfg
new file mode 100644
index 0000000..632b62f
--- /dev/null
+++ b/ClientCentric2PLBug_MC.cfg
@@ -0,0 +1,32 @@
+CONSTANTS
+  t1 = t1
+  t2 = t2
+  t3 = t3
+  t4 = t4
+CONSTANTS
+  r1 = r1
+  r2 = r2
+  r3 = r3
+
+CONSTANT
+  transactions <- mc_transactions
+CONSTANT
+  resources <- mc_resources
+SYMMETRY mc_symm
+
+SPECIFICATION Spec
+
+INVARIANTS
+  TypeOK
+  CCTypeOK
+  Atomicity
+  Serializable
+\*   SerializabilityDebug
+\*   Serializable
+\*   SnapshotIsolation
+\*   ReadCommitted
+\*   ReadUncommitted
+
+\* Takes a long time to check
+\* PROPERTY
+\*   AllTransactionsFinish
diff --git a/ClientCentric2PLBug_MC.tla b/ClientCentric2PLBug_MC.tla
new file mode 100644
index 0000000..3640756
--- /dev/null
+++ b/ClientCentric2PLBug_MC.tla
@@ -0,0 +1,15 @@
+---- MODULE ClientCentric2PLBug_MC ----
+EXTENDS ClientCentric2PLBug, TLC
+
+CONSTANTS
+t1, t2, t3, t4
+CONSTANTS
+r1, r2, r3
+
+mc_transactions == {t1,t2,t3}
+mc_resources == {r1,r2}
+mc_symm == Permutations(mc_transactions) \union Permutations(mc_resources)
+
+SerializabilityDebug == CC!SerializabilityDebug(InitialState, ccTransactions)
+
+=============================================================================
diff --git a/Util.tla b/Util.tla
new file mode 100644
index 0000000..9bcdfbe
--- /dev/null
+++ b/Util.tla
@@ -0,0 +1,45 @@
+-------------------------------- MODULE Util --------------------------------
+EXTENDS Sequences, FiniteSets, Naturals, TLC
+
+\* Utilies from Practical TLA+
+ReduceSet(op(_, _), set, acc) ==
+  LET f[s \in SUBSET set] == \* here's where the magic is
+    IF s = {} THEN acc
+    ELSE LET x == CHOOSE x \in s: TRUE
+         IN op(x, f[s \ {x}])
+  IN f[set]
+ReduceSeq(op(_, _), seq, acc) == 
+  ReduceSet(LAMBDA i, a: op(seq[i], a), DOMAIN seq, acc)
+\* Pulls an indice of the sequence for elem.
+Index(seq, elem) == CHOOSE i \in 1..Len(seq): seq[i] = elem
+\* end from Practical TLA+
+
+Range(T) == { T[x] : x \in DOMAIN T }
+    
+SeqToSet(s) == {s[i] : i \in DOMAIN s}
+Last(seq) == seq[Len(seq)]
+IsEmpty(seq) == Len(seq) = 0
+\* Remove all occurences of `elem` from `seq`
+Remove(seq, elem) == SelectSeq(seq, LAMBDA e: e /= elem)
+
+\* Dual to UNION on intersect
+INTERSECTION(setOfSets) == ReduceSet(\intersect, setOfSets, UNION setOfSets)
+
+\* Borrowed from Stephan Merz. TLA+ Case Study: A Resource Allocator. [Intern report] A04-R-101 || merz04a, 2004, 20 p. ffinria-00107809f
+(* The set of permutations of a finite set, represented as sequences.  *)
+PermSeqs(S) ==
+  LET perms[ss \in SUBSET S] ==
+       IF ss = {} THEN { << >> }
+       ELSE LET ps == [ x \in ss |-> 
+                        { Append(sq,x) : sq \in perms[ss \ {x}] } ]
+            IN  UNION { ps[x] : x \in ss }
+  IN  perms[S]
+
+\* Helper to write "unit test" ASSUMES which print when false
+test(lhs, rhs) == lhs /= rhs => Print(<<lhs, " IS NOT ", rhs>>, FALSE)
+
+
+=============================================================================
+\* Modification History
+\* Last modified Tue Jun 16 12:04:20 CEST 2020 by tim
+\* Created Tue Apr 28 16:43:24 CEST 2020 by tim