diff --git a/de.prob.core/src/de/prob/core/command/ConstraintBasedAssertionCheckCommand.java b/de.prob.core/src/de/prob/core/command/ConstraintBasedAssertionCheckCommand.java new file mode 100644 index 0000000000000000000000000000000000000000..802e83ad1674560e06e6b82aedde25fb6edaa2e4 --- /dev/null +++ b/de.prob.core/src/de/prob/core/command/ConstraintBasedAssertionCheckCommand.java @@ -0,0 +1,66 @@ +/** + * + */ +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; + + } +} diff --git a/de.prob.ui/plugin.xml b/de.prob.ui/plugin.xml index 308df3ea239606d90c3de7b9b543e9d4cac78683..d1ea1c26180b629f443957af830425eb0ca16efd 100644 --- a/de.prob.ui/plugin.xml +++ b/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> <!-- diff --git a/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckFinishedListener.java b/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckFinishedListener.java new file mode 100644 index 0000000000000000000000000000000000000000..03ae30457c6a0b2e6f38b2cfeaa8acd04e95f6fe --- /dev/null +++ b/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckFinishedListener.java @@ -0,0 +1,96 @@ +/** + * + */ +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(); + // } + } +} diff --git a/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckHandler.java b/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckHandler.java new file mode 100644 index 0000000000000000000000000000000000000000..e311721be347f77ab7d10108c2e6cd4fbe31b545 --- /dev/null +++ b/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckHandler.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.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(); + } +}