diff --git a/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java b/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java
index 25d840475431d94911ed63627672c99cdf168ba8..1825a6f0c934c2787d4e41966a6eb4ab915a0c2f 100644
--- a/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java
+++ b/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java
@@ -1,7 +1,9 @@
 package de.tlc4b.ltl;
 
 import java.util.ArrayList;
+import java.util.Collection;
 import java.util.Iterator;
+import java.util.LinkedHashMap;
 import java.util.List;
 
 import de.be4.classicalb.core.parser.node.APredicateParseUnit;
@@ -183,20 +185,55 @@ public class LTLFormulaPrinter extends DepthFirstAdapter {
 	@Override
 	public void caseADetLtl(ADetLtl node) {
 		List<PActions> copy = new ArrayList<PActions>(node.getArgs());
-		for (int i = 0; i < copy.size(); i++) {
-			AOpActions action1 = (AOpActions) copy.get(i);
-			for (int j = i + 1; j < copy.size(); j++) {
-				if (!(i == 0 && j == 1)) {
+		LinkedHashMap<String, Node> operations = ltlFormulaVisitor
+				.getMachineContext().getOperations();
+		if (copy.size() > 1) {
+			tlaPrinter.moduleStringAppend("(");
+			for (int i = 0; i < copy.size() - 1; i++) {
+				if (i != 0) {
 					tlaPrinter.moduleStringAppend(" /\\ ");
 				}
-				tlaPrinter.moduleStringAppend("\\neg(ENABLED(");
-				tlaPrinter.moduleStringAppend(action1.getOperation().getText());
-				tlaPrinter.moduleStringAppend(") /\\ ENABLED(");
-				AOpActions action2 = (AOpActions) copy.get(j);
-				tlaPrinter.moduleStringAppend(action2.getOperation().getText());
+				AOpActions action1 = (AOpActions) copy.get(i);
+				String action1Name = action1.getOperation().getText();
+				Node op1 = operations.get(action1Name);
+				tlaPrinter.moduleStringAppend("(ENABLED(");
+				tlaPrinter.printOperationCall(op1);
+				tlaPrinter.moduleStringAppend(") => \\neg(");
+				for (int j = i + 1; j < copy.size(); j++) {
+					AOpActions action2 = (AOpActions) copy.get(j);
+					String action2Name = action2.getOperation().getText();
+					Node op2 = operations.get(action2Name);
+					if (j != i + 1) {
+						tlaPrinter.moduleStringAppend(" \\/ ");
+					}
+					tlaPrinter.moduleStringAppend("ENABLED(");
+					tlaPrinter.printOperationCall(op2);
+					tlaPrinter.moduleStringAppend(")");
+				}
 				tlaPrinter.moduleStringAppend("))");
 			}
+			tlaPrinter.moduleStringAppend(")");
+		} else { // only the single operation should be enabled
+				AOpActions action1 = (AOpActions) copy.get(0);
+				String action1Name = action1.getOperation().getText();
+				Node op1 = operations.get(action1Name);
+				tlaPrinter.moduleStringAppend("(ENABLED(");
+				tlaPrinter.printOperationCall(op1);
+				tlaPrinter.moduleStringAppend(") => \\neg(");
+				ArrayList<Node> remainingOperations = new ArrayList<Node>(operations.values());
+				remainingOperations.remove(op1);
+				for (int i = 0; i < remainingOperations.size(); i++) {
+					if (i != 0) {
+						tlaPrinter.moduleStringAppend(" \\/ ");
+					}
+					Node op2 = remainingOperations.get(i);
+					tlaPrinter.moduleStringAppend("ENABLED(");
+					tlaPrinter.printOperationCall(op2);
+					tlaPrinter.moduleStringAppend(")");
+				}
+				tlaPrinter.moduleStringAppend("))");
 		}
+
 	}
 
 	@Override
diff --git a/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java b/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
index ebf1e42b92941985baf2fb3e951de65e1a0e750c..6e9410cffd06cc0ad2d7e996253781956117348b 100644
--- a/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
+++ b/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
@@ -309,5 +309,9 @@ public class LTLFormulaVisitor extends DepthFirstAdapter {
         }
         outAAndLtl(node);
     }
+    
+    protected MachineContext getMachineContext(){
+    	return this.machineContext;
+    }
 	
 }
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index f5a381b752e29279bf8e44192e3797fc2eba1c25..ecfda97357213b9e8e13d9447f140af563956f4e 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());
@@ -2914,5 +2914,4 @@ public class TLAPrinter extends DepthFirstAdapter {
 	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 a8c982b5eb6c4b88317e4e2102561805fde4f410..574e89b4b548fa0505a5f28e299e11aca6fd689a 100644
--- a/src/test/java/de/tlc4b/ltl/LtlFormulaTest.java
+++ b/src/test/java/de/tlc4b/ltl/LtlFormulaTest.java
@@ -182,10 +182,20 @@ public class LtlFormulaTest {
 		String machine = "MACHINE test\n"
 				+ "OPERATIONS foo = skip; bar = skip; bazz = skip\n"
 				+ "END";
-	    String expected = "\\neg(ENABLED(foo) /\\ ENABLED(bar)) /\\ \\neg(ENABLED(foo)  /\\ ENABLED(bazz)) /\\ \\neg(ENABLED(bar) /\\ ENABLED(bazz))";
+	    String expected = "((ENABLED(foo) => \\neg(ENABLED(bar) \\/ ENABLED(bazz))) /\\ (ENABLED(bar) => \\neg(ENABLED(bazz))))";
 		compareLTLFormula(expected, machine, "deterministic(foo,bar,bazz)");
 	}
 	
+	
+	@Test
+	public void testDeterministicOnly() throws Exception {
+		String machine = "MACHINE test\n"
+				+ "OPERATIONS foo = skip; bar = skip; bazz = skip\n"
+				+ "END";
+	    String expected = "(ENABLED(foo) => \\neg(ENABLED(bar) \\/ ENABLED(bazz)))";
+		compareLTLFormula(expected, machine, "deterministic(foo)");
+	}
+	
 	@Test
 	public void testDeadlock() throws Exception {
 		String machine = "MACHINE test\n"
diff --git a/src/test/resources/ltl/CounterLTL.mch b/src/test/resources/ltl/CounterLTL.mch
index ce5fae9d50d5b15a073d10b1f7b56828c1f989ee..c5a57a450686931693b87bded6d8f72774cb9e92 100644
--- a/src/test/resources/ltl/CounterLTL.mch
+++ b/src/test/resources/ltl/CounterLTL.mch
@@ -1,6 +1,8 @@
 MACHINE CounterLTL
 DEFINITIONS
-ASSERT_LTL_1 == "F {x = 10}"
+ASSERT_LTL_1 == "F {x = 10}";
+ASSERT_LTL_2 == "G(not(deadlock))";
+ASSERT_LTL_3 == "G(deterministic(Inc,Reset))";
 VARIABLES x
 INVARIANT
  x : 1..10