Skip to content
Snippets Groups Projects
Commit 680f739d authored by dgelessus's avatar dgelessus
Browse files

Add :find command (closes #20)

parent 3f62e185
No related branches found
No related tags found
No related merge requests found
......@@ -29,6 +29,7 @@ import de.prob2.jupyter.commands.ConstantsCommand;
import de.prob2.jupyter.commands.DotCommand;
import de.prob2.jupyter.commands.EvalCommand;
import de.prob2.jupyter.commands.ExecCommand;
import de.prob2.jupyter.commands.FindCommand;
import de.prob2.jupyter.commands.GotoCommand;
import de.prob2.jupyter.commands.GroovyCommand;
import de.prob2.jupyter.commands.HelpCommand;
......@@ -158,6 +159,7 @@ public final class ProBKernel extends BaseKernel {
this.commands.put(":constants", injector.getInstance(ConstantsCommand.class));
this.commands.put(":init", injector.getInstance(InitialiseCommand.class));
this.commands.put(":goto", injector.getInstance(GotoCommand.class));
this.commands.put(":find", injector.getInstance(FindCommand.class));
this.commands.put(":show", injector.getInstance(ShowCommand.class));
this.commands.put(":dot", injector.getInstance(DotCommand.class));
this.commands.put(":assert", injector.getInstance(AssertCommand.class));
......
package de.prob2.jupyter.commands;
import com.google.inject.Inject;
import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.animator.domainobjects.IEvalElement;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
import io.github.spencerpark.jupyter.kernel.display.DisplayData;
import org.jetbrains.annotations.NotNull;
public final class FindCommand implements Command {
private final @NotNull AnimationSelector animationSelector;
@Inject
private FindCommand(final @NotNull AnimationSelector animationSelector) {
super();
this.animationSelector = animationSelector;
}
@Override
public @NotNull String getSyntax() {
return ":find PREDICATE";
}
@Override
public @NotNull String getShortHelp() {
return "Try to find a state for which the given predicate is true (in addition to the machine's invariant).";
}
@Override
public @NotNull String getHelpBody() {
return "If such a state is found, it is made the current state, otherwise an error is displayed.\n\nNote that this command does not necessarily find a valid *trace* to the found state. Instead, in some cases a single \"fake\" transition is added to the trace, which goes directly to the found state and does not use the machine's operations to reach it.";
}
@Override
public @NotNull DisplayData run(final @NotNull String argString) {
final Trace trace = this.animationSelector.getCurrentTrace();
final IEvalElement pred = trace.getModel().parseFormula(argString, FormulaExpand.EXPAND);
final Trace newTrace = trace.getStateSpace().getTraceToState(pred);
this.animationSelector.changeCurrentAnimation(newTrace);
return new DisplayData("Found state: " + newTrace.getCurrentState().getId());
}
@Override
public @NotNull ReplacementOptions complete(final @NotNull String argString, final int at) {
return CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment