diff --git a/TLA+/DieHard.cfg b/TLA+/DieHard.cfg
new file mode 100644
index 0000000..5364dc3
--- /dev/null
+++ b/TLA+/DieHard.cfg
@@ -0,0 +1,3 @@
+INIT Init
+NEXT Next
+INVARIANT TypeOk Impossible
diff --git a/TLA+/DieHard.tla b/TLA+/DieHard.tla
new file mode 100644
index 0000000..c1e2867
--- /dev/null
+++ b/TLA+/DieHard.tla
@@ -0,0 +1,47 @@
+----------------------------- MODULE DieHard -----------------------------
+EXTENDS Naturals 
+VARIABLES small, big
+
+Init == /\ small = 0
+        /\ big = 0
+
+TypeOk == /\ big \in 0..5
+          /\ small \in 0..3
+
+FillBig == /\ big' = 5
+           /\ small' = small
+
+FillSmall == /\ small' = 3
+             /\ big' = big
+
+EmptyBig == /\ big' = 0
+            /\ small' = small
+
+EmptySmall == /\ small' = 0
+              /\ big' = big
+
+Small2Big == IF big + small > 5
+            THEN /\ big' = 5
+                 /\ small' = (big + small) - 5
+            ELSE /\ big' = big + small
+                 /\ small' = 0
+
+Big2Small == IF big + small > 3
+            THEN /\ small' = 3
+                 /\ big' = (big + small) - 3
+            ELSE /\ small' = big + small
+                 /\ big' = 0
+
+Next == \/ Big2Small
+        \/ Small2Big
+        \/ EmptyBig
+        \/ EmptySmall
+        \/ FillBig
+        \/ FillSmall
+
+Impossible == big # 4
+
+=============================================================================
+\* Modification History
+\* Last modified Fri Feb 28 17:31:43 EST 2025 by danesabo
+\* Created Fri Feb 28 17:23:34 EST 2025 by danesabo