Skip to content
Snippets Groups Projects
Commit 76e7a10b authored by dgelessus's avatar dgelessus
Browse files

Remove uses of deprecated ClassicalBFactory.create method

parent d8b83600
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
notebooks/tests/animate.ipynb
+ 4
− 4
View file @ 76e7a10b
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:help :browse :help :browse
``` ```
%% Output %% Output
``` ```
:browse :browse
``` ```
Show information about the current state. 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 transitions that are available in the current state. Each transition has a numeric ID, which can be passed to `:exec` to execute that transition. The output shows the names of all sets, constants, and variables defined by the current machine, as well as a list of transitions that are available in the current state. Each transition has a numeric ID, which can be passed to `:exec` to execute that transition.
``` ```
:browse :browse
``` ```
Show information about the current state. 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 transitions that are available in the current state. Each transition has a numeric ID, which can be passed to `:exec` to execute that transition. The output shows the names of all sets, constants, and variables defined by the current machine, as well as a list of transitions that are available in the current state. Each transition has a numeric ID, which can be passed to `:exec` to execute that transition.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:help :exec :help :exec
``` ```
%% Output %% Output
``` ```
:exec OPERATION [PREDICATE] :exec OPERATION [PREDICATE]
:exec OPERATION_ID :exec OPERATION_ID
``` ```
Execute an operation with the specified predicate, or by its ID. Execute an operation with the specified predicate, or by its ID.
In the first form, the given operation is executed. If the optional predicate is specified, a transition is found for which the predicate is $\mathit{TRUE}$. The predicate can be used to restrict what values the operation's parameters or the variables in the next state may have. In the first form, the given operation is executed. If the optional predicate is specified, a transition is found for which the predicate is $\mathit{TRUE}$. The predicate can be used to restrict what values the operation's parameters or the variables in the next state may have.
In the second form, a known transition with the given numeric ID is executed. A list of the current state's available transitions and their IDs can be viewed using `:browse`. Only transition IDs from the current state can be executed. In the second form, a known transition with the given numeric ID is executed. A list of the current state's available transitions and their IDs can be viewed using `:browse`. Only transition IDs from the current state can be executed.
``` ```
:exec OPERATION [PREDICATE] :exec OPERATION [PREDICATE]
:exec OPERATION_ID :exec OPERATION_ID
``` ```
Execute an operation with the specified predicate, or by its ID. Execute an operation with the specified predicate, or by its ID.
In the first form, the given operation is executed. If the optional predicate is specified, a transition is found for which the predicate is $\mathit{TRUE}$. The predicate can be used to restrict what values the operation's parameters or the variables in the next state may have. In the first form, the given operation is executed. If the optional predicate is specified, a transition is found for which the predicate is $\mathit{TRUE}$. The predicate can be used to restrict what values the operation's parameters or the variables in the next state may have.
In the second form, a known transition with the given numeric ID is executed. A list of the current state's available transitions and their IDs can be viewed using `:browse`. Only transition IDs from the current state can be executed. In the second form, a known transition with the given numeric ID is executed. A list of the current state's available transitions and their IDs can be viewed using `:browse`. Only transition IDs from the current state can be executed.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:help :constants :help :constants
``` ```
%% Output %% Output
``` ```
:constants [PREDICATE] :constants [PREDICATE]
``` ```
Set up the current machine's constants. Set up the current machine's constants.
This is a shorthand for `:exec SETUP_CONSTANTS [PREDICATE]`. This is a shorthand for `:exec SETUP_CONSTANTS [PREDICATE]`.
``` ```
:constants [PREDICATE] :constants [PREDICATE]
``` ```
Set up the current machine's constants. Set up the current machine's constants.
This is a shorthand for `:exec SETUP_CONSTANTS [PREDICATE]`. This is a shorthand for `:exec SETUP_CONSTANTS [PREDICATE]`.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:help :init :help :init
``` ```
%% Output %% Output
``` ```
:init [PREDICATE] :init [PREDICATE]
``` ```
Initialise the current machine with the specified predicate Initialise the current machine with the specified predicate
This is a shorthand for `:exec INITIALISATION [PREDICATE]`. This is a shorthand for `:exec INITIALISATION [PREDICATE]`.
``` ```
:init [PREDICATE] :init [PREDICATE]
``` ```
Initialise the current machine with the specified predicate Initialise the current machine with the specified predicate
This is a shorthand for `:exec INITIALISATION [PREDICATE]`. This is a shorthand for `:exec INITIALISATION [PREDICATE]`.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: repl Machine: repl
Sets: (none) Sets: (none)
Constants: (none) Constants: (none)
Variables: (none) Variables: (none)
Operations: Operations:
0: $initialise_machine() 0: $initialise_machine()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE Counter MACHINE Counter
CONSTANTS min_value, max_value CONSTANTS min_value, max_value
PROPERTIES min_value : MININT..0 & max_value : 0..MAXINT & min_value <= max_value PROPERTIES min_value : MININT..0 & max_value : 0..MAXINT & min_value <= max_value
VARIABLES value VARIABLES value
INVARIANT value : min_value..max_value INVARIANT value : min_value..max_value
INITIALISATION value :: min_value..max_value INITIALISATION value :: min_value..max_value
OPERATIONS OPERATIONS
add(diff) = SELECT add(diff) = SELECT
value+diff : min_value..max_value value+diff : min_value..max_value
THEN THEN
value := value+diff value := value+diff
END END
END END
``` ```
%% Output %% Output
Loaded machine: Counter Loaded machine: Counter
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: Counter Machine: Counter
Sets: (none) Sets: (none)
Constants: min_value, max_value Constants: min_value, max_value
Variables: value Variables: value
Operations: Operations:
0: $setup_constants() 0: $setup_constants()
1: $setup_constants() 1: $setup_constants()
2: $setup_constants() 2: $setup_constants()
3: $setup_constants() 3: $setup_constants()
More operations may be available (MAX_OPERATIONS/MAX_INITIALISATIONS reached) More operations may be available (MAX_OPERATIONS/MAX_INITIALISATIONS reached)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
min_value..max_value min_value..max_value
``` ```
%% Output %% Output
:eval: NOT-INITIALISED :eval: NOT-INITIALISED
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
value value
``` ```
%% Output %% Output
:eval: NOT-INITIALISED :eval: NOT-INITIALISED
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:constants min_value=5 & max_value=-5 :constants min_value=5 & max_value=-5
``` ```
%% Output %% Output
:constants: Could not setup constants with the specified predicate :constants: Could not setup constants with the specified predicate
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:constants min_value=-1 & max_value=2 :constants min_value=-1 & max_value=2
``` ```
%% Output %% Output
Machine constants set up using operation 2: $setup_constants() Machine constants set up using operation 2: $setup_constants()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: Counter Machine: Counter
Sets: (none) Sets: (none)
Constants: min_value, max_value Constants: min_value, max_value
Variables: value Variables: value
Operations: Operations:
4: $initialise_machine() 4: $initialise_machine()
5: $initialise_machine() 5: $initialise_machine()
6: $initialise_machine() 6: $initialise_machine()
7: $initialise_machine() 7: $initialise_machine()
More operations may be available (MAX_OPERATIONS/MAX_INITIALISATIONS reached) More operations may be available (MAX_OPERATIONS/MAX_INITIALISATIONS reached)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
min_value..max_value min_value..max_value
``` ```
%% Output %% Output
$\{-1,0,1,2\}$ $\{-1,0,1,2\}$
{−1,0,1,2} {−1,0,1,2}
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
value value
``` ```
%% Output %% Output
:eval: NOT-INITIALISED :eval: NOT-INITIALISED
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:init value=-100 :init value=-100
``` ```
%% Output %% Output
Error from ProB: ProB reported Errors Error from ProB: ProB reported Errors
Error: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/from_string.mch:6:15 to 6:44) Error: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:6:15 to 6:44)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:init value=2 :init value=2
``` ```
%% Output %% Output
Machine initialised using operation 7: $initialise_machine() Machine initialised using operation 7: $initialise_machine()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: Counter Machine: Counter
Sets: (none) Sets: (none)
Constants: min_value, max_value Constants: min_value, max_value
Variables: value Variables: value
Operations: Operations:
8: add(-3) 8: add(-3)
9: add(-2) 9: add(-2)
10: add(-1) 10: add(-1)
11: add(0) 11: add(0)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
value value
``` ```
%% Output %% Output
$2$ $2$
2 2
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec add diff=-1 :exec add diff=-1
``` ```
%% Output %% Output
Executed operation 10: add(-1) Executed operation 10: add(-1)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: Counter Machine: Counter
Sets: (none) Sets: (none)
Constants: min_value, max_value Constants: min_value, max_value
Variables: value Variables: value
Operations: Operations:
12: add(-2) 12: add(-2)
13: add(-1) 13: add(-1)
14: add(0) 14: add(0)
15: add(1) 15: add(1)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
value value
``` ```
%% Output %% Output
$1$ $1$
1 1
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec 15 :exec 15
``` ```
%% Output %% Output
Executed operation 15: add(1) Executed operation 15: add(1)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:browse :browse
``` ```
%% Output %% Output
Machine: Counter Machine: Counter
Sets: (none) Sets: (none)
Constants: min_value, max_value Constants: min_value, max_value
Variables: value Variables: value
Operations: Operations:
8: add(-3) 8: add(-3)
9: add(-2) 9: add(-2)
10: add(-1) 10: add(-1)
11: add(0) 11: add(0)
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec 10 1=1 :exec 10 1=1
``` ```
%% Output %% Output
:exec: Cannot specify a predicate when executing an operation by ID :exec: Cannot specify a predicate when executing an operation by ID
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
Useful error messages are shown when an operation cannot be executed. Useful error messages are shown when an operation cannot be executed.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:constants :constants
``` ```
%% Output %% Output
:constants: Machine constants are already set up :constants: Machine constants are already set up
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:init :init
``` ```
%% Output %% Output
:init: Machine is already initialised :init: Machine is already initialised
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec nope :exec nope
``` ```
%% Output %% Output
:exec: Could not execute operation nope :exec: Could not execute operation nope
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec add 1=0 :exec add 1=0
``` ```
%% Output %% Output
:exec: Could not execute operation add with the given predicate :exec: Could not execute operation add with the given predicate
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE NoConstants MACHINE NoConstants
VARIABLES z VARIABLES z
INVARIANT z : MININT..MAXINT INVARIANT z : MININT..MAXINT
INITIALISATION z :: {0, 1} INITIALISATION z :: {0, 1}
END END
``` ```
%% Output %% Output
Loaded machine: NoConstants Loaded machine: NoConstants
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:constants :constants
``` ```
%% Output %% Output
:constants: Machine has no constants, use :init instead :constants: Machine has no constants, use :init instead
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:init z = -1 :init z = -1
``` ```
%% Output %% Output
Error from ProB: ProB reported Errors Error from ProB: ProB reported Errors
Error: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/from_string.mch:4:15 to 4:26) Error: INITIALISATION FAILS (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:4:15 to 4:26)
%% Cell type:markdown id: tags: %% Cell type:markdown id: tags:
`SETUP_CONSTANTS` and `INITIALISATION` can be used as operation names. `SETUP_CONSTANTS` and `INITIALISATION` can be used as operation names.
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
::load ::load
MACHINE Foo MACHINE Foo
CONSTANTS x CONSTANTS x
PROPERTIES x : MININT..MAXINT PROPERTIES x : MININT..MAXINT
VARIABLES y VARIABLES y
INVARIANT y : MININT..MAXINT INVARIANT y : MININT..MAXINT
INITIALISATION y :: MININT..MAXINT INITIALISATION y :: MININT..MAXINT
END END
``` ```
%% Output %% Output
Loaded machine: Foo Loaded machine: Foo
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec SETUP_CONSTANTS x = 1 :exec SETUP_CONSTANTS x = 1
``` ```
%% Output %% Output
Executed operation 2: $setup_constants() Executed operation 2: $setup_constants()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
:exec INITIALISATION y = 2 :exec INITIALISATION y = 2
``` ```
%% Output %% Output
Executed operation 7: $initialise_machine() Executed operation 7: $initialise_machine()
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
x x
``` ```
%% Output %% Output
$1$ $1$
1 1
%% Cell type:code id: tags: %% Cell type:code id: tags:
``` prob ``` prob
y y
``` ```
%% Output %% Output
$2$ $2$
2 2
......
src/main/java/de/prob2/jupyter/ProBKernel.java
+ 1
− 1
View file @ 76e7a10b
...@@ -160,7 +160,7 @@ public final class ProBKernel extends BaseKernel { ...@@ -160,7 +160,7 @@ public final class ProBKernel extends BaseKernel {
this.commands.put("::render", injector.getInstance(RenderCommand.class)); this.commands.put("::render", injector.getInstance(RenderCommand.class));
this.commands.put(":prettyprint", injector.getInstance(PrettyPrintCommand.class)); this.commands.put(":prettyprint", injector.getInstance(PrettyPrintCommand.class));
this.animationSelector.changeCurrentAnimation(new Trace(classicalBFactory.create("MACHINE repl END").load())); this.animationSelector.changeCurrentAnimation(new Trace(classicalBFactory.create("(initial Jupyter machine)", "MACHINE repl END").load()));
} }
public @NotNull Map<@NotNull String, @NotNull Command> getCommands() { public @NotNull Map<@NotNull String, @NotNull Command> getCommands() {
......
src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java
+ 1
− 1
View file @ 76e7a10b
...@@ -56,7 +56,7 @@ public final class LoadCellCommand implements Command { ...@@ -56,7 +56,7 @@ public final class LoadCellCommand implements Command {
final List<String> args = CommandUtils.splitArgs(prefsString); final List<String> args = CommandUtils.splitArgs(prefsString);
final Map<String, String> preferences = CommandUtils.parsePreferences(args); final Map<String, String> preferences = CommandUtils.parsePreferences(args);
this.animationSelector.changeCurrentAnimation(new Trace(this.classicalBFactory.create(body).load(preferences))); this.animationSelector.changeCurrentAnimation(new Trace(this.classicalBFactory.create("(machine from Jupyter cell)", body).load(preferences)));
return new DisplayData("Loaded machine: " + this.animationSelector.getCurrentTrace().getStateSpace().getMainComponent()); return new DisplayData("Loaded machine: " + this.animationSelector.getCurrentTrace().getStateSpace().getMainComponent());
} }
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment