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

Make :exec/:init/:constants automatically move in trace as needed

parent bc7eafab
No related tags found
No related merge requests found
Pipeline #43247 passed
Stage: test
Show whitespace changes
Inline Side-by-side
CHANGELOG.md
+ 3
− 0
View file @ 3c030656
......@@ -4,6 +4,9 @@
* Updated ProB 2 to version 4.0.0-SNAPSHOT.
* Improved the performance of loading machines by reusing the existing instance of ProB instead of starting a new one for each machine.
* Changed the `:exec`, `:init` and `:constants` commands to automatically move forward or backward in the trace to allow the command to execute successfully.
* Executing `:init` in an already initialised state will return to the last uninitialised state to re-initialise the machine (possibly with different initial values). The same works for `:constants`. Previously this caused an error "Machine is already initialised" or "Machine constants are already set up".
* Executing an operation in an uninitialised state will automatically initialise the machine with an arbitrary valid initialisation transition. If the machine has constants, they are also set up automatically in a similar way. This is useful if the machine's constants/initial variables are unambiguous or the exact values are not important. Previously this caused an error "Machine is not initialised".
* Significantly refactored the logic for parsing commands and their arguments.
* This is an internal change and should not affect any user-visible behavior. That is, all inputs that were accepted by previous versions should still be accepted - if any previously valid inputs are no longer accepted, this is a bug.
* As a side effect, the inspection and code completion features now work better in a few edge cases.
......
notebooks/tests/animate.ipynb
+ 240
− 60
View file @ 3c030656
%% 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
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
Executed operation: INITIALISATION()
%% 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
: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}
OPERATIONS
nothing = skip
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: Machine is already initialised, cannot execute SETUP_CONSTANTS
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
:init z = -1
```
%% Output
java.lang.IllegalArgumentException: Executing operation $initialise_machine with predicate 1=1 produced errors: Machine is already initialised, cannot execute INITIALISATION
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:
Executing an operation in an uninitialised machine automatically initialises the machine.
%% Cell type:code id: tags:
``` prob
:exec nope
:exec nothing
```
%% Output
java.lang.IllegalArgumentException: Executing operation nope with predicate 1=1 produced errors: Unknown Operation nope
Machine was not initialised yet. Automatically initialised machine using arbitrary transition: INITIALISATION()
Executed operation: nothing()
%% Cell type:markdown id: tags:
An already initialised machine can be reinitialised.
%% Cell type:code id: tags:
``` prob
:exec add 1=0
:init z = 1
```
%% 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)
Machine was already initialised. Returned to uninitialised state to re-initialise the machine.
Executed operation: INITIALISATION()
%% Cell type:markdown id: tags:
The same also works if the machine has constants.
%% Cell type:code id: tags:
``` prob
::load
MACHINE NoConstants
MACHINE ItHasConstants
CONSTANTS c
PROPERTIES c : MININT..MAXINT
VARIABLES z
INVARIANT z : MININT..MAXINT
INITIALISATION z :: {0, 1}
OPERATIONS
nothing = skip
END
```
%% Output
Loaded machine: NoConstants
Loaded machine: ItHasConstants
%% Cell type:code id: tags:
``` prob
:constants
:init z = 0
```
%% Output
java.lang.IllegalArgumentException: Executing operation $setup_constants with predicate 1=1 produced errors: Could not execute operation SETUP_CONSTANTS in state root
java.lang.IllegalArgumentException: Executing operation $initialise_machine with predicate z = 0 produced errors: Could not execute operation INITIALISATION in state root with additional predicate
%% Cell type:code id: tags:
``` prob
:init z = -1
:constants c = 2
```
%% 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
Executed operation: SETUP_CONSTANTS()
%% Cell type:code id: tags:
``` prob
:exec nothing
```
%% Output
Machine was not initialised yet. Automatically initialised machine using arbitrary transition: INITIALISATION()
Executed operation: nothing()
%% Cell type:code id: tags:
``` prob
:init z = 1
```
%% Output
Machine was already initialised. Returned to uninitialised state to re-initialise the machine.
Executed operation: INITIALISATION()
%% Cell type:code id: tags:
``` prob
:goto -1
```
%% Output
Changed to state with index -1
%% Cell type:code id: tags:
``` prob
:exec nothing
```
%% Output
Machine constants were not set up yet. Automatically set up constants using arbitrary transition: SETUP_CONSTANTS()
Machine was not initialised yet. Automatically initialised machine using arbitrary transition: INITIALISATION()
Executed operation: nothing()
%% 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: INITIALISATION()
%% 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
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
Executed operation: INITIALISATION()
%% 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
......
src/main/java/de/prob2/jupyter/ProBKernel.java
+ 66
− 5
View file @ 3c030656
......@@ -15,6 +15,7 @@ import java.util.List;
import java.util.Map;
import java.util.Optional;
import java.util.Properties;
import java.util.Set;
import java.util.concurrent.atomic.AtomicReference;
import java.util.function.Function;
import java.util.regex.Matcher;
......@@ -32,6 +33,7 @@ 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.State;
import de.prob.statespace.StateSpace;
import de.prob.statespace.Trace;
import de.prob.statespace.Transition;
......@@ -304,22 +306,81 @@ public final class ProBKernel extends BaseKernel {
this.setCurrentMachineDirectory(machineDirectory);
}
private static @NotNull Transition singleTransitionFromPredicate(final State state, final String opName, final String predicate) {
final List<Transition> ops = state.getStateSpace().transitionFromPredicate(state, opName, predicate, 1);
assert !ops.isEmpty();
return ops.get(0);
}
public @NotNull DisplayData executeOperation(final @NotNull String name, final @Nullable String predicate) {
final Trace trace = this.animationSelector.getCurrentTrace();
Trace trace = this.animationSelector.getCurrentTrace();
final String translatedOpName = Transition.unprettifyName(name);
final StringBuilder sb = new StringBuilder();
if (Transition.SETUP_CONSTANTS_NAME.equals(translatedOpName) && trace.getCurrentState().isConstantsSetUp()) {
trace = trace.gotoPosition(-1);
sb.append("Machine constants were already set up. Returned to root state to set up machine constants again.\n");
} else if (Transition.INITIALISE_MACHINE_NAME.equals(translatedOpName) && trace.getCurrentState().isInitialised()) {
// The last uninitialised state may be at index 0 (if SETUP_CONSTANTS exists) or at index -1 (if not).
trace = trace.gotoPosition(0);
if (trace.getCurrentState().isInitialised()) {
trace = trace.gotoPosition(-1);
}
sb.append("Machine was already initialised. Returned to uninitialised state to re-initialise the machine.\n");
}
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);
Transition op;
try {
op = singleTransitionFromPredicate(trace.getCurrentState(), translatedOpName, modifiedPredicate);
} catch (IllegalArgumentException e) {
if (!trace.getCurrentState().isConstantsSetUp()) {
if (Transition.PARTIAL_SETUP_CONSTANTS_NAME.equals(translatedOpName) || Transition.SETUP_CONSTANTS_NAME.equals(translatedOpName)) {
throw e;
} else {
final Set<Transition> setupConstantsTransitions = trace.getNextTransitions();
if (setupConstantsTransitions.isEmpty()) {
throw new UserErrorException("Machine constants are not set up and no valid constant values were found automatically - cannot execute operation " + name, e);
}
final Transition setupConstants = setupConstantsTransitions.iterator().next();
trace = trace.add(setupConstants);
trace.getStateSpace().evaluateTransitions(Collections.singleton(setupConstants), FormulaExpand.TRUNCATE);
sb.append("Machine constants were not set up yet. Automatically set up constants using arbitrary transition: ");
sb.append(setupConstants.getPrettyRep());
sb.append('\n');
}
}
if (!trace.getCurrentState().isInitialised()) {
if (Transition.PARTIAL_SETUP_CONSTANTS_NAME.equals(translatedOpName) || Transition.SETUP_CONSTANTS_NAME.equals(translatedOpName) || Transition.INITIALISE_MACHINE_NAME.equals(translatedOpName)) {
throw e;
} else {
final Set<Transition> initialisationTransitions = trace.getNextTransitions();
if (initialisationTransitions.isEmpty()) {
throw new UserErrorException("Machine is not initialised and no valid initialisation was found automatically - cannot execute operation " + name, e);
}
final Transition initialisation = initialisationTransitions.iterator().next();
trace = trace.add(initialisation);
trace.getStateSpace().evaluateTransitions(Collections.singleton(initialisation), FormulaExpand.TRUNCATE);
sb.append("Machine was not initialised yet. Automatically initialised machine using arbitrary transition: ");
sb.append(initialisation.getPrettyRep());
sb.append('\n');
}
}
op = singleTransitionFromPredicate(trace.getCurrentState(), translatedOpName, modifiedPredicate);
}
this.animationSelector.changeCurrentAnimation(trace.add(op));
trace.getStateSpace().evaluateTransitions(Collections.singleton(op), FormulaExpand.TRUNCATE);
return new DisplayData(String.format("Executed operation: %s", op.getPrettyRep()));
sb.append("Executed operation: ");
sb.append(op.getPrettyRep());
return new DisplayData(sb.toString());
}
@Override
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment