add assertion checking to prob plugin. an existing error state is not displayed yet.

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

+/**
+ * 
+ */
+package de.prob.core.command;
+
+import de.prob.parser.ISimplifiedROMap;
+import de.prob.prolog.output.IPrologTermOutput;
+import de.prob.prolog.term.ListPrologTerm;
+import de.prob.prolog.term.PrologTerm;
+
+/**
+ * This command makes ProB search for a deadlock with an optional predicate to
+ * limit the search space.
+ * 
+ * @author plagge
+ */
+public class ConstraintBasedAssertionCheckCommand implements IComposableCommand {
+
+	public static enum ResultType {
+		TIMEOUT, COUNTER_EXAMPLE, NO_COUNTER_EXAMPLE
+	};
+
+	private static final String COMMAND_NAME = "cbc_static_assertion_violation_checking";
+	private static final String RESULT_VARIABLE = "R";
+
+	private ResultType result;
+	private ListPrologTerm counterExampleState;
+
+	public ConstraintBasedAssertionCheckCommand() {
+	}
+
+	public ResultType getResult() {
+		return result;
+	}
+
+	public ListPrologTerm getCounterExampleState() {
+		return counterExampleState;
+	}
+
+	@Override
+	public void writeCommand(final IPrologTermOutput pto) {
+		pto.openTerm(COMMAND_NAME);
+		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;
+		if (resultTerm.hasFunctor("time_out", 0)) {
+			result = ResultType.TIMEOUT;
+		} else if (resultTerm.hasFunctor("no_counterexample_found", 0)) {
+			result = ResultType.NO_COUNTER_EXAMPLE;
+		} else if (resultTerm.hasFunctor("counterexample_found", 1)) {
+			counterExampleState = (ListPrologTerm) resultTerm.getArgument(1);
+			result = ResultType.COUNTER_EXAMPLE;
+		} else
+			throw new CommandException(
+					"unexpected result from deadlock check: " + resultTerm);
+		this.result = result;
+
+	}
+}

de.prob.ui/plugin.xml

@@ -355,6 +355,11 @@
             id="de.prob.ui.newcore.export"
             name="Export for new Core">
       </command>
+      <command
+            categoryId="de.prob.ui.commands.category"
+            id="de.prob.ui.assertion_check"
+            name="Check Context Theorems">
+      </command>
    </extension>
    <extension
          point="org.eclipse.ui.handlers">
@@ -759,6 +764,20 @@
                class="de.prob.ui.refinementcheck.RefinementCheckHandler">
          </class>
       </handler>
+      <handler
+            commandId="de.prob.ui.assertion_check">
+         <class
+               class="de.prob.ui.deadlock.AssertionCheckHandler">
+         </class>
+         <enabledWhen>
+            <with
+                  variable="de.prob.core.model_loaded">
+               <equals
+                     value="enabled">
+               </equals>
+            </with>
+         </enabledWhen>
+      </handler>
 <!--      <handler
             commandId="de.prob.ui.startdmc">
          <class
@@ -1089,6 +1108,13 @@
                   mnemonic="R"
                   style="push">
             </command>
+            <command
+                  commandId="de.prob.ui.assertions_check"
+                  icon="icons/CBCInvariantCheck.png"
+                  label="Context Theorems"
+                  mnemonic="C"
+                  style="push">
+            </command>
          </menu>
       </menuContribution>
       <!--

de.prob.ui/src/de/prob/ui/assertion/AssertionCheckFinishedListener.java

+/**
+ * 
+ */
+package de.prob.ui.assertion;
+
+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.ConstraintBasedAssertionCheckCommand;
+import de.prob.core.command.ConstraintBasedAssertionCheckCommand.ResultType;
+import de.prob.core.command.IComposableCommand;
+import de.prob.logging.Logger;
+import de.prob.prolog.term.ListPrologTerm;
+
+/**
+ * This JobChangeAdapter presents the user the results of a deadlock freedom
+ * check.
+ * 
+ * @see AssertionCheckHandler
+ * 
+ * @author plagge
+ */
+public class AssertionCheckFinishedListener extends ProBJobFinishedListener {
+	private final Shell shell;
+
+	public AssertionCheckFinishedListener(final Shell shell) {
+		this.shell = shell;
+	}
+
+	@Override
+	protected void showResult(final IComposableCommand cmd,
+			final Animator animator) {
+		final ConstraintBasedAssertionCheckCommand command = (ConstraintBasedAssertionCheckCommand) cmd;
+		final ResultType result = command.getResult();
+		final int dialogType;
+		final String dialogTitle;
+		final String message;
+
+		if (result == null) {
+			dialogType = MessageDialog.ERROR;
+			dialogTitle = "Errow During Constraint Based Check";
+			message = "ProB did not return a result";
+		} else {
+			switch (result) {
+			case NO_COUNTER_EXAMPLE:
+				dialogType = MessageDialog.INFORMATION;
+				dialogTitle = "No Counter-Example Found";
+				message = "No Counter-Example to the Context Theorems was found.";
+				break;
+			case COUNTER_EXAMPLE:
+				dialogType = MessageDialog.WARNING;
+				dialogTitle = "COUNTER-EXAMPLE FOUND!";
+				message = "The model contains a Counter-Example state, it will be shown in the state view.";
+				displayCounterExample(command, animator);
+				break;
+			case TIMEOUT:
+				dialogType = MessageDialog.WARNING;
+				dialogTitle = " Interrupt";
+				message = "The deadlock check has been interrupted by the user or a time-out.";
+				break;
+			default:
+				Logger.notifyUser("Unexpected result: " + result);
+				return;
+			}
+		}
+		if (shell.isDisposed()) {
+			System.out.println("Deadlock freedom 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);
+		}
+	}
+
+	private void displayCounterExample(
+			final ConstraintBasedAssertionCheckCommand command,
+			final Animator animator) {
+		final ListPrologTerm errorState = command.getCounterExampleState();
+		// try {
+		// animator.getHistory().reset();
+
+		// ExecuteOperationCommand.executeOperation(animator, operation);
+		// } catch (ProBException e) {
+		// e.notifyUserOnce();
+		// }
+	}
+}

de.prob.ui/src/de/prob/ui/assertion/AssertionCheckHandler.java

+/**
+ * 
+ */
+package de.prob.ui.assertion;
+
+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.swt.widgets.Shell;
+import org.eclipse.ui.handlers.HandlerUtil;
+
+import de.prob.core.Animator;
+import de.prob.core.LanguageDependendAnimationPart;
+import de.prob.core.ProBCommandJob;
+import de.prob.core.command.ConstraintBasedAssertionCheckCommand;
+import de.prob.logging.Logger;
+
+/**
+ * This handler provides a simple dialog to ask for an optional predicate to
+ * check for deadlocks in the model.
+ * 
+ * @author plagge
+ */
+public class AssertionCheckHandler extends AbstractHandler {
+	@Override
+	public Object execute(final ExecutionEvent event) throws ExecutionException {
+		final Shell shell = HandlerUtil.getActiveShell(event);
+		if (Animator.getAnimator().isMachineLoaded()) {
+			performAssertionCheck(shell);
+		} else {
+			Logger.notifyUser("No ProB animation running. This is a bug. Please submit a report. Error in declaraion for class DeadlockCheckHandler");
+		}
+		return null;
+	}
+
+	private void performAssertionCheck(final Shell shell)
+			throws ExecutionException {
+		final Animator animator = Animator.getAnimator();
+		final LanguageDependendAnimationPart ldp = animator
+				.getLanguageDependendPart();
+		startCheck(animator, ldp, shell);
+
+	}
+
+	private void startCheck(final Animator animator,
+			final LanguageDependendAnimationPart ldp, final Shell shell)
+			throws ExecutionException {
+		final ConstraintBasedAssertionCheckCommand command = new ConstraintBasedAssertionCheckCommand();
+		final Job job = new ProBCommandJob(
+				"Checking Context Theorems / Assertions", animator, command);
+		job.setUser(true);
+		job.addJobChangeListener(new AssertionCheckFinishedListener(shell));
+		job.schedule();
+	}
+}