diff --git a/de.prob.ui/plugin.xml b/de.prob.ui/plugin.xml index bf2abf7483b4dcae8b647183045d4ca00b311778..8c118aecea1ff3887edaf7ec724db0178325ae0f 100644 --- a/de.prob.ui/plugin.xml +++ b/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" diff --git a/de.prob.ui/src/de/prob/ui/assertion/AssertionDynCheckFinishedListener.java b/de.prob.ui/src/de/prob/ui/assertion/AssertionDynCheckFinishedListener.java new file mode 100644 index 0000000000000000000000000000000000000000..9796d1fe9da9cff702374ce2aaed462ae58f58a2 --- /dev/null +++ b/de.prob.ui/src/de/prob/ui/assertion/AssertionDynCheckFinishedListener.java @@ -0,0 +1,104 @@ +/** + * + */ +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(); + } + } +} diff --git a/de.prob.ui/src/de/prob/ui/assertion/AssertionDynCheckHandler.java b/de.prob.ui/src/de/prob/ui/assertion/AssertionDynCheckHandler.java new file mode 100644 index 0000000000000000000000000000000000000000..4ba3f822ca8204ae181e179fa7f4579161e28424 --- /dev/null +++ b/de.prob.ui/src/de/prob/ui/assertion/AssertionDynCheckHandler.java @@ -0,0 +1,56 @@ +/** + * + */ +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(); + } +}