diff --git a/de.prob.core/src/de/prob/core/command/ModelCheckingCommand.java b/de.prob.core/src/de/prob/core/command/ModelCheckingCommand.java
index ce866b8124d49120152dca099eb364a00eb3e01f..31c294f4a59bb9277ed04993643dd3138031e6e6 100644
--- a/de.prob.core/src/de/prob/core/command/ModelCheckingCommand.java
+++ b/de.prob.core/src/de/prob/core/command/ModelCheckingCommand.java
@@ -63,11 +63,11 @@ public final class ModelCheckingCommand implements IComposableCommand {
 				.getValue().intValue();
 		int numStates = ((IntegerPrologTerm) stats.getArgument(1)).getValue()
 				.intValue();
-		int workedSoFar = (int) (1000 * Math.pow((double) processedTotal
-				/ numStates, 5));
+		int numTransitions = ((IntegerPrologTerm) stats.getArgument(2))
+				.getValue().intValue();
 
 		result = new ModelCheckingResult<Result>(Result.class, term,
-				workedSoFar);
+				processedTotal, numStates, numTransitions);
 	}
 
 	@Override
diff --git a/de.prob.core/src/de/prob/core/command/ModelCheckingResult.java b/de.prob.core/src/de/prob/core/command/ModelCheckingResult.java
index 5d35e00e0a3599ee60634801e227358795c5f5bb..b77ce406fcfdc610d6a9920fc68c8b198d7d6394 100644
--- a/de.prob.core/src/de/prob/core/command/ModelCheckingResult.java
+++ b/de.prob.core/src/de/prob/core/command/ModelCheckingResult.java
@@ -14,15 +14,18 @@ public class ModelCheckingResult<T extends Enum<T>> {
 
 	private final T result;
 	private final List<PrologTerm> arguments = new ArrayList<PrologTerm>();
-	private final int worked;
+	private final int processedTotal, numStates, numTransitions;
 
 	public ModelCheckingResult(final Class<T> enumeration,
-			final CompoundPrologTerm term, int workDone) {
+			final CompoundPrologTerm term, int total, int numStates,
+			int numTransitions) {
 		result = Enum.valueOf(enumeration, term.getFunctor());
 		for (int i = 1; i <= term.getArity(); i++) {
 			arguments.add(term.getArgument(i));
 		}
-		worked = workDone;
+		processedTotal = total;
+		this.numStates = numStates;
+		this.numTransitions = numTransitions;
 	}
 
 	public PrologTerm getArgument(final int i) {
@@ -33,7 +36,19 @@ public class ModelCheckingResult<T extends Enum<T>> {
 		return result;
 	}
 
+	public int getProcessedTotal() {
+		return processedTotal;
+	}
+
+	public int getNumStates() {
+		return numStates;
+	}
+
+	public int getNumTransitions() {
+		return numTransitions;
+	}
+
 	public int getWorked() {
-		return worked;
+		return (int) (1000 * Math.pow((double) processedTotal / numStates, 5));
 	}
 }
diff --git a/de.prob.ui/src/de/prob/ui/eventb/ModelCheckingJob.java b/de.prob.ui/src/de/prob/ui/eventb/ModelCheckingJob.java
index 48e5c687d6f5a31bb560d9f26a66d153ec842fa0..3081f89c204cc77fd1721fbf70153c1fc658e1ea 100644
--- a/de.prob.ui/src/de/prob/ui/eventb/ModelCheckingJob.java
+++ b/de.prob.ui/src/de/prob/ui/eventb/ModelCheckingJob.java
@@ -47,12 +47,19 @@ public class ModelCheckingJob extends Job {
 			return Status.CANCEL_STATUS;
 		}
 
-		monitor.beginTask("Model checking", 1000);
+		monitor.beginTask("Model Checking", 1000);
 		while (!abort) {
 			try {
 				modelCheckingResult = doSomeModelchecking();
 				options.remove("inspect_existing_nodes");
 
+				monitor.setTaskName("Model Checking - States: "
+						+ modelCheckingResult.getNumStates()
+						+ " (processed "
+						+ modelCheckingResult.getProcessedTotal()
+						+ ") - Transitions: "
+						+ modelCheckingResult.getNumTransitions());
+
 				int difference = modelCheckingResult.getWorked() - workedSoFar;
 				if (difference > 0) {
 					monitor.worked(difference);