optimized deterministic check

src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java

 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 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);
-				tlaPrinter.moduleStringAppend(action2.getOperation().getText());
+					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

src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java

@@ -310,4 +310,8 @@ public class LTLFormulaVisitor extends DepthFirstAdapter {
         outAAndLtl(node);
     }
     
+    protected MachineContext getMachineContext(){
+    	return this.machineContext;
+    }
+	
 }

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;
 	}
-	
 }

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"

src/test/resources/ltl/CounterLTL.mch

 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