“find valid state” ported to rodin

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

+/**
+ * 
+ */
+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;
+	}
+}

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>
       <!--

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;
-		}
-	}
 }

de.prob.ui/src/de/prob/ui/findvalidstate/FindValidStateFinishedListener.java

+/**
+ * 
+ */
+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();
+		}
+	}
+}

de.prob.ui/src/de/prob/ui/findvalidstate/FindValidStateHandler.java

+/**
+ * 
+ */
+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;
+	}
+
+}

de.prob.ui/src/de/prob/ui/validators/PredicateValidator.java

+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