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

Allow executing existing operations by ID

parent 8c85481e
Branches
Tags
No related merge requests found
......@@ -41,6 +41,7 @@ dependencies {
compile(group: "de.hhu.stups", name: "de.prob2.kernel", version: "3.2.10-SNAPSHOT", changing: true)
compile(group: "io.github.spencerpark", name: "jupyter-jvm-basekernel", version: "2.0.0-SNAPSHOT", changing: true)
compile(group: "org.jetbrains", name: "annotations", version: "16.0.1")
compile(group: "se.sawano.java", name: "alphanumeric-comparator", version: "1.4.1")
}
sourceCompatibility = "1.8"
......
%% Cell type:code id: tags:
``` prob
:help :browse
```
%% Output
:browse
Show information about the current state
%% Cell type:code id: tags:
``` prob
:help :exec
```
%% Output
:exec OPERATION [PREDICATE]
:exec OPERATION_ID
Execute an operation with the specified predicate
Execute an operation with the specified predicate, or by its ID
%% Cell type:code id: tags:
``` prob
:help :constants
```
%% Output
:constants [PREDICATE]
Set up the current machine's constants with the specified predicate
%% Cell type:code id: tags:
``` prob
:help :init
```
%% Output
:initialise [PREDICATE]
:init [PREDICATE]
Initialise the current machine with the specified predicate
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: repl
Sets: (none)
Constants: (none)
Variables: (none)
Operations: (none)
Operations:
0: $initialise_machine()
%% 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
[2018-05-23 12:33:10,169, T+6055] "Shell-0" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh
[2018-05-23 12:33:11,574, T+7460] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 52196
[2018-05-23 12:33:11,575, T+7461] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 1828
[2018-05-23 12:33:11,580, T+7466] "ProB Output Logger for instance 5b68ad44" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --
[2018-05-23 12:33:11,598, T+7484] "ProB Output Logger for instance 5b68ad44" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1
[2018-05-23 12:33:11,866, T+7752] "ProB Output Logger for instance 5b68ad44" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-05-16 13:34:59.07),Counter,[/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests])
[2018-05-23 15:13:10,940, T+6251] "Shell-0" de.prob.cli.PrologProcessProvider.makeProcess(PrologProcessProvider.java:64): [INFO] Starting ProB's Prolog Core. Path is /Users/david/.prob/prob2-3.2.10-SNAPSHOT/probcli.sh
[2018-05-23 15:13:12,528, T+7839] "Shell-0" de.prob.cli.PortPattern.setValue(PortPattern.java:30): [INFO] Server has started and listens on port 56654
[2018-05-23 15:13:12,530, T+7841] "Shell-0" de.prob.cli.InterruptRefPattern.setValue(InterruptRefPattern.java:29): [INFO] Server can receive user interrupts via reference 3008
[2018-05-23 15:13:12,533, T+7844] "ProB Output Logger for instance 7bd5a630" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] -- starting command loop --
[2018-05-23 15:13:12,554, T+7865] "ProB Output Logger for instance 7bd5a630" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Connected: 127.0.0.1
[2018-05-23 15:13:12,842, T+8153] "ProB Output Logger for instance 7bd5a630" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] loading_classical_b(parser_version(2018-05-16 13:34:59.07),Counter,[/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests])
Loaded machine: Counter : []
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
[2018-05-23 15:13:13,175, T+8486] "ProB Output Logger for instance 7bd5a630" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 120 ms (walltime: 150 ms)
[2018-05-23 15:13:13,176, T+8487] "ProB Output Logger for instance 7bd5a630" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)
[2018-05-23 15:13:13,182, T+8493] "ProB Output Logger for instance 7bd5a630" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)
[2018-05-23 15:13:13,183, T+8494] "ProB Output Logger for instance 7bd5a630" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 0 ms (walltime: 0 ms)
Machine: Counter
Sets: (none)
Constants: min_value, max_value
Variables: value
Operations: add(diff)
Operations:
0: $setup_constants()
1: $setup_constants()
2: $setup_constants()
3: $setup_constants()
More operations may be available (MAX_OPERATIONS/MAX_INITIALISATIONS reached)
%% Cell type:code id: tags:
``` prob
min_value..max_value
```
%% Output
NOT-INITIALISED
%% Cell type:code id: tags:
``` prob
value
```
%% Output
NOT-INITIALISED
%% Cell type:code id: tags:
``` prob
:constants min_value=-1 & max_value=2
```
%% Output
[2018-05-23 12:33:12,406, T+8292] "ProB Output Logger for instance 5b68ad44" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 80 ms (walltime: 80 ms)
[2018-05-23 15:13:13,491, T+8802] "ProB Output Logger for instance 7bd5a630" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] % Runtime for SOLUTION for SETUP_CONSTANTS: 20 ms (walltime: 20 ms)
Machine constants set up
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: Counter
Sets: (none)
Constants: min_value, max_value
Variables: value
Operations: add(diff)
Operations:
4: $initialise_machine()
5: $initialise_machine()
6: $initialise_machine()
7: $initialise_machine()
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}
%% Cell type:code id: tags:
``` prob
value
```
%% Output
NOT-INITIALISED
%% Cell type:code id: tags:
``` prob
:init value=2
```
%% Output
[2018-05-23 12:33:12,769, T+8655] "ProB Output Logger for instance 5b68ad44" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] 
[2018-05-23 12:33:12,769, T+8655] "ProB Output Logger for instance 5b68ad44" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ALL OPERATIONS COVERED
[2018-05-23 12:33:12,770, T+8656] "ProB Output Logger for instance 5b68ad44" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] 
[2018-05-23 15:13:13,866, T+9177] "ProB Output Logger for instance 7bd5a630" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] 
[2018-05-23 15:13:13,867, T+9178] "ProB Output Logger for instance 7bd5a630" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ALL OPERATIONS COVERED
[2018-05-23 15:13:13,868, T+9179] "ProB Output Logger for instance 7bd5a630" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] 
Machine initialised
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: Counter
Sets: (none)
Constants: min_value, max_value
Variables: value
Operations:
8: add(-3)
9: add(-2)
10: add(-1)
11: add(0)
%% Cell type:code id: tags:
``` prob
value
```
%% Output
2
%% Cell type:code id: tags:
``` prob
:exec add diff=-1
```
%% Output
Executed operation add
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: Counter
Sets: (none)
Constants: min_value, max_value
Variables: value
Operations:
12: add(-2)
13: add(-1)
14: add(0)
15: add(1)
%% Cell type:code id: tags:
``` prob
value
```
%% Output
1
%% Cell type:code id: tags:
``` prob
:exec 15
```
%% Output
Executed operation 15
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: Counter
Sets: (none)
Constants: min_value, max_value
Variables: value
Operations:
8: add(-3)
9: add(-2)
10: add(-1)
11: add(0)
%% Cell type:code id: tags:
``` prob
:exec 10 1=1
```
%% Output
:exec: Cannot specify a predicate when executing an operation by ID
......
package de.prob2.jupyter.commands;
import java.util.ArrayList;
import java.util.Comparator;
import java.util.List;
import java.util.function.Function;
import java.util.stream.Collectors;
import com.google.inject.Inject;
import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.model.representation.AbstractElement;
import de.prob.model.representation.BEvent;
import de.prob.model.representation.Constant;
import de.prob.model.representation.Set;
import de.prob.model.representation.Variable;
import de.prob.statespace.AnimationSelector;
import de.prob.statespace.Trace;
import de.prob.statespace.Transition;
import de.prob2.jupyter.ProBKernel;
......@@ -19,6 +23,8 @@ import io.github.spencerpark.jupyter.messages.DisplayData;
import org.jetbrains.annotations.NotNull;
import se.sawano.java.text.AlphanumericComparator;
public final class BrowseCommand implements LineCommand {
private final @NotNull AnimationSelector animationSelector;
......@@ -65,8 +71,18 @@ public final class BrowseCommand implements LineCommand {
sb.append("\nVariables: ");
sb.append(elementsToString(mainComponent, Variable.class, Variable::getName));
sb.append("\nOperations: ");
sb.append(elementsToString(mainComponent, BEvent.class, Object::toString));
final List<Transition> sortedTransitions = new ArrayList<>(trace.getNextTransitions(true, FormulaExpand.TRUNCATE));
// Transition IDs are strings, but they almost always contain numbers.
sortedTransitions.sort(Comparator.comparing(Transition::getId, new AlphanumericComparator()));
for (final Transition t : sortedTransitions) {
sb.append('\n');
sb.append(t.getId());
sb.append(": ");
sb.append(t.getRep());
}
if (trace.getCurrentState().isMaxTransitionsCalculated()) {
sb.append("\nMore operations may be available (MAX_OPERATIONS/MAX_INITIALISATIONS reached)");
}
return new DisplayData(sb.toString());
}
}
package de.prob2.jupyter.commands;
import java.util.List;
import java.util.Optional;
import com.google.inject.Inject;
......@@ -26,25 +27,39 @@ public final class ExecCommand implements LineCommand {
@Override
public @NotNull String getSyntax() {
return ":exec OPERATION [PREDICATE]";
return ":exec OPERATION [PREDICATE]\n:exec OPERATION_ID";
}
@Override
public @NotNull String getShortHelp() {
return "Execute an operation with the specified predicate";
return "Execute an operation with the specified predicate, or by its ID";
}
@Override
public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String name, final @NotNull String argString) {
final String[] split = argString.split("\\h", 2);
assert split.length >= 1;
final String opName = split[0];
final String predicate = split.length >= 2 ? split[1] : "1=1";
final String opNameOrId = split[0];
final Trace trace = this.animationSelector.getCurrentTrace();
final List<Transition> transitions = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), opName, predicate, 1);
// Check if the argument is an ID, by searching for a transition with that ID.
final Optional<Transition> opt = trace.getNextTransitions().stream().filter(t -> t.getId().equals(opNameOrId)).findAny();
final Transition op;
if (opt.isPresent()) {
// Transition found, nothing else needs to be done.
if (split.length != 1) {
throw new CommandExecutionException(name, "Cannot specify a predicate when executing an operation by ID");
}
op = opt.get();
} else {
// Transition not found, assume that the argument is an operation name instead.
final String predicate = split.length >= 2 ? split[1] : "1=1";
final List<Transition> transitions = trace.getStateSpace().transitionFromPredicate(trace.getCurrentState(), opNameOrId, predicate, 1);
assert transitions.size() == 1;
final Transition op = transitions.get(0);
op = transitions.get(0);
}
this.animationSelector.changeCurrentAnimation(trace.add(op));
return new DisplayData(String.format("Executed operation %s", opName));
return new DisplayData(String.format("Executed operation %s", opNameOrId));
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment