diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index 68662fb60d13f6687245487ceee2180e6ce9ebf0..fcfd24d506f48b30bab29b4d02dcd1acb78072ee 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -281,6 +281,7 @@ public class TLC4B {
 			TLC4BGlobals.setCreateTraceFile(!line.hasOption(NOTRACE.arg()));
 			TLC4BGlobals.setDeleteOnExit(line.hasOption(DEL.arg()));
 			TLC4BGlobals.setPartialInvariantEvaluation(line.hasOption(PARINVEVAL.arg()));
+			TLC4BGlobals.setPrintCoverage(line.hasOption(COVERAGE.arg()));
 
 			if (line.hasOption(TMP.arg())) {
 				buildDir = new File(System.getProperty("java.io.tmpdir"));
diff --git a/src/main/java/de/tlc4b/TLC4BCliOptions.java b/src/main/java/de/tlc4b/TLC4BCliOptions.java
index d9fe2e12c9a8cc738122de1b31da78ed4bea9660..bb86ae433d46e8d588b5874fcc9844d17c24bcf8 100644
--- a/src/main/java/de/tlc4b/TLC4BCliOptions.java
+++ b/src/main/java/de/tlc4b/TLC4BCliOptions.java
@@ -31,7 +31,8 @@ public class TLC4BCliOptions {
 		LTLFORMULA("ltlformula", "provide an additional LTL formula", String.class),
 		VERBOSE("verbose", "put TLC4B in verbose mode", null),
 		SILENT("silent", "put TLC4B in silent mode", null),
-		OUTPUT("output", "provide path for output directory", String.class);
+		OUTPUT("output", "provide path for output directory", String.class),
+		COVERAGE("coverage", "print operation coverage", null);
 
 		private final String arg, desc;
 		private final Class<?> expectsArg;
diff --git a/src/main/java/de/tlc4b/Translator.java b/src/main/java/de/tlc4b/Translator.java
index 407184590e94dec41cdc4c50b7f130a3f50c5e41..159f16730f1e0c56280684b4d75679d534047211 100644
--- a/src/main/java/de/tlc4b/Translator.java
+++ b/src/main/java/de/tlc4b/Translator.java
@@ -120,8 +120,9 @@ public class Translator {
 		machineContext.analyseMachine();
 
 		this.machineName = machineContext.getMachineName();
-		if (machineContext.machineContainsOperations()) {
-			TLC4BGlobals.setPrintCoverage(true);
+		// ignore coverage option if machine contains no operations
+		if (!machineContext.machineContainsOperations()) {
+			TLC4BGlobals.setPrintCoverage(false);
 		}
 
 		Typechecker typechecker = new Typechecker(machineContext);