diff --git a/notebooks/tests/animate.ipynb b/notebooks/tests/animate.ipynb index 80c4c8967ad77841e77743c62d4a6e00c6334285..c2f7f87119fb3d96db2e95f7387f2d2d3c92323b 100644 --- a/notebooks/tests/animate.ipynb +++ b/notebooks/tests/animate.ipynb @@ -275,11 +275,20 @@ "metadata": {}, "outputs": [ { - "ename": "CommandExecutionException", - "evalue": ":constants: Could not setup constants with the specified predicate", + "ename": "IllegalArgumentException", + "evalue": "Executing operation $setup_constants with predicate min_value=5 & max_value=-5 produced errors: Could not execute operation SETUP_CONSTANTS with additional predicate", "output_type": "error", "traceback": [ - "\u001b[1m\u001b[31m:constants: Could not setup constants with the specified predicate\u001b[0m" + "\u001b[1m\u001b[31m---------------------------------------------------------------------------\u001b[0m", + "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $setup_constants with predicate min_value=5 & max_value=-5 produced errors: Could not execute operation SETUP_CONSTANTS with additional predicate\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:279)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.ConstantsCommand.run(ConstantsCommand.java:47)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:222)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:245)\u001b[0m", + "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:303)\u001b[0m", + "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$16(ShellChannel.java:54)\u001b[0m", + "\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m", + "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:44)\u001b[0m" ] } ], @@ -388,7 +397,8 @@ "output_type": "error", "traceback": [ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProB reported Errors\u001b[0m", - "\u001b[1m\u001b[31mError: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:6:15 to 6:44)\u001b[0m" + "\u001b[1m\u001b[31mError: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:6:15 to 6:44)\u001b[0m", + "\u001b[1m\u001b[31mError start line 6 out of bounds (1..1)\u001b[0m" ] } ], @@ -617,11 +627,20 @@ "metadata": {}, "outputs": [ { - "ename": "CommandExecutionException", - "evalue": ":constants: Machine constants are already set up", + "ename": "IllegalArgumentException", + "evalue": "Executing operation $setup_constants with predicate 1=1 produced errors: Machine is already initialised, cannot execute SETUP_CONSTANTS", "output_type": "error", "traceback": [ - "\u001b[1m\u001b[31m:constants: Machine constants are already set up\u001b[0m" + "\u001b[1m\u001b[31m---------------------------------------------------------------------------\u001b[0m", + "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $setup_constants with predicate 1=1 produced errors: Machine is already initialised, cannot execute SETUP_CONSTANTS\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:279)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.ConstantsCommand.run(ConstantsCommand.java:47)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:222)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:245)\u001b[0m", + "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:303)\u001b[0m", + "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$16(ShellChannel.java:54)\u001b[0m", + "\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m", + "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:44)\u001b[0m" ] } ], @@ -635,11 +654,20 @@ "metadata": {}, "outputs": [ { - "ename": "CommandExecutionException", - "evalue": ":init: Machine is already initialised", + "ename": "IllegalArgumentException", + "evalue": "Executing operation $initialise_machine with predicate 1=1 produced errors: Machine is already initialised, cannot execute INITIALISATION", "output_type": "error", "traceback": [ - "\u001b[1m\u001b[31m:init: Machine is already initialised\u001b[0m" + "\u001b[1m\u001b[31m---------------------------------------------------------------------------\u001b[0m", + "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $initialise_machine with predicate 1=1 produced errors: Machine is already initialised, cannot execute INITIALISATION\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:279)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.InitialiseCommand.run(InitialiseCommand.java:47)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:222)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:245)\u001b[0m", + "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:303)\u001b[0m", + "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$16(ShellChannel.java:54)\u001b[0m", + "\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m", + "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:44)\u001b[0m" ] } ], @@ -653,11 +681,20 @@ "metadata": {}, "outputs": [ { - "ename": "CommandExecutionException", - "evalue": ":exec: Could not execute operation nope", + "ename": "IllegalArgumentException", + "evalue": "Executing operation nope with predicate 1=1 produced errors: Unknown Operation nope", "output_type": "error", "traceback": [ - "\u001b[1m\u001b[31m:exec: Could not execute operation nope\u001b[0m" + "\u001b[1m\u001b[31m---------------------------------------------------------------------------\u001b[0m", + "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation nope with predicate 1=1 produced errors: Unknown Operation nope\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:279)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.ExecCommand.run(ExecCommand.java:70)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:222)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:245)\u001b[0m", + "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:303)\u001b[0m", + "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$16(ShellChannel.java:54)\u001b[0m", + "\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m", + "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:44)\u001b[0m" ] } ], @@ -671,11 +708,20 @@ "metadata": {}, "outputs": [ { - "ename": "CommandExecutionException", - "evalue": ":exec: Could not execute operation add with the given predicate", + "ename": "IllegalArgumentException", + "evalue": "Executing operation add with predicate 1=0 produced errors: Could not execute operation add with additional predicate", "output_type": "error", "traceback": [ - "\u001b[1m\u001b[31m:exec: Could not execute operation add with the given predicate\u001b[0m" + "\u001b[1m\u001b[31m---------------------------------------------------------------------------\u001b[0m", + "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation add with predicate 1=0 produced errors: Could not execute operation add with additional predicate\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:279)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.ExecCommand.run(ExecCommand.java:70)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:222)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:245)\u001b[0m", + "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:303)\u001b[0m", + "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$16(ShellChannel.java:54)\u001b[0m", + "\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m", + "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:44)\u001b[0m" ] } ], @@ -714,11 +760,20 @@ "metadata": {}, "outputs": [ { - "ename": "CommandExecutionException", - "evalue": ":constants: Machine has no constants, use :init instead", + "ename": "IllegalArgumentException", + "evalue": "Executing operation $setup_constants with predicate 1=1 produced errors: Could not execute operation SETUP_CONSTANTS", "output_type": "error", "traceback": [ - "\u001b[1m\u001b[31m:constants: Machine has no constants, use :init instead\u001b[0m" + "\u001b[1m\u001b[31m---------------------------------------------------------------------------\u001b[0m", + "\u001b[1m\u001b[31mjava.lang.IllegalArgumentException: Executing operation $setup_constants with predicate 1=1 produced errors: Could not execute operation SETUP_CONSTANTS\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob.statespace.StateSpace.transitionFromPredicate(StateSpace.java:279)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.ConstantsCommand.run(ConstantsCommand.java:47)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeCommand(ProBKernel.java:222)\u001b[0m", + "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:245)\u001b[0m", + "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:303)\u001b[0m", + "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$16(ShellChannel.java:54)\u001b[0m", + "\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m", + "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:44)\u001b[0m" ] } ], @@ -737,7 +792,8 @@ "output_type": "error", "traceback": [ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProB reported Errors\u001b[0m", - "\u001b[1m\u001b[31mError: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:4:15 to 4:26)\u001b[0m" + "\u001b[1m\u001b[31mError: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:4:15 to 4:26)\u001b[0m", + "\u001b[1m\u001b[31mError start line 4 out of bounds (1..1)\u001b[0m" ] } ], diff --git a/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java b/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java index 1b0a6c948425ebc6325d68805abb8ba91c6e9395..8dbbacca5ed7c2988114b122c32f478b1eeee8ea 100644 --- a/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java @@ -10,8 +10,6 @@ import de.prob.statespace.AnimationSelector; import de.prob.statespace.Trace; import de.prob.statespace.Transition; -import de.prob2.jupyter.UserErrorException; - import io.github.spencerpark.jupyter.kernel.ReplacementOptions; import io.github.spencerpark.jupyter.kernel.display.DisplayData; @@ -45,17 +43,10 @@ public final class ConstantsCommand implements Command { @Override public @NotNull DisplayData run(final @NotNull String argString) { final Trace trace = this.animationSelector.getCurrentTrace(); - final List<String> predicates = argString.isEmpty() ? Collections.emptyList() : Collections.singletonList(argString); - final Transition op = trace.getCurrentState().findTransition("$setup_constants", predicates); - if (op == null) { - if (trace.gotoPosition(-1).canExecuteEvent("$initialise_machine")) { - throw new UserErrorException("Machine has no constants, use :init instead"); - } else if (trace.getCurrent().getIndex() > -1) { - throw new UserErrorException("Machine constants are already set up"); - } else { - throw new UserErrorException("Could not setup constants" + (argString.isEmpty() ? "" : " with the specified predicate")); - } - } + final String predicate = argString.isEmpty() ? "1=1" : argString; + final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), "$setup_constants", predicate, 1); + assert !ops.isEmpty(); + final Transition op = ops.get(0); this.animationSelector.changeCurrentAnimation(trace.add(op)); trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE); return new DisplayData(String.format("Machine constants set up using operation %s: %s", op.getId(), op.getRep())); diff --git a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java index 66a19399484522beec5e8611d030d434d2b16f07..75453e702fac5ba0b3f1be75570646a504576fc3 100644 --- a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java @@ -66,11 +66,10 @@ public final class ExecCommand implements Command { } else { // Transition not found, assume that the argument is an operation name instead. final String translatedOpName = CommandUtils.unprettyOperationName(opNameOrId); - final List<String> predicates = split.size() < 2 ? Collections.emptyList() : Collections.singletonList(split.get(1)); - op = trace.getCurrentState().findTransition(translatedOpName, predicates); - if (op == null) { - throw new UserErrorException("Could not execute operation " + opNameOrId + (split.size() < 2 ? "" : " with the given predicate")); - } + final String predicate = split.size() < 2 ? "1=1" : split.get(1); + final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), translatedOpName, predicate, 1); + assert !ops.isEmpty(); + op = ops.get(0); } this.animationSelector.changeCurrentAnimation(trace.add(op)); diff --git a/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java b/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java index e26e3547f5c75ccc43f40dbca7dcd66080bad195..33c1f55694853de909e1dea442b830f99c2b0b2b 100644 --- a/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java @@ -10,8 +10,6 @@ import de.prob.statespace.AnimationSelector; import de.prob.statespace.Trace; import de.prob.statespace.Transition; -import de.prob2.jupyter.UserErrorException; - import io.github.spencerpark.jupyter.kernel.ReplacementOptions; import io.github.spencerpark.jupyter.kernel.display.DisplayData; @@ -45,17 +43,10 @@ public final class InitialiseCommand implements Command { @Override public @NotNull DisplayData run(final @NotNull String argString) { final Trace trace = this.animationSelector.getCurrentTrace(); - final List<String> predicates = argString.isEmpty() ? Collections.emptyList() : Collections.singletonList(argString); - final Transition op = trace.getCurrentState().findTransition("$initialise_machine", predicates); - if (op == null) { - if (trace.getCurrentState().isInitialised()) { - throw new UserErrorException("Machine is already initialised"); - } else if (trace.getHead().getPrevious() == null && trace.canExecuteEvent("$setup_constants")) { - throw new UserErrorException("Machine constants are not yet set up, use :constants first"); - } else { - throw new UserErrorException("Could not initialise machine" + (argString.isEmpty() ? "" : " with the specified predicate")); - } - } + final String predicate = argString.isEmpty() ? "1=1" : argString; + final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), "$initialise_machine", predicate, 1); + assert !ops.isEmpty(); + final Transition op = ops.get(0); this.animationSelector.changeCurrentAnimation(trace.add(op)); trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE); return new DisplayData(String.format("Machine initialised using operation %s: %s", op.getId(), op.getRep()));