diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index 880bd4de78a2a2c8d7802707e7b770ab59f8be98..046c82279cd6a7abbe6b86d2e44f2b70e0571f68 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -317,6 +317,13 @@ public class TLC4B {
 				}
 				TLC4BGlobals.setWorkers(Integer.parseInt(workers));
 			}
+			if (line.hasOption(DFID.arg())) {
+				String dfid_initial_depth = line.getOptionValue(DFID.arg());
+				if (dfid_initial_depth == null) {
+					throw new TLC4BIOException("Error: Number required after option '-dfid'.");
+				}
+				TLC4BGlobals.setDfidInitialDepth(Integer.parseInt(dfid_initial_depth));
+			}
 			if (line.hasOption(CONSTANTSSETUP.arg())) {
 				TLC4BGlobals.setProBconstantsSetup(true);
 				constantsSetup = line.getOptionValue(CONSTANTSSETUP.arg());
diff --git a/src/main/java/de/tlc4b/TLC4BCliOptions.java b/src/main/java/de/tlc4b/TLC4BCliOptions.java
index 70fce665b003f629057ae870ddfa2a8f06d1932c..c71b74a53496b846cb2f4e7372af8801e842106d 100644
--- a/src/main/java/de/tlc4b/TLC4BCliOptions.java
+++ b/src/main/java/de/tlc4b/TLC4BCliOptions.java
@@ -29,6 +29,7 @@ public class TLC4BCliOptions {
 		DEFAULT_SETSIZE("default_setsize", "", Integer.class),
 		MININT("minint", "", Integer.class),
 		WORKERS("workers", "", Integer.class),
+		DFID("dfid", "depth-first model checking with iterative deepening, specify initial depth", Integer.class),
 		CONSTANTSSETUP("constantssetup", "use constants found by ProB for TLC model checking", String.class),
 		LTLFORMULA("ltlformula", "", String.class),
 		VERBOSE("verbose", "put TLC4B in verbose mode", null),
diff --git a/src/main/java/de/tlc4b/TLC4BGlobals.java b/src/main/java/de/tlc4b/TLC4BGlobals.java
index 93b492cc70df3504acf923ac33190398f596af57..8a510ca7719bf657b8bdad8ecbf209bc63bcc1a9 100644
--- a/src/main/java/de/tlc4b/TLC4BGlobals.java
+++ b/src/main/java/de/tlc4b/TLC4BGlobals.java
@@ -34,6 +34,7 @@ public class TLC4BGlobals {
 	private static boolean forceTLCToEvalConstants;
 
 	private static int workers;
+	private static int dfid_initial_depth;
 
 	private static boolean runTestscript;
 
@@ -57,12 +58,15 @@ public class TLC4BGlobals {
 		printCoverage = false;
 		forceTLCToEvalConstants = false;
 		checkOnlyMainAssertions = false;
+		verbose = false;
+		silent = false;
 
 		proBconstantsSetup = false;
 
 		cleanup = true;
 
 		workers = 1;
+		dfid_initial_depth = -1; // option not selected
 
 		// for debugging purposes
 		runTLC = true;
@@ -147,20 +151,20 @@ public class TLC4BGlobals {
 		partialInvariantEvaluation = b;
 	}
 
-	public static void setDEFERRED_SET_SIZE(int DEFERRED_SET_SIZE) {
-		TLC4BGlobals.DEFERRED_SET_SIZE = DEFERRED_SET_SIZE;
+	public static void setDEFERRED_SET_SIZE(int deferredSetSize) {
+		TLC4BGlobals.DEFERRED_SET_SIZE = deferredSetSize;
 	}
 
-	public static void setMAX_INT(int mAX_INT) {
-		MAX_INT = mAX_INT;
+	public static void setMAX_INT(int maxInt) {
+		TLC4BGlobals.MAX_INT = maxInt;
 	}
 
-	public static void setMIN_INT(int mIN_INT) {
-		MIN_INT = mIN_INT;
+	public static void setMIN_INT(int minInt) {
+		TLC4BGlobals.MIN_INT = minInt;
 	}
 
-	public static void setGOAL(boolean gOAL) {
-		checkGOAL = gOAL;
+	public static void setGOAL(boolean goal) {
+		TLC4BGlobals.checkGOAL = goal;
 	}
 
 	public static void setDeadlockCheck(boolean deadlockCheck) {
@@ -203,6 +207,14 @@ public class TLC4BGlobals {
 		return TLC4BGlobals.workers;
 	}
 
+	public static void setDfidInitialDepth(int depth) {
+		TLC4BGlobals.dfid_initial_depth = depth;
+	}
+
+	public static int getDfidInitialDepth() {
+		return TLC4BGlobals.dfid_initial_depth;
+	}
+
 	public static boolean isCleanup() {
 		return cleanup;
 	}
diff --git a/src/main/java/de/tlc4b/TLCRunner.java b/src/main/java/de/tlc4b/TLCRunner.java
index 7bbb47fdeede04b97b47278d8ea1ad83a72656c2..9f06c585c1c3f7adb9ba92f28ac6d732af4c0149 100644
--- a/src/main/java/de/tlc4b/TLCRunner.java
+++ b/src/main/java/de/tlc4b/TLCRunner.java
@@ -106,6 +106,10 @@ public class TLCRunner {
 			list.add("-workers");
 			list.add("" + TLC4BGlobals.getWorkers());
 		}
+		if (TLC4BGlobals.getDfidInitialDepth() >= 0) {
+			list.add("-dfid");
+			list.add("" + TLC4BGlobals.getDfidInitialDepth());
+		}
 
 		if (TLC4BGlobals.isPrintCoverage()) {
 			list.add("-nowarning");
diff --git a/src/main/java/de/tlc4b/tlc/TLCResults.java b/src/main/java/de/tlc4b/tlc/TLCResults.java
index f59445b1038f98c246a55daca505a80a47a8e51d..99c032da73e734157abe48766cf8047e41a9f800 100644
--- a/src/main/java/de/tlc4b/tlc/TLCResults.java
+++ b/src/main/java/de/tlc4b/tlc/TLCResults.java
@@ -230,13 +230,11 @@ public class TLCResults implements ToolGlobals {
 				break;
 
 			case EC.TLC_STATS:
+			case EC.TLC_STATS_DFID:
 				numberOfTransitions = Integer.parseInt(m.getParameters()[0]);
 				numberOfDistinctStates = Integer.parseInt(m.getParameters()[1]);
 				break;
 
-			case EC.TLC_STATS_DFID:
-				break;
-
 			case EC.TLC_SUCCESS:
 				tlcResult = TLCResult.NoError;
 				break;
diff --git a/src/test/java/de/tlc4b/tlc/integration/BasicTest.java b/src/test/java/de/tlc4b/tlc/integration/BasicTest.java
index 0204d721ccd20f40c14be5d5af6190f414719a8a..0c22eb6fa3f9b00c9ea63c4ede998494b397b8cf 100644
--- a/src/test/java/de/tlc4b/tlc/integration/BasicTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/BasicTest.java
@@ -12,6 +12,7 @@ import org.junit.runner.RunWith;
 import java.io.File;
 import java.util.ArrayList;
 
+import static de.tlc4b.TLC4BCliOptions.TLCOption.DFID;
 import static de.tlc4b.tlc.TLCResults.TLCResult.NoError;
 import static de.tlc4b.util.TestUtil.test;
 import static org.junit.Assert.assertEquals;
@@ -33,6 +34,12 @@ public class BasicTest extends AbstractParseMachineTest {
 		assertEquals(error, test(a));
 	}
 
+	@Test
+	public void testRunTLCDFS() throws Exception {
+		String[] a = new String[] { machine.getPath(), "-" + DFID.arg(), "20" };
+		assertEquals(error, test(a));
+	}
+
 	@Config
 	public static Configuration getConfig() {
 		final ArrayList<TestPair> list = new ArrayList<>();