add progress bar to model checking dialog

de.prob.core/src/de/prob/core/command/ModelCheckingCommand.java

@@ -12,8 +12,7 @@ import de.prob.core.Animator;
 import de.prob.exceptions.ProBException;
 import de.prob.parser.ISimplifiedROMap;
 import de.prob.prolog.output.IPrologTermOutput;
-import de.prob.prolog.term.CompoundPrologTerm;
-import de.prob.prolog.term.PrologTerm;
+import de.prob.prolog.term.*;
 
 public final class ModelCheckingCommand implements IComposableCommand {
 	private final int time;
@@ -43,8 +42,7 @@ public final class ModelCheckingCommand implements IComposableCommand {
 
 	public static ModelCheckingResult<Result> modelcheck(final Animator a,
 			final int time, final List<String> options) throws ProBException {
-		ModelCheckingCommand command = new ModelCheckingCommand(
-				time, options);
+		ModelCheckingCommand command = new ModelCheckingCommand(time, options);
 		a.execute(command);
 		return command.getResult();
 	}
@@ -53,20 +51,32 @@ public final class ModelCheckingCommand implements IComposableCommand {
 		return result;
 	}
 
+	@Override
 	public void processResult(
 			final ISimplifiedROMap<String, PrologTerm> bindings)
 			throws CommandException {
 
 		CompoundPrologTerm term = (CompoundPrologTerm) bindings.get("Result");
-		result = new ModelCheckingResult<Result>(Result.class, term);
 
+		CompoundPrologTerm stats = (CompoundPrologTerm) bindings.get("Stats");
+		int processedTotal = ((IntegerPrologTerm) stats.getArgument(3))
+				.getValue().intValue();
+		int numStates = ((IntegerPrologTerm) stats.getArgument(1)).getValue()
+				.intValue();
+		int workedSoFar = (int) (1000 * Math.pow((double) processedTotal
+				/ numStates, 5));
+
+		result = new ModelCheckingResult<Result>(Result.class, term,
+				workedSoFar);
 	}
 
+	@Override
 	public void writeCommand(final IPrologTermOutput pto) {
 		pto.openTerm("do_modelchecking").printNumber(time).openList();
 		for (String o : options) {
 			pto.printAtom(o);
 		}
-		pto.closeList().printVariable("Result").closeTerm();
+		pto.closeList().printVariable("Result");
+		pto.printVariable("Stats").closeTerm();
 	}
 }

de.prob.core/src/de/prob/core/command/ModelCheckingResult.java

@@ -6,23 +6,23 @@
 
 package de.prob.core.command;
 
-import java.util.ArrayList;
-import java.util.List;
+import java.util.*;
 
-import de.prob.prolog.term.CompoundPrologTerm;
-import de.prob.prolog.term.PrologTerm;
+import de.prob.prolog.term.*;
 
 public class ModelCheckingResult<T extends Enum<T>> {
 
 	private final T result;
 	private final List<PrologTerm> arguments = new ArrayList<PrologTerm>();
+	private final int worked;
 
 	public ModelCheckingResult(final Class<T> enumeration,
-			final CompoundPrologTerm term) {
+			final CompoundPrologTerm term, int workDone) {
 		result = Enum.valueOf(enumeration, term.getFunctor());
 		for (int i = 1; i <= term.getArity(); i++) {
 			arguments.add(term.getArgument(i));
 		}
+		worked = workDone;
 	}
 
 	public PrologTerm getArgument(final int i) {
@@ -33,4 +33,7 @@ public class ModelCheckingResult<T extends Enum<T>> {
 		return result;
 	}
 
+	public int getWorked() {
+		return worked;
+	}
 }

de.prob.ui/src/de/prob/ui/eventb/ModelCheckingJob.java

@@ -6,20 +6,14 @@
 
 package de.prob.ui.eventb;
 
-import java.util.ArrayList;
-import java.util.List;
-import java.util.Set;
+import java.util.*;
 
-import org.eclipse.core.runtime.IProgressMonitor;
-import org.eclipse.core.runtime.IStatus;
-import org.eclipse.core.runtime.Status;
+import org.eclipse.core.runtime.*;
 import org.eclipse.core.runtime.jobs.Job;
 
 import de.prob.core.Animator;
-import de.prob.core.command.ModelCheckingCommand;
+import de.prob.core.command.*;
 import de.prob.core.command.ModelCheckingCommand.Result;
-import de.prob.core.command.ModelCheckingSearchOption;
-import de.prob.core.command.SetPreferenceCommand;
 import de.prob.exceptions.ProBException;
 
 public class ModelCheckingJob extends Job {
@@ -28,7 +22,8 @@ public class ModelCheckingJob extends Job {
 	private boolean abort = false;
 	private final List<String> options;
 	private final String symmetryOption;
-	private Result modelCheckingResult = null;
+	private ModelCheckingResult<Result> modelCheckingResult = null;
+	private int workedSoFar = 0;
 
 	public ModelCheckingJob(final String name,
 			final Set<ModelCheckingSearchOption> options,
@@ -43,7 +38,7 @@ public class ModelCheckingJob extends Job {
 	}
 
 	public Result getModelCheckingResult() {
-		return modelCheckingResult;
+		return modelCheckingResult.getResult();
 	}
 
 	@Override
@@ -52,16 +47,21 @@ public class ModelCheckingJob extends Job {
 			return Status.CANCEL_STATUS;
 		}
 
-		monitor.beginTask("Model checking", IProgressMonitor.UNKNOWN);
+		monitor.beginTask("Model checking", 1000);
 		while (!abort) {
 			try {
 				modelCheckingResult = doSomeModelchecking();
 				options.remove("inspect_existing_nodes");
-				monitor.worked(500);
+
+				int difference = modelCheckingResult.getWorked() - workedSoFar;
+				if (difference > 0) {
+					monitor.worked(difference);
+					workedSoFar = modelCheckingResult.getWorked();
+				}
 			} catch (ProBException e) {
 				return Status.CANCEL_STATUS; // Failed
 			}
-			abort = modelCheckingResult.isAbort() || monitor.isCanceled();
+			abort = getModelCheckingResult().isAbort() || monitor.isCanceled();
 		}
 		return Status.OK_STATUS;
 	}
@@ -76,9 +76,9 @@ public class ModelCheckingJob extends Job {
 		return true;
 	}
 
-	private Result doSomeModelchecking() throws ProBException {
-		return ModelCheckingCommand.modelcheck(animator, 500, options)
-				.getResult();
+	private ModelCheckingResult<Result> doSomeModelchecking()
+			throws ProBException {
+		return ModelCheckingCommand.modelcheck(animator, 500, options);
 	}
 
 }