Merge branch 'develop' into rodin3

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

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

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