Merge branch 'feature/cbc_refinement' into develop

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

+/**
+ * 
+ */
+package de.prob.core.command;
+
+import de.prob.core.domainobjects.Operation;
+import de.prob.parser.ISimplifiedROMap;
+import de.prob.prolog.output.IPrologTermOutput;
+import de.prob.prolog.term.ListPrologTerm;
+import de.prob.prolog.term.PrologTerm;
+
+public class ConstraintBasedRefinementCheckCommand implements
+		IComposableCommand {
+
+	public static enum ResultType {
+		VIOLATION_FOUND, NO_VIOLATION_FOUND, INTERRUPTED
+	};
+
+	public static class RefinementCheckCounterExample {
+		private final String eventName;
+		private final Operation step1, step2;
+
+		public RefinementCheckCounterExample(final String eventName,
+				final Operation step1, final Operation step2) {
+			this.eventName = eventName;
+			this.step1 = step1;
+			this.step2 = step2;
+		}
+
+		public String getEventName() {
+			return eventName;
+		}
+
+		public Operation getStep1() {
+			return step1;
+		}
+
+		public Operation getStep2() {
+			return step2;
+		}
+	}
+
+	private static final String COMMAND_NAME = "refinement_check";
+	private static final String RESULT_VARIABLE = "R";
+	private static final String RESULT_STRINGS_VARIABLE = "S";
+
+	private ResultType result;
+	private String resultsString = "";
+
+	public ConstraintBasedRefinementCheckCommand() {
+	}
+
+	public ResultType getResult() {
+		return result;
+	}
+
+	@Override
+	public void writeCommand(final IPrologTermOutput pto) {
+		pto.openTerm(COMMAND_NAME);
+		pto.printVariable(RESULT_STRINGS_VARIABLE);
+		pto.printVariable(RESULT_VARIABLE);
+		pto.closeTerm();
+	}
+
+	@Override
+	public void processResult(
+			final ISimplifiedROMap<String, PrologTerm> bindings)
+			throws CommandException {
+		final PrologTerm resultTerm = bindings.get(RESULT_VARIABLE);
+		final ResultType result;
+
+		final ListPrologTerm resultStringTerm = (ListPrologTerm) bindings
+				.get(RESULT_STRINGS_VARIABLE);
+
+		System.out.println(resultStringTerm.toString());
+
+		for (PrologTerm t : resultStringTerm) {
+			resultsString += PrologTerm.atomicString(t) + "\n";
+		}
+
+		if (resultTerm.hasFunctor("time_out", 0)) {
+			result = ResultType.INTERRUPTED;
+		} else if (resultTerm.hasFunctor("true", 0)) { // Errors were found
+			result = ResultType.VIOLATION_FOUND;
+			// TODO extract message
+		} else if (resultTerm.hasFunctor("false", 0)) { // Errors were found
+			result = ResultType.NO_VIOLATION_FOUND;
+		} else
+			throw new CommandException(
+					"unexpected result from refinement check: " + resultTerm);
+		this.result = result;
+	}
+
+	public String getResultsString() {
+		return resultsString;
+	}
+}

de.prob.ui/plugin.xml

@@ -303,6 +303,11 @@
             id="de.prob.ui.invariant_check"
             name="Check for Invariant Preservation">
       </command>
+      <command
+            categoryId="de.prob.ui.commands.category"
+            id="de.prob.ui.refinement_check"
+            name="Validate Refinement">
+      </command>
       <command
             categoryId="de.prob.ui.commands.category"
             id="de.prob.ui.opview.checks"
@@ -740,6 +745,20 @@
             </with>
          </enabledWhen>
       </handler>
+      <handler
+            commandId="de.prob.ui.refinement_check">
+         <enabledWhen>
+            <with
+                  variable="de.prob.core.model_loaded">
+               <equals
+                     value="enabled">
+               </equals>
+            </with>
+         </enabledWhen>
+         <class
+               class="de.prob.ui.refinementcheck.RefinementCheckHandler">
+         </class>
+      </handler>
 <!--      <handler
             commandId="de.prob.ui.startdmc">
          <class
@@ -1061,6 +1080,13 @@
                mnemonic="I"
                style="push">
          </command>
+         <command
+               commandId="de.prob.ui.refinement_check"
+               icon="icons/CBCInvariantCheck.png"
+               label="Refinement Checking"
+               mnemonic="R"
+               style="push">
+         </command>
       </menuContribution>
       <!--
       <menuContribution

de.prob.ui/src/de/prob/ui/refinementcheck/RefinementCheckFinishedListener.java

+/**
+ * 
+ */
+package de.prob.ui.refinementcheck;
+
+import org.eclipse.jface.dialogs.MessageDialog;
+import org.eclipse.swt.SWT;
+import org.eclipse.swt.widgets.Shell;
+
+import de.prob.core.Animator;
+import de.prob.core.ProBJobFinishedListener;
+import de.prob.core.command.ConstraintBasedRefinementCheckCommand;
+import de.prob.core.command.ConstraintBasedRefinementCheckCommand.ResultType;
+import de.prob.core.command.IComposableCommand;
+import de.prob.logging.Logger;
+
+/**
+ * 
+ * @author krings
+ * 
+ */
+public class RefinementCheckFinishedListener extends ProBJobFinishedListener {
+	private final Shell shell;
+
+	public RefinementCheckFinishedListener(final Shell shell) {
+		this.shell = shell;
+	}
+
+	@Override
+	protected void showResult(final IComposableCommand command,
+			final Animator animator) {
+		final ConstraintBasedRefinementCheckCommand refCmd = (ConstraintBasedRefinementCheckCommand) command;
+
+		final ResultType result = refCmd.getResult();
+		final int dialogType;
+		final String dialogTitle;
+		final String message;
+
+		switch (result) {
+		case INTERRUPTED:
+			dialogType = MessageDialog.WARNING;
+			dialogTitle = "User Interrupt";
+			message = "The refinement check has been interrupted by the user.";
+			break;
+		case NO_VIOLATION_FOUND:
+			dialogType = MessageDialog.INFORMATION;
+			dialogTitle = "No Refinement Violation found";
+			message = "No possible refinement violation has been found.";
+			break;
+		case VIOLATION_FOUND:
+			dialogType = MessageDialog.ERROR;
+			dialogTitle = "Refinement Violation found";
+			message = refCmd.getResultsString();
+			break;
+		default:
+			Logger.notifyUser("Unexpected result: " + result);
+			return;
+		}
+		if (shell.isDisposed()) {
+			System.out.println("Refinement Check finished: " + dialogTitle);
+		} else {
+			final Runnable runnable = new Runnable() {
+				@Override
+				public void run() {
+					MessageDialog.open(dialogType, shell, dialogTitle, message,
+							SWT.NONE);
+				}
+			};
+			shell.getDisplay().asyncExec(runnable);
+		}
+	}
+
+}

de.prob.ui/src/de/prob/ui/refinementcheck/RefinementCheckHandler.java

+/**
+ * 
+ */
+package de.prob.ui.refinementcheck;
+
+import org.eclipse.core.commands.AbstractHandler;
+import org.eclipse.core.commands.ExecutionEvent;
+import org.eclipse.core.commands.ExecutionException;
+import org.eclipse.core.runtime.jobs.Job;
+import org.eclipse.jface.dialogs.MessageDialog;
+import org.eclipse.swt.widgets.Shell;
+import org.eclipse.ui.handlers.HandlerUtil;
+
+import de.prob.core.Animator;
+import de.prob.core.ProBCommandJob;
+import de.prob.core.command.ConstraintBasedRefinementCheckCommand;
+
+/**
+ * 
+ * @author krings
+ */
+public class RefinementCheckHandler extends AbstractHandler {
+	@Override
+	public Object execute(final ExecutionEvent event) throws ExecutionException {
+		final Shell shell = HandlerUtil.getActiveShell(event);
+		final Animator animator = Animator.getAnimator();
+		if (animator.isMachineLoaded()) {
+			performRefinementCheck(animator, shell);
+		} else {
+			MessageDialog
+					.openError(
+							shell,
+							"Error: No ProB animation running",
+							"To perform a constraint based refinement check, please start the animation of the model first.");
+		}
+		return null;
+	}
+
+	private void performRefinementCheck(final Animator animator,
+			final Shell shell) throws ExecutionException {
+		final ConstraintBasedRefinementCheckCommand command = new ConstraintBasedRefinementCheckCommand();
+		final Job job = new ProBCommandJob(
+				"Performing CBC Refinement Checking", animator, command);
+		job.setUser(true);
+		job.addJobChangeListener(new RefinementCheckFinishedListener(shell));
+		job.schedule();
+	}
+
+}