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

Use new StateSpace preference methods in :pref implementation

parent 8ecd72e1
Branches
No related tags found
No related merge requests found
Pipeline #41752 passed
Stage: test
Show whitespace changes
Inline Side-by-side
notebooks/tests/pref.ipynb
+ 4
− 0
View file @ ae69755e
%% Cell type:code id: tags:
``` prob
:help :pref
```
%% Output
```
:pref [NAME ...]
// or
:pref NAME=VALUE [NAME=VALUE ...]
```
View or change the value of one or more preferences.
In the first form, the values of the given preferences are displayed (or all preferences, if no preference names are given). In the second form, the values of the given preferences are changed. The two forms cannot be mixed; it is not possible to view and change preferences in a single command.
Certain preference changes do not take full effect when performed on an already loaded machine. Such preferences must be set when the machine is loaded using the `::load` or `:load` command.
:pref [NAME ...]
// or
:pref NAME=VALUE [NAME=VALUE ...]
View or change the value of one or more preferences.
In the first form, the values of the given preferences are displayed (or all preferences, if no preference names are given). In the second form, the values of the given preferences are changed. The two forms cannot be mixed; it is not possible to view and change preferences in a single command.
Certain preference changes do not take full effect when performed on an already loaded machine. Such preferences must be set when the machine is loaded using the `::load` or `:load` command.
%% Cell type:markdown id: tags:
The values of all preferences can be viewed.
%% Cell type:code id: tags:
``` prob
:pref
```
%% Output
ALLOW_COMPLEX_LETS = false
ALLOW_INCOMPLETE_SETUP_CONSTANTS = false
ALLOW_LOCAL_OPERATION_CALLS = false
ALLOW_NEW_OPERATIONS_IN_REFINEMENT = false
ALLOW_OPERATION_CALLS_IN_EXPRESSIONS = false
ALLOW_OUTPUT_READING = false
ALLOW_SIMULTANEOUS_ASSIGNMENTS = false
ALLOW_UNTYPED_IDENTIFIERS = false
ALLOY_SCOPELESS_TRANSLATION = false
ALLOY_STRICT_INTEGERS = true
ALLOY_TRANSLATION_FOR_PROOF = false
ALLOY_USE_IMPLEMENTABLE_INTEGERS = false
ASSERT_CHECKING = true
ATELIERB_KRT_PATH = krt
BBRESULTS = false
BOOL_AS_PREDICATE = false
BUGLY = false
CHR = false
CLPFD = true
COMPILE_WHILE = true
COMPRESSION = false
CSE = false
CSE_PRED = true
CSE_SUBST = false
CSE_WD_ONLY = false
CSP_STRIP_SOURCE_LOC = false
DATA_VALIDATION = false
DEFAULT_SETSIZE = 2
DETECT_LAMBDAS = true
DISPROVER_MODE = false
DOT = /opt/local/bin/dot
DOT_ARC_COLORS = true
DOT_ARGUMENTS = true
DOT_COLOR_ARC = #006391
DOT_COLOR_NODE = #99BF38
DOT_COLOR_NODE_ERROR = #FF3800
DOT_COLOR_NODE_GOAL = orange
DOT_COLOR_NODE_OPEN = #F4E3C1
DOT_COLOUR_GOAL = true
DOT_CURRENT_NODE_SHAPE = doubleoctagon
DOT_DECOMPOSE_NODES = true
DOT_DEFINITIONS_SHOW_ALL = false
DOT_DEFINITIONS_USE_SUB_GRAPH = true
DOT_EDGE_FONT_SIZE = 12
DOT_EDGE_LABELS = true
DOT_EDGE_PEN_WIDTH = 1
DOT_ENGINE = dot
DOT_EVENT_HIERARCHY_EDGE_COL = #806040
DOT_EVENT_HIERARCHY_EXTENDS_COL = gray50
DOT_EVENT_HIERARCHY_GRD_KEEP_COL = #E0C080
DOT_EVENT_HIERARCHY_GRD_STRGTH_COL = gray83
DOT_EVENT_HIERARCHY_HORIZONTAL = true
DOT_EVENT_HIERARCHY_MCH_COL = gray95
DOT_EVENT_HIERARCHY_NEW_COL = #C06040
DOT_EVENT_HIERARCHY_REF_COL = #C0A060
DOT_EVENT_HIERARCHY_RENAME_COL = #E0E0A0
DOT_EVENT_HIERARCHY_RENAME_UNCHG_COL = #E0F0E0
DOT_EVENT_HIERARCHY_UNCHG_COL = gray92
DOT_EXPRESSION_NODE_SHAPE = record
DOT_FILL_NORMAL_NODES = false
DOT_FUNCTIONS = false
DOT_HORIZONTAL_LAYOUT = false
DOT_IDS = false
DOT_INFO = true
DOT_LIMIT_PAGE_SIZE = true
DOT_LOOPS = true
DOT_MACHINE_HIERARCHY_MAX_IDS = 0
DOT_NODE_FONT_SIZE = 12
DOT_NORMAL_NODE_SHAPE = box
DOT_PEN_WIDTH = 2
DOT_PREDICATE_NODE_SHAPE = rect
DOT_PROJECTION_DEF_COL = solid
DOT_PROJECTION_DET_COL = black
DOT_PROJECTION_LABEL_LIMIT = 75
DOT_PROJECTION_NON_DEF_COL = dashed
DOT_PROJECTION_NON_DET_COL = #806040
DOT_PROP = false
DOT_ROOT = true
DOT_ROOT_SHAPE = invtriangle
DOT_SCOPE_LIMIT_COL = gray
DOT_SHOW_OP_READ_WRITES = true
DOT_USE_CONSTANTS = true
DOT_USE_UNICODE = true
DOT_VARIABLE_MODIFICATION_HIDE_ONLY_WRITTEN = false
DOUBLE_EVALUATION = true
EDITOR = /usr/local/bin/bbedit
EDITOR_GUI = /Applications/BBEdit.app
ENUMERATE_INFINITE_TYPES = true
EXPAND_FORALL_UPTO = 100
FILTER_UNUSED = false
FORGET_STATE_SPACE = false
IGNORE_HASH_COLLISIONS = false
IGNORE_PRJ_TYPES = false
INTERNAL_ARGUMENT_PREFIX = $none
INVARIANT_CHECKING = true
JAVA_PATH = /usr/bin/java
JVM_PARSER_ARGS =
JVM_PARSER_HEAP_MB = 0
KODKOD = false
KODKOD_MAX_NR_SOLS = 22
KODKOD_ONLY_FULL = true
KODKOD_RAISE_WARNINGS = false
KODKOD_SAT_SOLVER = sat4j
KODKOD_SYMMETRY = 0
LATEX_ENCODING = auto
LATEX_GREEK_IDENTIFIERS = false
LIFT_EXISTS = false
LTSMIN = ./lib/
MAXINT = 3
MAX_DISPLAY_SET = 100
MAX_INITIALISATIONS = 4
MAX_OPERATIONS = 10
MC_DC_Level = 2
MEMO = false
MEMOIZE_FUNCTIONS = false
MINIMAL_TEST_SUITES = true
MININT = -1
NDJSON_ERROR_LOG_FILE =
NORMALIZE_AST = false
NUMBER_OF_ANIMATED_ABSTRACTIONS = 20
OPERATION_REUSE = false
OPTIMIZE_AST = true
PARTITION_PROPERTIES = true
PARTITION_PROPERTIES_INLINE = true
PERFORMANCE_INFO = false
PERFORMANCE_INFO_LIMIT = 100
PGE = off
PP_CS_STYLE_SEQUENCES = false
PP_FROZEN_INFOS = false
PP_SEQUENCES = false
PROB2_TRACE_FILE =
PROB2_TRACE_FILE_UNIQUE = false
PROOF_INFO = true
RAISE_ABORT_IMMEDIATELY = false
RANDOMISED_RESTART_INIT = false
RANDOMISE_ENUMERATION_ORDER = false
RANDOMISE_OPERATION_ORDER = false
REMOVE_IMPLIED_CONSTRAINTS = false
REPL_CACHE_PARSING = false
REPL_UNICODE = false
REQUIRE_OUTPUT_ASSIGNMENT = false
SAFETY_MODEL_CHECK = false
SAT_SUPPORTED_INTERPRETER = false
SHOW_EVENTB_ANY_VALUES = false
SMT = false
SMTLIB_BOOL_ARRAYS_TO_SETS = false
SMTLIB_PREPROCESS = false
SMT_SUPPORTED_INTERPRETER = false
SOLVER_STRENGTH = 0
STATIC_ORDERING = false
STATIC_SYMMETRY_DETECTION = true
STRICT_CLASH_CHECKING = false
STRICT_RAISE_ENUM_WARNINGS = false
STRICT_RAISE_WARNINGS = false
STRING_AS_SEQUENCE = true
SYMBOLIC = false
SYMBOLIC_MC_TRY_OTHER_SOLVERS = false
SYMMETRY_MODE = off
SYNTAX_HIGHLIGHT = true
TIME_OUT = 2500
TK_CUSTOM_STATE_VIEW_FONT_NAME =
TK_CUSTOM_STATE_VIEW_FONT_SIZE = 0
TK_CUSTOM_STATE_VIEW_PADDING = 0
TK_CUSTOM_STATE_VIEW_STRING_PADDING = 10
TK_CUSTOM_STATE_VIEW_VISIBLE = true
TLC_WORKERS = 2
TRACE_INFO = false
TRACE_UPON_ERROR = false
TRY_ATELIERB_PROVERS = false
TRY_FIND_ABORT = false
TYPE_CHECK_DEFINITIONS = false
USELESS_CODE_ELIMINATION = false
USE_IGNORE_PRAGMAS = false
USE_RECORD_CONSTRUCTION = true
USE_SCOPE_DEFINITION = true
WARN_IF_DEFINITION_HIDES_VARIABLE = true
XML_ENCODING = auto
%% Cell type:markdown id: tags:
The values of specific preferences can be viewed.
%% Cell type:code id: tags:
``` prob
:pref MININT MAXINT
```
%% Output
MININT = -1
MAXINT = 3
%% Cell type:code id: tags:
``` prob
MININT..MAXINT
```
%% Output
$\{-1,0,1,2,3\}$
{−1,0,1,2,3}
%% Cell type:markdown id: tags:
The values of preferences can be changed.
%% Cell type:code id: tags:
``` prob
:pref MININT=-5 MAXINT=5
```
%% Output
Preference changed: MININT = -5
Preference changed: MAXINT = 5
%% Cell type:code id: tags:
``` prob
:pref MININT MAXINT
```
%% Output
MININT = -5
MAXINT = 5
%% Cell type:code id: tags:
``` prob
MININT..MAXINT
```
%% Output
$\{-5,-4,-3,-2,-1,0,1,2,3,4,5\}$
{−5,−4,−3,−2,−1,0,1,2,3,4,5}
%% Cell type:markdown id: tags:
Preferences cannot be viewed and changed in one command.
%% Cell type:code id: tags:
``` prob
:pref MININT MAXINT=5
```
%% Output
:pref: Cannot view and change preferences in the same command (attempted to assign preference MAXINT=5)
%% Cell type:code id: tags:
``` prob
:pref MININT=-5 MAXINT
```
%% Output
:pref: Missing value for preference MAXINT
......
src/main/java/de/prob2/jupyter/commands/PrefCommand.java
+ 8
− 19
View file @ ae69755e
package de.prob2.jupyter.commands;
import java.util.ArrayList;
import java.util.Collections;
import java.util.List;
import java.util.Map;
import java.util.TreeMap;
import com.google.inject.Inject;
import de.prob.animator.command.ComposedCommand;
import de.prob.animator.command.GetCurrentPreferencesCommand;
import de.prob.animator.command.GetPreferenceCommand;
import de.prob.animator.command.SetPreferenceCommand;
import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
......@@ -67,10 +63,9 @@ public final class PrefCommand implements Command {
public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
final StringBuilder sb = new StringBuilder();
if (args.get(PREFS_PARAM).isEmpty()) {
final GetCurrentPreferencesCommand cmd = new GetCurrentPreferencesCommand();
this.animationSelector.getCurrentTrace().getStateSpace().execute(cmd);
final Map<String, String> preferences = this.animationSelector.getCurrentTrace().getStateSpace().getCurrentPreferences();
// TreeMap is used to sort the preferences by name.
new TreeMap<>(cmd.getPreferences()).forEach((k, v) -> {
new TreeMap<>(preferences).forEach((k, v) -> {
sb.append(k);
sb.append(" = ");
sb.append(v);
......@@ -79,29 +74,23 @@ public final class PrefCommand implements Command {
} else {
final List<String> prefsSplit = args.get(PREFS_PARAM);
if (prefsSplit.get(0).contains("=")) {
final List<SetPreferenceCommand> cmds = new ArrayList<>();
CommandUtils.parsePreferences(prefsSplit).forEach((pref, value) -> {
cmds.add(new SetPreferenceCommand(pref, value));
final Map<String, String> newPreferenceValues = CommandUtils.parsePreferences(prefsSplit);
this.animationSelector.getCurrentTrace().getStateSpace().changePreferences(newPreferenceValues);
newPreferenceValues.forEach((pref, value) -> {
sb.append("Preference changed: ");
sb.append(pref);
sb.append(" = ");
sb.append(value);
sb.append('\n');
});
this.animationSelector.getCurrentTrace().getStateSpace().execute(new ComposedCommand(cmds));
} else {
final List<GetPreferenceCommand> cmds = new ArrayList<>();
for (final String arg : prefsSplit) {
if (arg.contains("=")) {
throw new UserErrorException(String.format("Cannot view and change preferences in the same command (attempted to assign preference %s)", arg));
}
cmds.add(new GetPreferenceCommand(arg));
}
this.animationSelector.getCurrentTrace().getStateSpace().execute(new ComposedCommand(cmds));
for (final GetPreferenceCommand cmd : cmds) {
sb.append(cmd.getKey());
sb.append(arg);
sb.append(" = ");
sb.append(cmd.getValue());
sb.append(this.animationSelector.getCurrentTrace().getStateSpace().getCurrentPreference(arg));
sb.append('\n');
}
}
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment