diff --git a/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java b/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java
index 0f5546fe39373a5d3d12fc5e661fe81349950cef..564bcfd704ee9ca027aadfbc2a69ad26719ab1db 100644
--- a/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java
+++ b/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java
@@ -1,15 +1,18 @@
 package de.tlc4b.ltl;
 
 import java.util.ArrayList;
+import java.util.Iterator;
 import java.util.List;
 
 import de.be4.classicalb.core.parser.node.APredicateParseUnit;
 import de.be4.classicalb.core.parser.node.Node;
+import de.be4.classicalb.core.parser.node.POperation;
 import de.be4.classicalb.core.parser.node.Start;
 import de.be4.ltl.core.parser.analysis.DepthFirstAdapter;
 import de.be4.ltl.core.parser.node.AAndFair1Ltl;
 import de.be4.ltl.core.parser.node.AAndFair2Ltl;
 import de.be4.ltl.core.parser.node.AAndLtl;
+import de.be4.ltl.core.parser.node.ADeadlockLtl;
 import de.be4.ltl.core.parser.node.ADetLtl;
 import de.be4.ltl.core.parser.node.AEnabledLtl;
 import de.be4.ltl.core.parser.node.AExistsLtl;
@@ -194,8 +197,27 @@ public class LTLFormulaPrinter extends DepthFirstAdapter {
 				tlaPrinter.moduleStringAppend("))");
 			}
 		}
-		
-
 	}
 
+	
+    @Override
+    public void caseADeadlockLtl(ADeadlockLtl node)
+    {
+    	tlaPrinter.moduleStringAppend("\\neg(");
+    	
+    	
+    Iterator<POperation> itr = this.tlaPrinter.getTLAModule().getOperations().iterator();
+		while (itr.hasNext()) {
+			Node operation = itr.next();
+			tlaPrinter.moduleStringAppend("ENABLED(");
+			tlaPrinter.printOperationCall(operation);
+			tlaPrinter.moduleStringAppend(")");
+			if (itr.hasNext()) {
+				tlaPrinter.moduleStringAppend(" \\/ ");
+			}
+		}
+    	
+        tlaPrinter.moduleStringAppend(")");
+    }
+	
 }
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 1b60e57c5280a665776bbfe77815548c9b0a2b86..9903b944a5be2b311eb1b0855f215ed251a9cc01 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -523,7 +523,7 @@ public class TLAPrinter extends DepthFirstAdapter {
 		moduleStringAppend("\n");
 	}
 
-	private void printOperationCall(Node operation) {
+	public void printOperationCall(Node operation) {
 		AOperation op = (AOperation) operation;
 		List<PExpression> newList = new ArrayList<PExpression>();
 		newList.addAll(op.getParameters());
@@ -2908,7 +2908,11 @@ public class TLAPrinter extends DepthFirstAdapter {
 	}
 
 	public String geTranslatedLTLFormula() {
-		return translatedLTLFormula.toString();
+		return this.translatedLTLFormula.toString();
 	}
 
+	public TLAModule getTLAModule(){
+		return this.tlaModule;
+	}
+	
 }
diff --git a/src/test/java/de/tlc4b/ltl/LtlFormulaTest.java b/src/test/java/de/tlc4b/ltl/LtlFormulaTest.java
index 35465bdd68353f5f8cdc87a62c4eb9e5eb4d89e6..5647ff54f4722e6a84fec781e3be70bd9130ab51 100644
--- a/src/test/java/de/tlc4b/ltl/LtlFormulaTest.java
+++ b/src/test/java/de/tlc4b/ltl/LtlFormulaTest.java
@@ -186,6 +186,24 @@ public class LtlFormulaTest {
 		compareLTLFormula(expected, machine, "deterministic(foo,bar,bazz)");
 	}
 	
+	@Test
+	public void testDeadlock() throws Exception {
+		String machine = "MACHINE test\n"
+				+ "OPERATIONS foo = skip; bar = skip; bazz = skip\n"
+				+ "END";
+	    String expected = "\\neg(ENABLED(foo) \\/ ENABLED(bar) \\/ ENABLED(bazz))";
+		compareLTLFormula(expected, machine, "deadlock");
+	}
+	
+	@Test
+	public void testDeadlockOperationParameter() throws Exception {
+		String machine = "MACHINE test\n"
+				+ "OPERATIONS foo(a) = SELECT a : 1..3 THEN skip END\n"
+				+ "END";
+	    String expected = "\\neg(ENABLED(\\E a \\in (1 .. 3) : foo(a)))";
+		compareLTLFormula(expected, machine, "deadlock");
+	}
+	
 	@Test
 	public void testWeakFairness() throws Exception {
 		String machine = "MACHINE test\n"