Glossary:Advanced Preferences: Difference between revisions

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