Merge implementations of :constants, :init and :exec

24839b33 · dgelessus · 0c2896e4 · 24839b33 · 24839b33 · 24839b33
Commit 24839b33 authored 4 years ago by dgelessus
--- a/notebooks/tests/animate.ipynb
+++ b/notebooks/tests/animate.ipynb
@@ -281,7 +281,7 @@
    {
     "data": {
      "text/plain": [
-       "Machine constants set up using operation 2: $setup_constants()"
+       "Executed operation: $setup_constants()"
      ]
     },
     "execution_count": 11,
@@ -391,7 +391,7 @@
    {
     "data": {
      "text/plain": [
-       "Machine initialised using operation 7: $initialise_machine()"
+       "Executed operation: $initialise_machine()"
      ]
     },
     "execution_count": 16,
@@ -906,7 +906,7 @@
    {
     "data": {
      "text/plain": [
-       "Machine constants set up using operation 0: $setup_constants()"
+       "Executed operation: $setup_constants()"
      ]
     },
     "execution_count": 38,
@@ -949,7 +949,7 @@
    {
     "data": {
      "text/plain": [
-       "Machine initialised using operation 3: $initialise_machine()"
+       "Executed operation: $initialise_machine()"
      ]
     },
     "execution_count": 40,

 %% Cell type:code id: tags:
 ``` prob
 :help :browse
 ```
 %% Output
    ```
    :browse
    ```
    Show information about the current state.
    The output shows the names of all sets, constants, and variables defined by the current machine, as well as a list of enabled operations (and possible parameter values) in the current state.
    :browse
    Show information about the current state.
    The output shows the names of all sets, constants, and variables defined by the current machine, as well as a list of enabled operations (and possible parameter values) in the current state.
 %% Cell type:code id: tags:
 ``` prob
 :help :exec
 ```
 %% Output
    ```
    :exec OPERATION [PREDICATE]
    ```
    Execute an operation.
    The predicate is used to select the operation's parameter values. The parameters can be fully specified explicitly (e. g. `:exec op param1 = 123 & param2 = {1, 2}`), or they can be partially constrained (e. g. `:exec op param1 > 100 & card(param2) >= 2`) to let ProB find a valid combination of parameters. If there are multiple valid combinations of parameters that satisfy the predicate, it is undefined which one is selected by ProB.
    If no predicate is specified, the parameters are not constrained, and ProB will select an arbitrary valid combination of parameters.
    :exec OPERATION [PREDICATE]
    Execute an operation.
    The predicate is used to select the operation's parameter values. The parameters can be fully specified explicitly (e. g. `:exec op param1 = 123 & param2 = {1, 2}`), or they can be partially constrained (e. g. `:exec op param1 > 100 & card(param2) >= 2`) to let ProB find a valid combination of parameters. If there are multiple valid combinations of parameters that satisfy the predicate, it is undefined which one is selected by ProB.
    If no predicate is specified, the parameters are not constrained, and ProB will select an arbitrary valid combination of parameters.
 %% Cell type:code id: tags:
 ``` prob
 :help :constants
 ```
 %% Output
    ```
    :constants [PREDICATE]
    ```
    Set up the current machine's constants.
    This is a shorthand for `:exec SETUP_CONSTANTS [PREDICATE]`.
    :constants [PREDICATE]
    Set up the current machine's constants.
    This is a shorthand for `:exec SETUP_CONSTANTS [PREDICATE]`.
 %% Cell type:code id: tags:
 ``` prob
 :help :init
 ```
 %% Output
    ```
    :init [PREDICATE]
    ```
    Initialise the current machine with the specified predicate
    This is a shorthand for `:exec INITIALISATION [PREDICATE]`.
    :init [PREDICATE]
    Initialise the current machine with the specified predicate
    This is a shorthand for `:exec INITIALISATION [PREDICATE]`.
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: repl
    Sets: (none)
    Constants: (none)
    Variables: (none)
    Operations:
    INITIALISATION()
 %% Cell type:code id: tags:
 ``` prob
 ::load
 MACHINE Counter
 CONSTANTS min_value, max_value
 PROPERTIES min_value : MININT..0 & max_value : 0..MAXINT & min_value <= max_value
 VARIABLES value
 INVARIANT value : min_value..max_value
 INITIALISATION value :: min_value..max_value
 OPERATIONS
    add(diff) = SELECT
        value+diff : min_value..max_value
    THEN
        value := value+diff
    END
 END
 ```
 %% Output
    Loaded machine: Counter
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: Counter
    Sets: (none)
    Constants: min_value, max_value
    Variables: value
    Operations:
    SETUP_CONSTANTS()
    SETUP_CONSTANTS()
    SETUP_CONSTANTS()
    SETUP_CONSTANTS()
    More operations may be available (MAX_OPERATIONS/MAX_INITIALISATIONS reached)
 %% Cell type:code id: tags:
 ``` prob
 min_value..max_value
 ```
 %% Output
    :eval: NOT-INITIALISED
 %% Cell type:code id: tags:
 ``` prob
 value
 ```
 %% Output
    :eval: NOT-INITIALISED
 %% Cell type:code id: tags:
 ``` prob
 :constants min_value=5 & max_value=-5
 ```
 %% Output
    java.lang.IllegalArgumentException: Executing operation $setup_constants with predicate min_value=5 & max_value=-5 produced errors: Could not execute operation SETUP_CONSTANTS in state root with additional predicate
 %% Cell type:code id: tags:
 ``` prob
 :constants min_value=-1 & max_value=2
 ```
 %% Output
-    Machine constants set up using operation 2: $setup_constants()
+    Executed operation: $setup_constants()
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: Counter
    Sets: (none)
    Constants: min_value, max_value
    Variables: value
    Operations:
    INITIALISATION()
    INITIALISATION()
    INITIALISATION()
    INITIALISATION()
    More operations may be available (MAX_OPERATIONS/MAX_INITIALISATIONS reached)
 %% Cell type:code id: tags:
 ``` prob
 min_value..max_value
 ```
 %% Output
    $\{-1,0,1,2\}$
    {−1,0,1,2}
 %% Cell type:code id: tags:
 ``` prob
 value
 ```
 %% Output
    :eval: NOT-INITIALISED
 %% Cell type:code id: tags:
 ``` prob
 :init value=-100
 ```
 %% Output
    Error from ProB: ProB reported Errors
    Error: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:6:15 to 6:44)
    // Source code not known
 %% Cell type:code id: tags:
 ``` prob
 :init value=2
 ```
 %% Output
-    Machine initialised using operation 7: $initialise_machine()
+    Executed operation: $initialise_machine()
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: Counter
    Sets: (none)
    Constants: min_value, max_value
    Variables: value
    Operations:
    add(-3)
    add(-2)
    add(-1)
    add(0)
 %% Cell type:code id: tags:
 ``` prob
 value
 ```
 %% Output
    $2$
    2
 %% Cell type:code id: tags:
 ``` prob
 :exec add diff=-1
 ```
 %% Output
    Executed operation: add(-1)
 %% Cell type:code id: tags:
 ``` prob
 :browse
 ```
 %% Output
    Machine: Counter
    Sets: (none)
    Constants: min_value, max_value
    Variables: value
    Operations:
    add(-2)
    add(-1)
    add(0)
    add(1)
 %% Cell type:code id: tags:
 ``` prob
 value
 ```
 %% Output
    $1$
    1
 %% Cell type:code id: tags:
 ``` prob
 :stats
 ```
 %% Output
    **Explored States:** 4/9
    **Transitions:** 16
    Explored States: 4/9
    Transitions: 16
 %% Cell type:markdown id: tags:
 Useful error messages are shown when an operation cannot be executed.
 %% Cell type:code id: tags:
 ``` prob
 :constants
 ```
 %% Output
    java.lang.IllegalArgumentException: Executing operation $setup_constants with predicate 1=1 produced errors: Machine is already initialised, cannot execute SETUP_CONSTANTS
 %% Cell type:code id: tags:
 ``` prob
 :init
 ```
 %% Output
    java.lang.IllegalArgumentException: Executing operation $initialise_machine with predicate 1=1 produced errors: Machine is already initialised, cannot execute INITIALISATION
 %% Cell type:code id: tags:
 ``` prob
 :exec nope
 ```
 %% Output
    java.lang.IllegalArgumentException: Executing operation nope with predicate 1=1 produced errors: Unknown Operation nope
 %% Cell type:code id: tags:
 ``` prob
 :exec add 1=0
 ```
 %% Output
    java.lang.IllegalArgumentException: Executing operation add with predicate 1=0 produced errors: Could not execute operation add in state 6 with additional predicate (but a transition for operation exists)
 %% Cell type:code id: tags:
 ``` prob
 ::load
 MACHINE NoConstants
 VARIABLES z
 INVARIANT z : MININT..MAXINT
 INITIALISATION z :: {0, 1}
 END
 ```
 %% Output
    Loaded machine: NoConstants
 %% Cell type:code id: tags:
 ``` prob
 :constants
 ```
 %% Output
    java.lang.IllegalArgumentException: Executing operation $setup_constants with predicate 1=1 produced errors: Could not execute operation SETUP_CONSTANTS in state root
 %% Cell type:code id: tags:
 ``` prob
 :init z = -1
 ```
 %% Output
    Error from ProB: ProB reported Errors
    Error: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:4:15 to 4:26)
    // Source code not known
 %% Cell type:markdown id: tags:
 `SETUP_CONSTANTS` and `INITIALISATION` can be used as operation names.
 %% Cell type:code id: tags:
 ``` prob
 ::load
 MACHINE Foo
 CONSTANTS x
 PROPERTIES x : MININT..MAXINT
 VARIABLES y
 INVARIANT y : MININT..MAXINT
 INITIALISATION y :: MININT..MAXINT
 END
 ```
 %% Output
    Loaded machine: Foo
 %% Cell type:code id: tags:
 ``` prob
 :exec SETUP_CONSTANTS x = 1
 ```
 %% Output
    Executed operation: $setup_constants()
 %% Cell type:code id: tags:
 ``` prob
 :exec INITIALISATION y = 2
 ```
 %% Output
    Executed operation: $initialise_machine()
 %% Cell type:code id: tags:
 ``` prob
 x
 ```
 %% Output
    $1$
    1
 %% Cell type:code id: tags:
 ``` prob
 y
 ```
 %% Output
    $2$
    2
 %% Cell type:markdown id: tags:
 Local variables can be used in operation predicates.
 %% Cell type:code id: tags:
 ``` prob
 ::load
 MACHINE Counter
 CONSTANTS min_value, max_value
 PROPERTIES min_value : MININT..0 & max_value : 0..MAXINT & min_value <= max_value
 VARIABLES value
 INVARIANT value : min_value..max_value
 INITIALISATION value :: min_value..max_value
 OPERATIONS
    add(diff) = SELECT
        value+diff : min_value..max_value
    THEN
        value := value+diff
    END
 END
 ```
 %% Output
    Loaded machine: Counter
 %% Cell type:code id: tags:
 ``` prob
 :let one 1
 ```
 %% Output
    $1$
    1
 %% Cell type:code id: tags:
 ``` prob
 :let two 2
 ```
 %% Output
    $2$
    2
 %% Cell type:code id: tags:
 ``` prob
 :constants min_value=-one & max_value=two
 ```
 %% Output
-    Machine constants set up using operation 0: $setup_constants()
+    Executed operation: $setup_constants()
 %% Cell type:code id: tags:
 ``` prob
 min_value..max_value
 ```
 %% Output
    $\{-1,0,1,2\}$
    {−1,0,1,2}
 %% Cell type:code id: tags:
 ``` prob
 :init value=one
 ```
 %% Output
-    Machine initialised using operation 3: $initialise_machine()
+    Executed operation: $initialise_machine()
 %% Cell type:code id: tags:
 ``` prob
 value
 ```
 %% Output
    $1$
    1
 %% Cell type:code id: tags:
 ``` prob
 :exec add diff=-one
 ```
 %% Output
    Executed operation: add(-1)
 %% Cell type:code id: tags:
 ``` prob
 value
 ```
 %% Output
    $0$
    0

--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -28,11 +28,13 @@ import com.google.inject.Singleton;
 import de.prob.animator.ReusableAnimator;
 import de.prob.animator.domainobjects.ErrorItem;
+import de.prob.animator.domainobjects.FormulaExpand;
 import de.prob.exception.ProBError;
 import de.prob.scripting.ClassicalBFactory;
 import de.prob.statespace.AnimationSelector;
 import de.prob.statespace.StateSpace;
 import de.prob.statespace.Trace;
+import de.prob.statespace.Transition;
 import de.prob2.jupyter.commands.AssertCommand;
 import de.prob2.jupyter.commands.BrowseCommand;
 import de.prob2.jupyter.commands.BsymbCommand;
@@ -302,6 +304,24 @@ public final class ProBKernel extends BaseKernel {
 		this.setCurrentMachineDirectory(machineDirectory);
 	}
+	public @NotNull DisplayData executeOperation(final @NotNull String name, final @Nullable String predicate) {
+		final Trace trace = this.animationSelector.getCurrentTrace();
+		final String translatedOpName = Transition.unprettifyName(name);
+		final String modifiedPredicate;
+		if (predicate == null) {
+			modifiedPredicate = "1=1";
+		} else {
+			modifiedPredicate = this.insertLetVariables(predicate);
+		}
+		final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), translatedOpName, modifiedPredicate, 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("Executed operation: %s", op.getRep()));
+	}
 	@Override
 	public @NotNull String getBanner() {
 		return "ProB Interactive Expression and Predicate Evaluator (on Jupyter)\nType \":help\" for more information.";

--- a/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/ConstantsCommand.java
@@ -64,19 +64,7 @@ public final class ConstantsCommand implements Command {
 	@Override
 	public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
-		final Trace trace = this.animationSelector.getCurrentTrace();
+		return this.kernelProvider.get().executeOperation(Transition.SETUP_CONSTANTS_NAME, args.get(PREDICATE_PARAM).orElse(null));
-		final String predicate;
-		if (!args.get(PREDICATE_PARAM).isPresent()) {
-			predicate = "1=1";
-		} else {
-			predicate = this.kernelProvider.get().insertLetVariables(args.get(PREDICATE_PARAM).get());
-		}
-		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()));
 	}
 	@Override

--- a/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/ExecCommand.java
@@ -70,21 +70,7 @@ public final class ExecCommand implements Command {
 	@Override
 	public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
-		final Trace trace = this.animationSelector.getCurrentTrace();
+		return this.kernelProvider.get().executeOperation(args.get(OPERATION_PARAM), args.get(PREDICATE_PARAM).orElse(null));
-		final String translatedOpName = Transition.unprettifyName(args.get(OPERATION_PARAM));
-		final String predicate;
-		if (!args.get(PREDICATE_PARAM).isPresent()) {
-			predicate = "1=1";
-		} else {
-			predicate = this.kernelProvider.get().insertLetVariables(args.get(PREDICATE_PARAM).get());
-		}
-		final List<Transition> ops = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), translatedOpName, 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("Executed operation: %s", op.getRep()));
 	}
 	@Override

--- a/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/InitialiseCommand.java
@@ -64,19 +64,7 @@ public final class InitialiseCommand implements Command {
 	@Override
 	public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
-		final Trace trace = this.animationSelector.getCurrentTrace();
+		return this.kernelProvider.get().executeOperation(Transition.INITIALISE_MACHINE_NAME, args.get(PREDICATE_PARAM).orElse(null));
-		final String predicate;
-		if (!args.get(PREDICATE_PARAM).isPresent()) {
-			predicate = "1=1";
-		} else {
-			predicate = this.kernelProvider.get().insertLetVariables(args.get(PREDICATE_PARAM).get());
-		}
-		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()));
 	}
 	@Override