diff --git a/src/main/java/de/tlc4b/TLC4BGlobals.java b/src/main/java/de/tlc4b/TLC4BGlobals.java
index faf0db7a8bff8c80c820edd6993d05001d6277ab..88abc3976ac94c1121fec8d470b9e691da7037c3 100644
--- a/src/main/java/de/tlc4b/TLC4BGlobals.java
+++ b/src/main/java/de/tlc4b/TLC4BGlobals.java
@@ -14,6 +14,7 @@ public class TLC4BGlobals {
 	private static boolean proBconstantsSetup;
 	private static boolean partialInvariantEvaluation;
 	private static boolean useSymmetry;
+	private static boolean printCoverage;
 
 	private static boolean deleteFilesOnExit;
 
@@ -49,6 +50,7 @@ public class TLC4BGlobals {
 		checkWD = false;
 		partialInvariantEvaluation = false;
 		useSymmetry = false;
+		printCoverage = false;
 		setForceTLCToEvalConstants(true);
 
 		setProBconstantsSetup(false);
@@ -247,5 +249,13 @@ public class TLC4BGlobals {
 	public static void setSymmetryUse(boolean b) {
 		useSymmetry = b;
 	}
+	
+	public static void setPrintCoverage(boolean b){
+		printCoverage = b;
+	}
+	
+	public static boolean isPrintCoverage(){ 
+		return printCoverage;
+	}
 
 }
diff --git a/src/main/java/de/tlc4b/TLCRunner.java b/src/main/java/de/tlc4b/TLCRunner.java
index 8be4aade3d8aaf2bcd2432cdfbe6b1cfd7a9aabc..9e67b65b9d415675db0f2b6c948b5315cf91629d 100644
--- a/src/main/java/de/tlc4b/TLCRunner.java
+++ b/src/main/java/de/tlc4b/TLCRunner.java
@@ -103,6 +103,12 @@ public class TLCRunner {
 			list.add("-workers");
 			list.add("" + TLC4BGlobals.getWorkers());
 		}
+		
+		if(TLC4BGlobals.isPrintCoverage()){
+			list.add("-nowarning");
+			list.add("-coverage");
+			list.add(""+ 100);
+		}
 
 		//list.add("-config");
 		//list.add(machineName + ".cfg");
diff --git a/src/main/java/de/tlc4b/Translator.java b/src/main/java/de/tlc4b/Translator.java
index 135c9f0647e5633229c4e08ea886c8d3d3c15c6a..efc50e442f88dccbcfd455b4b4a62d707137f6a5 100644
--- a/src/main/java/de/tlc4b/Translator.java
+++ b/src/main/java/de/tlc4b/Translator.java
@@ -111,6 +111,10 @@ public class Translator {
 		MachineContext machineContext = new MachineContext(machineName, start,
 				ltlFormula, constantsSetup);
 		this.machineName = machineContext.getMachineName();
+		if(machineContext
+				.machineContainsOperations()){
+			TLC4BGlobals.setPrintCoverage(true);
+		}
 
 		Typechecker typechecker = new Typechecker(machineContext);
 		UnchangedVariablesFinder unchangedVariablesFinder = new UnchangedVariablesFinder(
@@ -155,7 +159,8 @@ public class Translator {
 		TLAPrinter printer = new TLAPrinter(machineContext, typechecker,
 				unchangedVariablesFinder, precedenceCollector, usedModules,
 				typeRestrictor, generator.getTlaModule(),
-				generator.getConfigFile(), primedNodesMarker, renamer, invariantPreservationAnalysis);
+				generator.getConfigFile(), primedNodesMarker, renamer,
+				invariantPreservationAnalysis);
 		printer.start();
 		moduleString = printer.getStringbuilder().toString();
 		configString = printer.getConfigString().toString();
@@ -197,9 +202,8 @@ public class Translator {
 		return usedStandardModules;
 	}
 
-	public String getTranslatedLTLFormula(){
+	public String getTranslatedLTLFormula() {
 		return translatedLTLFormula;
 	}
 
-	
 }
diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
index 0db6b07057522f599df6ea665ddd52d8707e3ebd..2002c160c94fe184440603cbfd4b1de6edf625aa 100644
--- a/src/main/java/de/tlc4b/analysis/MachineContext.java
+++ b/src/main/java/de/tlc4b/analysis/MachineContext.java
@@ -1090,6 +1090,10 @@ public class MachineContext extends DepthFirstAdapter {
 		return invariantMachineClause;
 	}
 
+	public boolean machineContainsOperations() {
+		return operations.size() > 0;
+	}
+
 	public AInitialisationMachineClause getInitialisationMachineClause() {
 		return initialisationMachineClause;
 	}