diff --git a/de.prob.core/src/de/prob/core/command/FindValidStateCommand.java b/de.prob.core/src/de/prob/core/command/FindValidStateCommand.java
new file mode 100644
index 0000000000000000000000000000000000000000..7fa2cff9b343f4c62ff79bfd60f0d001a27e68b4
--- /dev/null
+++ b/de.prob.core/src/de/prob/core/command/FindValidStateCommand.java
@@ -0,0 +1,88 @@
+/**
+ *
+ */
+package de.prob.core.command;
+
+import de.prob.core.LanguageDependendAnimationPart;
+import de.prob.core.domainobjects.Operation;
+import de.prob.parser.ISimplifiedROMap;
+import de.prob.prolog.output.IPrologTermOutput;
+import de.prob.prolog.term.CompoundPrologTerm;
+import de.prob.prolog.term.PrologTerm;
+
+public class FindValidStateCommand implements IComposableCommand {
+
+ public static enum ResultType {
+ STATE_FOUND, NO_STATE_FOUND, INTERRUPTED, ERROR
+ };
+
+ private static final String COMMAND_NAME = "find_state_satisfying_predicate";
+ private static final String RESULT_VARIABLE = "R";
+
+ private final PrologTerm predicate;
+
+ private ResultType result;
+ private String stateId;
+ private Operation operation;
+
+ /**
+ * @param predicate
+ * is a parsed predicate or <code>null</code>
+ * @see LanguageDependendAnimationPart#parsePredicate(IPrologTermOutput,
+ * String, boolean)
+ */
+ public FindValidStateCommand(final PrologTerm predicate) {
+ this.predicate = predicate;
+ }
+
+ public PrologTerm getPredicate() {
+ return predicate;
+ }
+
+ public ResultType getResult() {
+ return result;
+ }
+
+ public String getStateId() {
+ return stateId;
+ }
+
+ public Operation getOperation() {
+ return operation;
+ }
+
+ @Override
+ public void writeCommand(final IPrologTermOutput pto) {
+ pto.openTerm(COMMAND_NAME);
+ if (predicate != null) {
+ predicate.toTermOutput(pto);
+ }
+ 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("no_valid_state_found", 0)) {
+ result = ResultType.NO_STATE_FOUND;
+ } else if (resultTerm.hasFunctor("errors", 1)) {
+ result = ResultType.ERROR;
+ } else if (resultTerm.hasFunctor("interrupted", 0)) {
+ result = ResultType.INTERRUPTED;
+ } else if (resultTerm.hasFunctor("state_found", 2)) {
+ CompoundPrologTerm term = (CompoundPrologTerm) resultTerm;
+ result = ResultType.STATE_FOUND;
+ operation = Operation.fromPrologTerm(term.getArgument(1));
+ stateId = term.getArgument(2).toString();
+ } 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 847cb80e140890db88aa9da3cf28b58a41c30b16..6bf2e1f287fe32c93a44f4924fcb7d4f3c4a6dfc 100644
--- a/de.prob.ui/plugin.xml
+++ b/de.prob.ui/plugin.xml
@@ -369,6 +369,11 @@
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"
+ name="Find State satisfying Predicate">
+ </command>
</extension>
<extension
point="org.eclipse.ui.handlers">
@@ -809,6 +814,20 @@
class="de.prob.ui.assertion.AssertionCheckHandler">
</class>
</handler>
+ <handler
+ commandId="de.prob.ui.find_valid_state">
+ <class
+ class="de.prob.ui.findvalidstate.FindValidStateHandler">
+ </class>
+ <enabledWhen>
+ <with
+ variable="de.prob.core.model_loaded">
+ <equals
+ value="enabled">
+ </equals>
+ </with>
+ </enabledWhen>
+ </handler>
<!-- <handler
commandId="de.prob.ui.startdmc">
<class
@@ -1188,6 +1207,13 @@
mnemonic="C"
style="push">
</command>
+ <command
+ commandId="de.prob.ui.find_valid_state"
+ icon="icons/CBCInvariantCheck.png"
+ label="Find State satisfying Predicate"
+ mnemonic="f"
+ style="push">
+ </command>
</menu>
</menuContribution>
<!--
diff --git a/de.prob.ui/src/de/prob/ui/deadlock/DeadlockCheckHandler.java b/de.prob.ui/src/de/prob/ui/deadlock/DeadlockCheckHandler.java
index 7a7dc427d17b0bb06333835cf760e085781d1316..293ce887871be5519d73a2764cb69efafdc763a2 100644
--- a/de.prob.ui/src/de/prob/ui/deadlock/DeadlockCheckHandler.java
+++ b/de.prob.ui/src/de/prob/ui/deadlock/DeadlockCheckHandler.java
@@ -17,9 +17,9 @@ import de.prob.core.LanguageDependendAnimationPart;
import de.prob.core.ProBCommandJob;
import de.prob.core.command.ConstraintBasedDeadlockCheckCommand;
import de.prob.logging.Logger;
-import de.prob.parserbase.ProBParseException;
import de.prob.parserbase.ProBParserBaseAdapter;
import de.prob.prolog.term.PrologTerm;
+import de.prob.ui.validators.PredicateValidator;
/**
* This handler provides a simple dialog to ask for an optional predicate to
@@ -86,30 +86,4 @@ public class DeadlockCheckHandler extends AbstractHandler {
}
return predicate;
}
-
- private static final class PredicateValidator implements IInputValidator {
- final LanguageDependendAnimationPart ldp;
-
- public PredicateValidator(final LanguageDependendAnimationPart ldp) {
- this.ldp = ldp;
- }
-
- @Override
- public String isValid(final String newText) {
- if (newText.trim().isEmpty())
- return null;
- if (ldp == null)
- return "Cannot parse predicates for the current formalism";
- try {
- final ProBParserBaseAdapter parser = new ProBParserBaseAdapter(
- ldp);
- parser.parsePredicate(newText, false);
- } catch (UnsupportedOperationException e) {
- return "The parser for this formalism cannot parse predicates";
- } catch (ProBParseException e) {
- return e.getLocalizedMessage();
- }
- return null;
- }
- }
}
diff --git a/de.prob.ui/src/de/prob/ui/findvalidstate/FindValidStateFinishedListener.java b/de.prob.ui/src/de/prob/ui/findvalidstate/FindValidStateFinishedListener.java
new file mode 100644
index 0000000000000000000000000000000000000000..bc3d75a4c906554d0b5c1cbceef60ad1853c3c35
--- /dev/null
+++ b/de.prob.ui/src/de/prob/ui/findvalidstate/FindValidStateFinishedListener.java
@@ -0,0 +1,94 @@
+/**
+ *
+ */
+package de.prob.ui.findvalidstate;
+
+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.ExecuteOperationCommand;
+import de.prob.core.command.FindValidStateCommand;
+import de.prob.core.command.FindValidStateCommand.ResultType;
+import de.prob.core.command.IComposableCommand;
+import de.prob.core.domainobjects.Operation;
+import de.prob.exceptions.ProBException;
+import de.prob.logging.Logger;
+
+public class FindValidStateFinishedListener extends ProBJobFinishedListener {
+ private final Shell shell;
+
+ public FindValidStateFinishedListener(final Shell shell) {
+ this.shell = shell;
+ }
+
+ @Override
+ protected void showResult(final IComposableCommand cmd,
+ final Animator animator) {
+ final FindValidStateCommand command = (FindValidStateCommand) cmd;
+ final ResultType result = command.getResult();
+ final int dialogType;
+ final String dialogTitle;
+ final String message;
+ if (result == null) {
+ dialogType = MessageDialog.ERROR;
+ dialogTitle = "Errow During Deadlock Freedom Check";
+ message = "ProB did not return a result";
+ } else {
+ switch (result) {
+ case NO_STATE_FOUND:
+ dialogType = MessageDialog.WARNING;
+ dialogTitle = "No State Found";
+ message = "No State satisfying both the Invariant and the Predicate was found.";
+ break;
+ case ERROR:
+ dialogType = MessageDialog.ERROR;
+ dialogTitle = "Errow During Search for Valid State";
+ message = "An unexpected error occurred while typechecking the given predicate.";
+ break;
+ case STATE_FOUND:
+ dialogType = MessageDialog.INFORMATION;
+ dialogTitle = "State found";
+ message = "The model contains a state satisfying the given predicate and the invariant, it will be shown in the state view.";
+ displayState(command, animator);
+ break;
+ case INTERRUPTED:
+ dialogType = MessageDialog.WARNING;
+ dialogTitle = "User Interrupt";
+ message = "The search 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 displayState(final FindValidStateCommand cmd,
+ final Animator animator) {
+ final Operation operation = cmd.getOperation();
+ 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/findvalidstate/FindValidStateHandler.java b/de.prob.ui/src/de/prob/ui/findvalidstate/FindValidStateHandler.java
new file mode 100644
index 0000000000000000000000000000000000000000..9de29c8f68fe1ecf9389c2c5ef37a29a778e584c
--- /dev/null
+++ b/de.prob.ui/src/de/prob/ui/findvalidstate/FindValidStateHandler.java
@@ -0,0 +1,89 @@
+/**
+ *
+ */
+package de.prob.ui.findvalidstate;
+
+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.IInputValidator;
+import org.eclipse.jface.dialogs.InputDialog;
+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.FindValidStateCommand;
+import de.prob.logging.Logger;
+import de.prob.parserbase.ProBParserBaseAdapter;
+import de.prob.prolog.term.PrologTerm;
+import de.prob.ui.validators.PredicateValidator;
+
+/**
+ * This handler provides a simple dialog to ask for an optional predicate to
+ * check for deadlocks in the model.
+ *
+ * @author krings
+ */
+public class FindValidStateHandler extends AbstractHandler {
+ @Override
+ public Object execute(final ExecutionEvent event) throws ExecutionException {
+ final Shell shell = HandlerUtil.getActiveShell(event);
+ if (Animator.getAnimator().isMachineLoaded()) {
+ findValidState(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 findValidState(final Shell shell) throws ExecutionException {
+ final Animator animator = Animator.getAnimator();
+ final LanguageDependendAnimationPart ldp = animator
+ .getLanguageDependendPart();
+ final IInputValidator validator = new PredicateValidator(ldp);
+ final InputDialog dialog = new InputDialog(
+ shell,
+ "Find Valid State Freedom Check",
+ "ProB will try to find a state satisfying the invariant and the predicate:",
+ "1=1", validator);
+ final int status = dialog.open();
+ if (status == InputDialog.OK) {
+ startFindState(animator, ldp, dialog.getValue(), shell);
+ }
+ }
+
+ private void startFindState(final Animator animator,
+ final LanguageDependendAnimationPart ldp, final String value,
+ final Shell shell) throws ExecutionException {
+ final PrologTerm predicate = parsePredicate(ldp, value);
+ final FindValidStateCommand command = new FindValidStateCommand(
+ predicate);
+ final Job job = new ProBCommandJob(
+ "Searching for State satisfying Predicate", animator, command);
+ job.setUser(true);
+ job.addJobChangeListener(new FindValidStateFinishedListener(shell));
+ job.schedule();
+ }
+
+ private PrologTerm parsePredicate(final LanguageDependendAnimationPart ldp,
+ final String input) throws ExecutionException {
+ final PrologTerm predicate;
+ if (input != null && input.trim().isEmpty()) {
+ predicate = null;
+ } else {
+ try {
+ final ProBParserBaseAdapter parser = new ProBParserBaseAdapter(
+ ldp);
+ predicate = parser.parsePredicate(input, false);
+ } catch (Exception e) {
+ throw (new ExecutionException(
+ "Exception while parsing the input", e));
+ }
+ }
+ return predicate;
+ }
+
+}
diff --git a/de.prob.ui/src/de/prob/ui/validators/PredicateValidator.java b/de.prob.ui/src/de/prob/ui/validators/PredicateValidator.java
new file mode 100644
index 0000000000000000000000000000000000000000..567cd042720803818550ad3745cbacd13ec241a3
--- /dev/null
+++ b/de.prob.ui/src/de/prob/ui/validators/PredicateValidator.java
@@ -0,0 +1,32 @@
+package de.prob.ui.validators;
+
+import org.eclipse.jface.dialogs.IInputValidator;
+
+import de.prob.core.LanguageDependendAnimationPart;
+import de.prob.parserbase.ProBParseException;
+import de.prob.parserbase.ProBParserBaseAdapter;
+
+public final class PredicateValidator implements IInputValidator {
+ final LanguageDependendAnimationPart ldp;
+
+ public PredicateValidator(final LanguageDependendAnimationPart ldp) {
+ this.ldp = ldp;
+ }
+
+ @Override
+ public String isValid(final String newText) {
+ if (newText.trim().isEmpty())
+ return null;
+ if (ldp == null)
+ return "Cannot parse predicates for the current formalism";
+ try {
+ final ProBParserBaseAdapter parser = new ProBParserBaseAdapter(ldp);
+ parser.parsePredicate(newText, false);
+ } catch (UnsupportedOperationException e) {
+ return "The parser for this formalism cannot parse predicates";
+ } catch (ProBParseException e) {
+ return e.getLocalizedMessage();
+ }
+ return null;
+ }
+}
\ No newline at end of file