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

Refactor preference parsing into a common utility method

parent abbcace7
No related branches found
No related tags found
No related merge requests found
%% Cell type:code id: tags:
``` prob
:help :pref
```
%% Output
:pref [NAME ...]
:pref NAME=VALUE [NAME=VALUE ...]
View or change the value of one or more preferences.
%% 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_SIMULTANEOUS_ASSIGNMENTS = false
ALLOW_UNTYPED_IDENTIFIERS = false
ATELIERB_KRT_PATH = krt
BBRESULTS = false
BOOL_AS_PREDICATE = false
BUGLY = false
CHR = false
CLPFD = 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 = false
DISPROVER_MODE = false
DOT = dot
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_EDGE_LABELS = true
DOT_FUNCTIONS = false
DOT_IDS = false
DOT_INFO = true
DOT_LOOPS = true
DOT_PEN_WIDTH = 2
DOT_PROP = false
DOT_ROOT = true
DOT_SHOW_OP_READ_WRITES = true
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
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
LTSMIN = ./lib/
MAXINT = 3
MAX_DISPLAY_SET = 100
MAX_INITIALISATIONS = 4
MAX_OPERATIONS = 10
MEMO = 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
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
RANDOMISE_ENUMERATION_ORDER = false
RANDOMISE_OPERATION_ORDER = false
REMOVE_IMPLIED_CONSTRAINTS = false
REPL_CACHE_PARSING = false
REPL_UNICODE = false
REQUIRE_OUTPUT_ASSIGNMENT = false
SFDP = sfdp
SHOW_EVENTB_ANY_VALUES = false
SHOW_FULL_ERROR_LOCATIONS = true
SMT = 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
TIME_OUT = 2500
TK_CUSTOM_STATE_VIEW_PADDING = 0
TLC_WORKERS = 2
TRACE_INFO = false
TRACE_UPON_ERROR = false
TRY_ATELIERB_PROVERS = false
TRY_FIND_ABORT = false
TYPE_CHECK_DEFINITIONS = false
USE_RECORD_CONSTRUCTION = true
WARN_IF_DEFINITION_HIDES_VARIABLE = true
WARN_WHEN_EXPANDING_INFINITE_CLOSURES = 5
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}
%% 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}
%% 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: Cannot view and change preferences in the same command (missing value for preference "MAXINT")
:pref: Missing value for preference MAXINT
......
......@@ -2,7 +2,9 @@ package de.prob2.jupyter.commands;
import java.util.Arrays;
import java.util.Collections;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import org.jetbrains.annotations.NotNull;
......@@ -15,4 +17,16 @@ public final class CommandUtils {
return Arrays.asList(split);
}
}
public static @NotNull Map<@NotNull String, @NotNull String> parsePreferences(final @NotNull String name, final @NotNull List<@NotNull String> args) {
final Map<String, String> preferences = new HashMap<>();
for (final String arg : args) {
final String[] split = arg.split("=", 2);
if (split.length == 1) {
throw new CommandExecutionException(name, "Missing value for preference " + split[0]);
}
preferences.put(split[0], split[1]);
}
return preferences;
}
}
package de.prob2.jupyter.commands;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
......@@ -38,14 +37,7 @@ public final class LoadCellCommand implements CellCommand {
@Override
public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String name, final @NotNull String argString, final @NotNull String body) {
final List<String> args = CommandUtils.splitArgs(argString);
final Map<String, String> preferences = new HashMap<>();
for (final String arg : args) {
final String[] split = arg.split("=", 2);
if (split.length == 1) {
throw new CommandExecutionException(name, "Missing value for preference " + split[0]);
}
preferences.put(split[0], split[1]);
}
final Map<String, String> preferences = CommandUtils.parsePreferences(name, args);
kernel.setTrace(new Trace(this.classicalBFactory.create(body).load(preferences)));
return new DisplayData("Loaded machine: " + kernel.getTrace().getModel());
......
package de.prob2.jupyter.commands;
import java.io.IOException;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
......@@ -45,15 +44,7 @@ public final class LoadFileCommand implements LineCommand {
}
final String fileName = args.get(0);
final List<String> prefArgs = args.subList(1, args.size());
final Map<String, String> preferences = new HashMap<>();
for (final String arg : prefArgs) {
final String[] split = arg.split("=", 2);
if (split.length == 1) {
throw new CommandExecutionException(name, "Missing value for preference " + split[0]);
}
preferences.put(split[0], split[1]);
}
final Map<String, String> preferences = CommandUtils.parsePreferences(name, args.subList(1, args.size()));
try {
kernel.setTrace(new Trace(this.classicalBFactory.extract(fileName).load(preferences)));
......
......@@ -49,21 +49,14 @@ public final class PrefCommand implements LineCommand {
});
} else if (args.get(0).contains("=")) {
final List<SetPreferenceCommand> cmds = new ArrayList<>();
for (final String arg : args) {
final String[] split = arg.split("=", 2);
if (split.length == 1) {
throw new CommandExecutionException(name, String.format("Cannot view and change preferences in the same command (missing value for preference %s)", split[0]));
}
assert split.length == 2;
final String pref = split[0];
final String value = split[1];
CommandUtils.parsePreferences(name, args).forEach((pref, value) -> {
cmds.add(new SetPreferenceCommand(pref, value));
sb.append("Preference changed: ");
sb.append(pref);
sb.append(" = ");
sb.append(value);
sb.append('\n');
}
});
kernel.getTrace().getStateSpace().execute(new ComposedCommand(cmds));
} else {
final List<GetPreferenceCommand> cmds = new ArrayList<>();
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment