add dynamic invariant theorems checking command

de.prob.ui/plugin.xml

@@ -315,7 +315,12 @@
       <command
             categoryId="de.prob.ui.commands.category"
             id="de.prob.ui.assertion_check"
-            name="Check Assertions">
+            name="Check Context Theorems">
+      </command>
+      <command
+            categoryId="de.prob.ui.commands.category"
+            id="de.prob.ui.assertion_dyn_check"
+            name="Check Invariant Theorems">
       </command>
       <command
             categoryId="de.prob.ui.commands.category"
@@ -364,11 +369,6 @@
             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>
       <command
             categoryId="de.prob.ui.commands.category"
             id="de.prob.ui.find_valid_state"
@@ -802,6 +802,28 @@
                class="de.prob.ui.assertion.AssertionCheckHandler">
          </class>
       </handler>
+      <handler
+            commandId="de.prob.ui.assertion_dyn_check">
+         <enabledWhen>
+            <or>
+               <with
+                     variable="de.prob.core.model_loaded">
+                  <equals
+                        value="enabled">
+                  </equals>
+               </with>
+               <with
+                     variable="de.prob.core.context_loaded">
+                  <equals
+                        value="enabled">
+                  </equals>
+               </with>
+            </or>
+         </enabledWhen>
+         <class
+               class="de.prob.ui.assertion.AssertionDynCheckHandler">
+         </class>
+      </handler>
       <handler
             commandId="de.prob.ui.find_valid_state">
          <class
@@ -1163,6 +1185,13 @@
                   mnemonic="C"
                   style="push">
             </command>
+            <command
+                  commandId="de.prob.ui.assertion_dyn_check"
+                  icon="icons/CBCInvariantCheck.png"
+                  label="Invariant Theorems"
+                  mnemonic="T"
+                  style="push">
+            </command>
             <command
                   commandId="de.prob.ui.find_valid_state"
                   icon="icons/CBCInvariantCheck.png"

de.prob.ui/src/de/prob/ui/assertion/AssertionDynCheckFinishedListener.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.ExecuteOperationCommand;
+import de.prob.core.command.IComposableCommand;
+import de.prob.core.domainobjects.Operation;
+import de.prob.exceptions.ProBException;
+import de.prob.logging.Logger;
+
+/**
+ * This JobChangeAdapter presents the user the results of a assertion
+ * check.
+ * 
+ * @see AssertionCheckHandler
+ * 
+ * @author plagge
+ */
+public class AssertionDynCheckFinishedListener extends ProBJobFinishedListener {
+	private final Shell shell;
+
+	public AssertionDynCheckFinishedListener(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_EXISTS:
+				dialogType = MessageDialog.INFORMATION;
+				dialogTitle = "No Counter-Example Exists";
+				message = "No Counter-Example to the Invariant Theorems exists.";
+				break;
+			case NO_COUNTER_EXAMPLE_FOUND:
+				dialogType = MessageDialog.INFORMATION;
+				dialogTitle = "No Counter-Example Found";
+				message = "No Counter-Example to the Invariant Theorems was found.";
+				break;
+			case COUNTER_EXAMPLE:
+				dialogType = MessageDialog.WARNING;
+				dialogTitle = "COUNTER-EXAMPLE FOUND!";
+				message = "The model contains a Counter-Example state to the Invariant Theorems, it will be shown in the state view.";
+				displayCounterExample(command, animator);
+				break;
+			case INTERRUPTED:
+				dialogType = MessageDialog.WARNING;
+				dialogTitle = " Interrupt";
+				message = "The assertion 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("Invariant Theorems 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 Operation operation = command.getCounterExampleOperation();
+		try {
+			// we do not reset the history because we want to keep the root
+			// state, we just start a new path from root
+			animator.getHistory().gotoPos(0);
+			ExecuteOperationCommand.executeOperation(animator, operation);
+		} catch (ProBException e) {
+			e.notifyUserOnce();
+		}
+	}
+}

de.prob.ui/src/de/prob/ui/assertion/AssertionDynCheckHandler.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.core.command.ConstraintBasedDynamicAssertionCheckCommand;
+import de.prob.logging.Logger;
+
+/**
+ * This handler provides a way to start the *dynamic* assertion checking command
+ * 
+ * @author plagge
+ */
+public class AssertionDynCheckHandler 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 ConstraintBasedDynamicAssertionCheckCommand command = new ConstraintBasedDynamicAssertionCheckCommand();
+		final Job job = new ProBCommandJob(
+				"Checking Machine Theorems from Invariants Clause", animator, command);
+		job.setUser(true);
+		job.addJobChangeListener(new AssertionDynCheckFinishedListener(shell));
+		job.schedule();
+	}
+}