VALUE and DESCRIPTION of 189 ProB PREFERENCES
PREFERENCE = CurrentValue(*) : Type ==> Description
ALLOW_COMPLEX_LETS = false : bool ==> Allow LET substitutions to directly use introduced identifiers (e.g., LET x,y BE x=4 & y=x*x IN ...)
ALLOW_INCOMPLETE_SETUP_CONSTANTS = false : bool ==> Allow ProB to proceed even if only part of the CONSTANTS have been found.
ALLOW_LOCAL_OPERATION_CALLS = false : bool ==> Allow to call (local) operations in same machine
ALLOW_NEW_OPERATIONS_IN_REFINEMENT = false : bool ==> Allow introduction of new operations in refinements (automatically set to TRUE for SYSTEM machines)
ALLOW_OPERATION_CALLS_IN_EXPRESSIONS = false : bool ==> Allow to call query operations in (some) expressions
ALLOW_OUTPUT_READING = false : bool ==> Allow B operations to read outputs; output values will be initialised to default value in animator.
ALLOW_REALS = default : dbool ==> Allow to use the REAL datatype
ALLOW_SIMULTANEOUS_ASSIGNMENTS = false : bool ==> Allow B operations to assign multiple times to same variable (ASM style)
ALLOW_UNTYPED_IDENTIFIERS = false : [true,false,true_with_string_type] ==> Allow UNTYPED identifiers (they will be assigned new deferred sets as type)
ALLOY_SCOPELESS_TRANSLATION = false : bool ==> Do not set any scopes when translating an Alloy model to B (useful for proof assistants).
ALLOY_STRICT_INTEGERS = true : bool ==> Only accept integers (i.e, singleton sets in Alloy) as arguments to integer operations. Otherwise, a well-definedness error is thrown.
ALLOY_TRANSLATION_FOR_PROOF = false : bool ==> Translate only a single command of an Alloy model to the B machine assertions section to enable generation of proof obligations in AtelierB.
ALLOY_USE_IMPLEMENTABLE_INTEGERS = false : bool ==> Use INT (minint..maxint) for the translation from Alloy to B.
ASSERT_CHECKING = true : bool ==> Check ASSERT statements while animating and model checking
ATELIERB_KRT_PATH = krt : path ==> Path to Atelier B Provers krt tool
BBRESULTS = false : bool ==> Show probcli errors using the BBEdit (11.6 or newer) bbresults command
BOOL_AS_PREDICATE = false : bool ==> Extended Predicate Syntax (allow p&q as syntactic sugar for (p=TRUE) & (q=TRUE), only possible in REPL and DEPRECATED)
BUGLY = false : bool ==> Scramble identifiers when pretty-printing (BUGLY)
CACHE_OPERATIONS = true : bool ==> Cache operations/events when -cache is activated
CBC_PROVIDE_EXPLANATIONS = false : bool ==> Provide explanations (unsat core,...) for some CBC commands
CHR = false : bool ==> Use CHR based solver. Should speed up detection of unsolvable predicates, but might slow down solving in general.
CLPFD = true : bool ==> Use CLP(FD) solver for B integers (restricts range to -2^28..2^28-1 on 32 bit machines)
COMPILE_WHILE = true : bool ==> Compile bodies of WHILE loops if variant large
COMPRESSION = false : bool ==> Use more aggressive COMPRESSION when storing states
CSE = false : bool ==> Enable CSE (Common Subexpression Elimination)
CSE_PRED = true : bool ==> Apply CSE (if enabled) also to predicates
CSE_SUBST = false : bool ==> Apply CSE (if enabled) also to substitutions (operation/event bodies) [EXPERIMENTAL]
CSE_WD_ONLY = false : bool ==> Apply CSE (if enabled) only to well-defined sub-formulas
CSP_STRIP_SOURCE_LOC = false : bool ==> Strip CSP source-location information (for RHS of processes, except for internal choice)
DATA_VALIDATION = false : bool ==> Assume everything can be computed without constraint solving.
DEFAULT_SETSIZE = 2 : nat ==> Size of unspecified deferred sets in SETS section
DETECT_LAMBDAS = true : bool ==> Detect set comprehensions which can be rewritten into lambdas.
DISPROVER_MODE = false : bool ==> Skip certain optimizations that effect soundness of proofs (for Rodin DISPROVER Plugin)
DOT = /usr/local/bin/dot : path ==> Path/Command for dot program (using "/" even on Windows. Try avoiding spaces in path)
DOT_ARC_COLORS = true : bool ==> Colour the arcs (disable for import in OmniGraffle)
DOT_ARGUMENTS = true : bool ==> Print Operation Arguments (when Edge Labels shown)
DOT_COLOR_ARC = #006391 : rgb_color ==> Colour for normal arcs
DOT_COLOR_NODE = #99BF38 : rgb_color ==> Colour for normal node
DOT_COLOR_NODE_ERROR = #FF3800 : rgb_color ==> Colour for invariant violation
DOT_COLOR_NODE_GOAL = orange : rgb_color ==> Colour for nodes satisfying the GOAL predicate
DOT_COLOR_NODE_OPEN = #F4E3C1 : rgb_color ==> Colour for open node (red,green,blue,gray,... or rgb hex #ff00ff) or adjacent to an open node if print leaves is off
DOT_COLOUR_GOAL = true : bool ==> Colour the nodes that satisfy the GOAL predicate
DOT_CURRENT_NODE_SHAPE = doubleoctagon : dot_shape ==> Shape for current node
DOT_DECOMPOSE_NODES = true : bool ==> Decompose sets and complex pairs into individual vertices
DOT_DEFINITIONS_SHOW_ALL = false : bool ==> Show all DEFINITIONS
DOT_DEFINITIONS_USE_SUB_GRAPH = true : bool ==> Show expression-, predicate-, substitution-DEFINITIONS as sub-graphs
DOT_EDGE_FONT_SIZE = 12 : nat1 ==> Font Size for Edge labels
DOT_EDGE_LABELS = true : bool ==> Show Edge Labels (Operation Names)
DOT_EDGE_PEN_WIDTH = 1 : nat ==> Pen width for edges
DOT_ENGINE = dot : [dot,neato,sfdp,fdp,twopi,circo] ==> Default layout engine used for dot (dot,neato,sfdp,fdp,twopi,circo)
DOT_EVENT_HIERARCHY_EDGE_COL = #806040 : rgb_color ==> Edge colour for refine relation
DOT_EVENT_HIERARCHY_EXTENDS_COL = gray50 : rgb_color ==> Edge colour for extends relation
DOT_EVENT_HIERARCHY_GRD_KEEP_COL = #E0C080 : rgb_color ==> Colour for events just changing an action (not renamed, keeping guard unchanged)
DOT_EVENT_HIERARCHY_GRD_STRGTH_COL = gray83 : rgb_color ==> Colour for events just adding a guard (not renamed, no actions added)
DOT_EVENT_HIERARCHY_HORIZONTAL = true : bool ==> Organize refinements horizontally
DOT_EVENT_HIERARCHY_MCH_COL = gray95 : rgb_color ==> Colour for machine event cluster
DOT_EVENT_HIERARCHY_NEW_COL = #C06040 : rgb_color ==> Colour for new events (not refining any event)
DOT_EVENT_HIERARCHY_REF_COL = #C0A060 : rgb_color ==> Colour for events refining themselves (i.e., not renamed and modifying guard or action)
DOT_EVENT_HIERARCHY_RENAME_COL = #E0E0A0 : rgb_color ==> Colour for renamed events (with change in guard or action)
DOT_EVENT_HIERARCHY_RENAME_UNCHG_COL = #E0F0E0 : rgb_color ==> Colour for renamed unchanged events
DOT_EVENT_HIERARCHY_UNCHG_COL = gray92 : rgb_color ==> Colour for unchanged events (not renamed, no guards or actions added)
DOT_EXPRESSION_NODE_SHAPE = record : dot_shape ==> Shape for expression nodes in formula trees
DOT_FILL_NORMAL_NODES = false : bool ==> Fill normal nodes with color
DOT_FUNCTIONS = false : bool ==> Print Functions (operations that return values w/o changing state)
DOT_HORIZONTAL_LAYOUT = false : bool ==> Use horizontal layout by default (does not affect all dot graphs)
DOT_IDS = false : bool ==> Print Node Identifiers
DOT_INFO = true : bool ==> Print Node information (values of variables)
DOT_LIMIT_PAGE_SIZE = true : bool ==> Limit page size by default (does not affect all dot graphs)
DOT_LOOPS = true : bool ==> Print Self-Loops
DOT_MACHINE_HIERARCHY_MAX_IDS = 0 : int ==> Max. number of identifiers shown in hierarchy view (-1 to show all)
DOT_NODE_FONT_SIZE = 12 : nat1 ==> Font Size for Node labels
DOT_NORMAL_NODE_SHAPE = box : dot_shape ==> Shape for normal node
DOT_PEN_WIDTH = 2 : nat ==> Pen width for nodes
DOT_PREDICATE_NODE_SHAPE = rect : dot_shape ==> Shape for predicate nodes in formula trees
DOT_PROJECTION_DEF_COL = solid : dot_line_style ==> Style for definite edges (solid,dashed,dotted,bold,invis)
DOT_PROJECTION_DET_COL = black : rgb_color ==> Edge colour for non-deterministic edges
DOT_PROJECTION_LABEL_LIMIT = 75 : nat ==> Max. nr of characters for node labels
DOT_PROJECTION_NON_DEF_COL = dashed : dot_line_style ==> Style for non-definite edges (solid,dashed,dotted,bold,invis)
DOT_PROJECTION_NON_DET_COL = #806040 : rgb_color ==> Edge colour for deterministic edges
DOT_PROP = false : bool ==> Show properties of statespace node (useful for CSP models)
DOT_ROOT = true : bool ==> Print Root Node
DOT_ROOT_SHAPE = invtriangle : dot_shape ==> Shape for root node (invtriangle,triangle, ellipse, box, diamond,...)
DOT_SCOPE_LIMIT_COL = gray : rgb_color ==> Colour for open, but uninteresting nodes (red,green,blue,gray,... or rgb hex #ff00ff)
DOT_SHOW_OP_READ_WRITES = true : bool ==> Show read/write info for enabling diagrams
DOT_USE_CONSTANTS = true : bool ==> Use constants for deferred set values if possible
DOT_USE_UNICODE = true : bool ==> Use Unicode symbols for values and formulas
DOT_VARIABLE_MODIFICATION_HIDE_ONLY_WRITTEN = false : bool ==> Hide variables which are only written and not read in any guard
DOUBLE_EVALUATION = true : bool ==> Evaluate PREDICATES positively and negatively when analysing
EDITOR = /usr/local/bin/bbedit : path ==> Path to external text editor for probcli (uses EDITOR environment variable by default)
EDITOR_GUI = /Applications/BBEdit.app : path ==> Path to external GUI text editor
ENUMERATE_INFINITE_TYPES = true : bool ==> Allow enumeration of infinite types
ENUMERATION_ORDER_ANALYSIS = true : bool ==> Perform enumeration order analysis within quantifiers, e.g., to detect identifiers that should not be enumerated
EXPAND_FORALL_UPTO = 100 : nat ==> When analysing predicates: max. domain size for expansion of forall
FILTER_UNUSED = false : bool ==> Filter out unused constants
FORGET_STATE_SPACE = false : bool ==> Do not remember state space (mainly useful in conjunction with IGNORE_HASH_COLLISIONS)
IGNORE_HASH_COLLISIONS = false : bool ==> Ignore Hash Collisions (if true not all states may be computed, visited states are not memorised !)
IGNORE_PRJ_TYPES = false : bool ==> Ignore types of prj1 and prj2 (i.e., prj1({1},{1})(2,3) is considered well-defined
INTERNAL_ARGUMENT_PREFIX = $none : string ==> Prefix of internal operation arguments (these are not included in test cases)
INVARIANT_CHECKING = true : bool ==> Check invariant while animating and model checking
JAVA_PATH = /usr/bin/java : path ==> Path to the "java" command (in case java is not found on the PATH)
JVM_PARSER_ARGS = : string ==> Additional arguments sent to the JVM for the Java parser (e.g., "-XX:+UseG1GC -Xss5m")
JVM_PARSER_HEAP_MB = 0 : nat ==> Heap size in MB for Java parser (-Xmx JVM option, 0 means default value)
KODKOD = false : bool ==> Apply translation to KODKOD on PROPERTIES when loading machines
KODKOD_MAX_NR_SOLS = 22 : nat1 ==> Maximum number of solutions computed and sent by KODKOD per batch.
KODKOD_ONLY_FULL = true : bool ==> Translate only complete components to KODKOD
KODKOD_RAISE_WARNINGS = false : bool ==> Raise WARNING when component or predicate cannot be translated to KODKOD
KODKOD_SAT_SOLVER = sat4j : [sat4j,minisat,lingeling,glucose] ==> SAT solver used for Kodkod (sat4j, minisat, lingeling, glucose)
KODKOD_SYMMETRY = 0 : nat ==> Symmetry level for Kodkod (0=off, 20=on), the higher this value, the more symmetries will be broken, you should probably only turn this on when MAX_INITIALISATIONS is set to 1
LATEX_ENCODING = auto : text_encoding ==> Encoding used for Latex processing with -latex (auto,ISO-8859-1,ISO-8859-2,UTF-8,UTF-16,...)
LATEX_GREEK_IDENTIFIERS = false : bool ==> Prety-print Greek identifiers (Sigma,...) in Latex mode
LIFT_EXISTS = false : bool ==> Lift existential quantifiers, i.e., treat existentially quantified variables like ordinary variables
LTL_SAFETY_MODEL_CHECK = true : bool ==> Recognise safety properties and check these using the safety property model checker (requires ltl2ba for more complex properties)
LTSMIN = ./lib/ : path ==> Path to LTSmin commands, such as prob2lts-sym for symbolic model checking (not available for Windows.)
MAXINT = 3 : nat1 ==> value of MAXINT, controls enumeration of integers and used to define NAT in classical B (2147483647 for 32 bit ints)
MAX_DISPLAY_SET = 100 : int ==> Max size for pretty-printing sets (-1 means no limit)
MAX_INITIALISATIONS = 4 : nat ==> Max Number of Initialisations and Constant-Setups Computed
MAX_OPERATIONS = 10 : nat ==> Max Number of Enablings per Operation Computed
MC_DC_Level = 2 : nat ==> Default Predicate Expansion Level for MC/DC Coverage Analyses (0=no expansion, 1=only top level connective expanded,...)
MEMO = false : bool ==> MEMOize expansions of set comprehensions and lambda abstractions.
MEMOIZE_FUNCTIONS = false : bool ==> MEMOIZE function applications of all functions defined in ABSTRACT_CONSTANTS (even if not marked with /*@desc memo */).
MINIMAL_TEST_SUITES = true : bool ==> Generate minimal suite of mcm testcases (and not one per event)
MININT = -1 : neg ==> value of MININT, controls enumeration of integers and used to define INT in classical B (-2147483648 for 32 bit ints)
NDJSON_ERROR_LOG_FILE = : path ==> File were all errors and warnings are logged (NDJSON format). Can be set to stderr or stdout.
NORMALIZE_AST = false : bool ==> Normalize AST before passing to ProB kernel (rewrites many B predicates into simpler form)
NUMBER_OF_ANIMATED_ABSTRACTIONS = 20 : nat ==> How many levels of refined models are animated by default
OPERATION_REUSE = false : xbool ==> Reuse previously computed operation effects in B/Event-B (false, true:local propagation, full:cache projected state space per operation)
OPTIMIZE_AST = true : bool ==> Optimize AST (Abstract Syntax Tree) before passing to ProB kernel (rewrites many B predicates into more efficient form)
PARTITION_PROPERTIES = true : bool ==> Partition predicates (PROPERTIES) into components
PARTITION_PROPERTIES_INLINE = true : bool ==> Inline equalities when partitioning into components
PERFORMANCE_INFO = false : bool ==> Provide performance monitoring information on the terminal/console.
PERFORMANCE_INFO_LIMIT = 100 : int ==> Limit in ms for printing warnings when expanding comprehension sets in performance monitoring mode.
PGE = off : [off,disabled,enabled,full,disabled2,enabled2,full2] ==> Use the Partial Guard Evaluation optimisation for the state space exploration of B models.
PP_CS_STYLE_SEQUENCES = false : bool ==> Print B sequences in theoretical CS style without separators.
PP_FROZEN_INFOS = false : bool ==> Print Prolog frozen goal infos for unbound variables
PP_SEQUENCES = false : bool ==> Print B relations as sequences when possible during pretty-printing.
PROB2_TRACE_FILE = : path ==> Path to file to store prob2_execute_custom_operation results for later replay
PROB2_TRACE_FILE_UNIQUE = false : bool ==> Make the file name for prob2_execute_custom_operation unique
PROB_LASTCHANGED_INFO = Mon Aug 23 11:25:24 2021 +0200 : string ==> Last change date of ProB source (read-only preference)
PROB_REVISION_INFO = 699cab6e6f76ea15eb9f25433c8da4bde1a1f326 : string ==> Git revision of ProB (read-only preference)
PROB_VERSION_INFO = 1.11.0-nightly : string ==> Version of ProB (read-only preference)
PROOF_INFO = true : bool ==> Use PROOF information to restrict invariant checking to affected clauses.
RAISE_ABORT_IMMEDIATELY = false : xbool ==> Raise potential well-definedness issues immediately (may lead to false spurious alarms, but can allow to better detect WD issues which lead to timeouts; possible values false,true,full)
RANDOMISED_RESTART_INIT = false : bool ==> Use Randomised Restart for Initialisation and Constant Setup (only makes sense if RANDOMISE_ENUMERATION_ORDER is set; for an operation OP use MAX_OPERATIONS_OP == -Nr)
RANDOMISE_ENUMERATION_ORDER = false : bool ==> Randomise enumeration of variables.
RANDOMISE_OPERATION_ORDER = false : bool ==> Randomise order of operations when computing successor states.
REMOVE_IMPLIED_CONSTRAINTS = false : bool ==> Remove unnecessary constraints implied by other constraints
REPL_CACHE_PARSING = false : bool ==> Cache parsing in REPL (useful if same formula gets parsed multiple times, e.g., for Latex processing)
REPL_UNICODE = false : bool ==> Use UNICODE in REPL and editing window
REQUIRE_OUTPUT_ASSIGNMENT = false : bool ==> Require operations to assign to all outputs
SAFETY_MODEL_CHECK = false : bool ==> Only store one incoming transition/operation per reached state. Can be used when model checking of safety properties (invariants, goal, assertions). Do not use for LTL model checking, deadlock checking or animation.
SAT_SUPPORTED_INTERPRETER = false : bool ==> Use Kodkod for specific predicates inside the B interpreter
SHOW_EVENTB_ANY_VALUES = false : bool ==> Show top-level ANY variable values of B Operations without parameters as parameters
SHOW_FORMULA_EXPLANATIONS = false : bool ==> Show explanation nodes in state view for certain formulas (e.g., <:, ...)
SHOW_FORMULA_FUNCTOR = -1 : int ==> Show prefix/infix operators in state view for formulas longer than (use -1 to disable feature):
SMT = false : bool ==> Enable SMT-Mode (aggressive treatment of : and /: inside predicates)
SMTLIB_BOOL_ARRAYS_TO_SETS = false : bool ==> Translate SMTLib boolean Arrays to B Sets (when processing .smt2 files)
SMTLIB_PREPROCESS = false : bool ==> Preprocess before solving SMTLib formulas (when processing .smt2 files)
SMT_SUPPORTED_INTERPRETER = false : bool ==> Use Z3 / CVC4 for predicates inside the B interpreter
SOLVER_STRENGTH = 0 : nat ==> Strength of certain Solver propagations (0 is default)
STATIC_ORDERING = false : bool ==> Use static ordering to enumerate constants which occur in most PROPERTIES first
STATIC_SYMMETRY_DETECTION = true : bool ==> Detect symmetries in forall/exists and in PROPERTIES for deferred sets
STRICT_CLASH_CHECKING = false : bool ==> Do a stricter checking for name CLASHES in B machines
STRICT_RAISE_ENUM_WARNINGS = false : bool ==> Treat ENUMERATION warnings (aka VIRTUAL TIME-OUTS) as errors (Warning: can generate spurious NOT-WELL-DEFINED messages).
STRICT_RAISE_WARNINGS = false : bool ==> Treat warnings as errors (Warning: can generate spurious NOT-WELL-DEFINED messages).
STRING_AS_SEQUENCE = true : bool ==> Allow sequence operators (^) to be applied to STRINGs
SYMBOLIC = false : bool ==> Lazy expansion of lambdas and set comprehensions
SYMBOLIC_MC_TRY_OTHER_SOLVERS = false : bool ==> Symbolic Model Checking: Try different solver / settings combinations
SYMMETRY_MODE = off : [off,flood,nauty,hash] ==> Symmetry Mode: off,flood,canon,nauty,hash
SYNTAX_HIGHLIGHT = true : bool ==> Enable Syntax Colour Highlighting
TIME_OUT = 2500 : nat1 ==> Time out for computing enabled transitions (in ms, is multiplied by a factor for other computations, value 2147483646 turns time outs off)
TK_CUSTOM_STATE_VIEW_FONT_NAME = : string ==> Font for animation strings (if empty, the editor font will be used)
TK_CUSTOM_STATE_VIEW_FONT_SIZE = 0 : nat ==> Font size for animation strings (if 0, the editor font size will be used)
TK_CUSTOM_STATE_VIEW_PADDING = 0 : nat ==> Padding (in pixels) between images of custom TK state viewer
TK_CUSTOM_STATE_VIEW_STRING_PADDING = 10 : nat ==> Padding (in pixels) between strings of custom TK state viewer
TK_CUSTOM_STATE_VIEW_VISIBLE = true : bool ==> Use custom Tk viewer to represent state of B Machine
TLC_WORKERS = 2 : nat1 ==> Number of parallel workers for external tool TLC (for -workers option)
TRACE_INFO = false : bool ==> Provide various tracing information on the terminal/console.
TRACE_UPON_ERROR = false : bool ==> Trace upon error (requires running from source)
TRY_ATELIERB_PROVERS = false : bool ==> Try Atelier B Provers for unknown SMTLIB specifications
TRY_FIND_ABORT = false : xbool ==> Try more aggressively to detect not well-defined expressions (e.g. applying function outside of domain), may slow down animator; possible values false,true,full
TYPE_CHECK_DEFINITIONS = false : bool ==> Type check all visible DEFINITIONs (not just used ones)
USELESS_CODE_ELIMINATION = false : bool ==> Useless Code Elimination: try and find useless statements which have no influence on the result of an operation.
USE_IGNORE_PRAGMAS = false : bool ==> Use /*@desc prob-ignore */ pragmas when checking predicates (PROPERTIES,...)
USE_RECORD_CONSTRUCTION = true : bool ==> Records: Check if axioms/properties describe a record pattern
USE_SCOPE_DEFINITION = true : bool ==> Use SCOPE predicate (if defined) to restrict state space exploration for model checking and animation.
WARN_IF_DEFINITION_HIDES_VARIABLE = true : bool ==> Warn if a DEFINITION hides a variable with the same name
WD_ANALYSIS_FOR_ANIMATION = true : bool ==> Perform the WD analysis in the context of ProB animation (e.g., deferred sets considered finite)
WD_IGNORE_EXTERNAL = false : bool ==> Generate (unprovable) WD PO for external functions with WD condition
XML_ENCODING = auto : text_encoding ==> Encoding used for XML processing, e.g., with -logxml (auto,ISO-8859-1,ISO-8859-2,UTF-8,UTF-16,...)
DESCRIPTION of ProB PREFERENCE GROUPS:
* PREFERENCE GROUP integer : SETTINGS [int32,int8] : Values for MAXINT and MININT
* PREFERENCE GROUP time_out : SETTINGS [disable_time_out] : To disable TIME_OUT
* PREFERENCE GROUP model_check : SETTINGS [disable_max,unlimited] : Model Checking Limits
* PREFERENCE GROUP dot_colors : SETTINGS [classic,dreams,winter] : Colours for Dot graphs
Set NO_COLOR environment variable to disable terminal colors