Full ProB release history:
RELEASE HISTORY
===============
20.2.2024 1.13.0
- superset and contains_element Unicode symbols can be used within B expressions
- support for template strings surrounded by triple backquotes, expressions in template marked by ${.} or $«.»
```1+1=${1+1}``` is equivalent to "1+1="^TO_STRING(1+1) and evaluates to "1+1=2"
(currently curly braces are disallowed inside template expression)
- export of comments for events, invariants, axioms and theorems from ProB for Rodin as description pragmas
- operations can be annotated with a description pragma at the end (/*@ desc "..." */),
descriptions are visible in hovers/context menus of the state view and in VisB HTML trace exports;
for Event-B models these descriptions can be placed in the comment field of an event
- new preference SOLVER_FOR_PROPERTIES to specify solver for PROPERTIES (axioms) when setting up constants,
can be set to prob (the default), kodkod, z3, z3cns, z3axm, cdclt, sat, sat-z3
- dot visualisations (-dot last_error FILE) for some Event-B state errors during multi-level refinement
- new variable refinement hierarchy diagram for Event-B models (e.g., probcli -dot variable_hierarchy FILE)
- new external functions SIGN and LCM (least common multiple) in LibraryMath.def,
and improved constraint solving for ABS, GCD, LCM and SIGN.
- Monte Carlo Tree Search (MCTS) available for specifications which define GAME_OVER, GAME_PLAYER,
GAME_VALUE definitions. MCTS tree can be visualised graphically.
MCTS commands are available by right-clicking in Tk operations view.
MCTS_AUTO_PLAY and RANDOM_ANIMATE are available as special event names for VisB.
- new external function READ_JSON in LibraryXML.def to readin JSON files in same format as READ_XML
- Tcl/Tk editor performs Latex (\cup,....) to Unicode conversions upon space or control-space
and code completion (also for Latex commands above) tab,
ProB2-UI editor does completion upon control-space
- projection diagram for expression merges multiple edges into one and takes DOT_LOOPS into account
- VisB: support use element and improve error messages and location, support use SVG element
and the generation of groups in VISB_SVG_OBJECTS, VISB_SVG_OBJECTS can now also
have fields with dynamic values (i.e., no separate VISB_SVG_UPDATES definition is required)
and event and predicate fields (i.e., no separate VISB_SVG_EVENT definition is required)
- Rodin theory support improvements: allow real literals and B formulas (between $) in ptm files,
check WD of operators (if TRY_FIND_ABORT is true), improved event error feedback,
support recursive inductive datatypes including recursive operators,
automatic lambda insertion if operator takes no arguments,
allow to use theory operators in REPL, VisB, trace replay files,etc.,
improved feedback for operators in state view
- small improvements in event refinement diagram, tooltips for ProB2-UI
- experimental setlog integration in REPL (:slog Formula) and disprover
- ADD_WARNINGS external function
- detect Alloy scalars and TLA2B partial records in VisB
- small performance improvement in B parser
- support Unicode oftype operator (0x2982)
3.2.2024 1.12.2-fix1 (1.12.3)
- fix issues with reification of predicates and predicate reuse for LET predicates and exists,
fix issue with STRING_JOIN, fix symbolic subset counter-example argument reversal
10.8.2023 1.12.2
- performance improvements in B parser
- experimental access to glucose satsolver backend in probcli REPL via :sat PRED
- reification of REAL comparison operators in ProB kernel
- new external function STORE(id) and predicate STORE_VALUE("name",Val) in LibraryMeta.def
to store values inside predicates; counterpart to :let ID=Expr in REPL, but for predicate solutions;
these temporary let values are now available within a wider range of commands (table and dot
commands in probcli or in Jupyter for example)
- new PROB_SAFE_MODE preference to force additional sanity checks
- new (hidden) preference optimize_enum_set_elems so that large sets using enumerated set elements
can be more efficiently type checked and pre-compiled (will in future happen automatically)
- ProB's AVL set representation of sets can now also be used for efficient (logarithmic)
member checks based on the first field of a record, such as f:1 in rec(f:1,g:y).
Previously this was only available for fully known elements or the first part of a pair.
- VISB_SVG_EVENTS definitions can specify event with a predicate to be triggered by a click
- VISB_SVG_FILE DEFINITION can be used to specify an SVG file and an empty JSON file
(all objects and updates should then be created by VisB DEFINITIONS)
- VisB items in JSON file can now group multiple SVG attributes in a single
record: instead of "name":"fill", "value":"BFormula" you can write "fill":"BFormula"
- new preference JAVA_PARSER_PATH to replace -parsercp probcli command; it can
now also point to a compiled version of the parser (cliparser) obtained by Graal VM
- new preference for Event-B models (NUMBER_OF_SKIPPED_REFINEMENTS) which enables
to start animation at higher refinement levels
- make failures refinement checking available for B models;
new probcli command: -ref_check MODE File with MODE being T, F, ...
- stricter checking of VISB SVG attributes
- ensure LET simplification rules do not create slow-downs
- improve image/function application of iterate(f,k) for symbolic functions f
- READ_XML(File,"auto") external function tries to use XML header to detect encoding
- new external function STRING_TO_REAL in LibraryStrings.def
- new external function ADD_STATE_ERROR, which stores error for current B state
- CUSTOM_GRAPH_EDGES now supports more dot edge attributes (like arrowhead, dir),
new CUSTOM_GRAPH definition where we can set global dot graph attributes,
specify directed and strict attributes and provide nodes and edges
(i.e., one can specify a dot graph rendering in a single B expression,
this format can also be used for -dotexpr expr_as_graph E probcli command or in Tcl/Tk)
- pretty print Event-B style set comprehensions properly (e.g., {x·x ∈ 1 ‥ 3|x * 10})
30.4.2023 1.12.1
- allow prj1/prj2 to be applied without type arguments, e.g., writing
prj2(prj1(1|->2|->3)) instead of prj2(INTEGER,INTEGER)(prj1(INTEGER*INTEGER,INTEGER)(1|->2|->3))
- allow to use Event-B style set comprehensions with expression terms
e.g., {x·x:1..10|x*x} = {1,4,9,16,25,36,49,64,81,100}
Note: due to conflicts with composed identifiers you cannot use the regular dot, but
have to use the middle dot (·, ASCII code 183 i.e. 0xb7) or the Unicode dot (0x22c5)
- improved enumeration in ProB kernel: separate waitflags for choice points with
exactly same priority
- performance improvements in kernel for image and function application of iterate operator,
fix in reification of cardinality closure and improve reification of subset for infinite sets
- improved treatment of well-definedness: WD conditions for iterate, exponentiation (**) for reals,
avoiding spurious WD errors in predicate components and real operators (such as RSQRT, RPOW)
- VisB DEFINITIONS can set viewBox and also accept SVG objects represented as functions STRING +-> STRING,
VisB SVG objects are only added when they do not already exist in the SVG image
- CUSTOM_GRAPH_NODES DEFINITIONS can now use records with many more GraphViz attributes like
fontcolor, height, URL, xlabel in addition to color, shape, style and label.
It is also possible to use single records or partial functions using
strings like {"label"|->"x","shape"|->"rect",...} for nodes.
- StartProB.sh script tries to guess correct Tcl/Tk location on macOS
4.4.2023 1.12.0
- support for infinite deferred sets, when PROPERTIES (axioms) contain
predicates of the form not(s:FIN(s)) or not(finite(s))
- no more spurious WD errors inside set comprehensions or quantifiers
- VisB declarations can be written as B DEFINITIONS rather than in the JSON
file via: VISB_SVG_OBJECTS, VISB_SVG_UPDATES, VISB_SVG_HOVERS, VISB_SVG_BOX,
VISB_SVG_CONTENTS definitions, automatic conversion of sequence of pairs
for points attribute
- min and max operators can be applied to finite sets of reals, also available
as new external functions RIMINIMUM and RMAXIMUM
- Tk Random Animate... dialog has options to try and explore new states and to
minimize out degree and HEURISTIC_FUNCTION
- LTL formulas defined via ASSERT_LTL can now be inspected in the evaluation view
of ProB Tcl/Tk and the state view of ProB2-UI
- the -timeout switch to probcli has been renamed to -global-time-out to avoid
confusion with the TIME_OUT preference
- Tcl/Tk animator presents (orange) list of candidate enabled operations when
MAX_OPERATIONS is set to 0; double clicking on the items opens the execute by predicate dialog
- Allow multiple inclusion of B enumerated and deferred sets and constants, no longer leading
to errors and warnings (cf ticket PROB-403).
Multiple inclusions are also allowed via REFINES (and not just SEES, INCLUDES, ...).
- new external functions NON_DET_OUTPUT_STATE, NON_DET_OUTPUT_OPERATIONS, GET_IS_DET_OUTPUT to check
whether operations have non-deterministic outputs
- new external predicate ENABLED_TRANSITION, a variation of ENABLED with arguments provided
- new :open FILE command in REPL
- bug fix in LTL safety model checker's cycle detection
- VisB can support enable, disable items, triggered when specified events are enabled or disabled
- improve Event-B theory support, AUTO_DETECT_THEORY_MAPPING preference so that standard Rodin
theories work without .ptm mapping file; support for simple Sigma/Pi operators on sets of values,
support for Real/Float theories,
Rodin ProB plugin can display strings and reals
- new external function REAL_DEC_TO_STRING, RADIANS, DEGREE
- allow operation calls without arguments in expressions (when ALLOW_OPERATION_CALLS_IN_EXPRESSIONS
is set) and fix issues when both ALLOW_OPERATION_CALLS_IN_EXPRESSIONS and
ALLOW_LOCAL_OPERATION_CALLS were set to TRUE
- enable to inspect instantiation patterns using -prob_profile after using external function observe
- @PROPERTIES and @INVARIANT can be used in REPL, new :check-ast command for developers
- new -properties_core probcli command to try and quickly find a small unsat core
- -ltlfile probcli command now accepts Rodin and Tcl/Tk format
- -lint command also checks specified VISB_JSON_FILE
- improvements in before-after predicate computation in symbolic model checker
- improve operation caching performance for machines with large number of operations
- improvements and fix of one faulty proof rule in WD prover
- :prob-file and :z3-file REPL commands can load ProB Prolog AST files
- solved performance issue for very large values in existential quantifier
- new dot command (-dotexpr id_value_formula_tree ID FILE) to visualise the
value of a constant or variable, useful for symbolic values;
- dot and -dotexpr automatically convert from dot to pdf, svg, png, ...
if specified file has the corresponding ending
- performance improvements in Java B parser
- support for new binary format for .prob files
by setting jvm_parser_fastrw preference to true
- VisB JSON files can now contain svg_objects list, containing SVG objects
that are added to the SVG file.
For/repeat loops can be applied to the objects for flexible creation of new objects.
The bound expression for loops and for created object attributes can now also depend
on constants, as long as they are set up and there is a single constants valuation.
Also, if no SVG file is provided, a default empty one is generated.
You can provide a svg_box attribute with height and width for this empty SVG.
It is also possible to associate multiple events with the same SVG id.
- ProB Tcl/Tk can directly open .prob files
- new -bench_csv_append FILE and bench_model_check Repitions options for probcli
for benchmarking usage
- support for new LTL transition operators: unchanged, changed, increasing, decreasing, BA
for example "G( changed({x}) => [Event])" or "G([Event] => decreasing({x*2+y}))"
- LTL counter example lassos shortened if possible
- added -csv CMD FILE and -csvexpr CMD EXPR FILE probcli table commands,
for example probcli B.mch -csv min_max_table out.csv
- improve type checking performance for certain large set extensions
- keep track of call stack in B models, e.g., for WD errors,
call stack currently contains called operations, memoised function calls,
quantifiers (universal, existential and set comprehensions) and external function calls.
When TRACE_INFO is set then also function calls are registered and other checks
like total or partial function checks.
- improvements in B kernel: symbolic treatment of relational composition membership, ...
- new -parserport PortNr command to start Java parser separately from probcli
(for debugging purposes)
- new jvm_parser_force_parsing preference to force parsing even if .prob file is up-to-date
- improved support for VALUES clause
- new regular expression external functions to ignore case: REGEX_IMATCH, REGEX_ISEARCH, ...
- new probcli command -check_lib to check the contents of ProB's lib folder
- new probcli install EXT command with EXT=ltsmin or EXT=ltl2ba
to download and install additional extensions into ProB's lib folder
- new commands for CDCL(T) solver (previously called DPLL(T))
:cdclt (previously called :dpllt)
:cdclt-free (ignore values for variables in current state)
29.12.2021: 1.11.1
- the ProB parser supports identifiers between backquotes. This can be used for example
to use identifiers which correspond to keywords (e.g., `front` = 10).
This is useful for Event-B, TLA or Z models, which have other keywords than B
and other rules for valid identifiers.
The parser also supports the Unicode forward composition operator from Event-B.
Stack usage has also been reduced.
- new intelligent JSON trace replay; ProB2 JSON trace format is now used
by default in ProB Tcl/Tk as well. The JSON format stores much more
information, allow more precise replay.
- improvements in equality comparison of infinite symbolic values
(e.g., via alpha conversion for quantifiers)
- breadth-first model checking (e.g., -bf option in probcli) keeps track of the
levels (distance from root) during model checking;
by using e.g. -bf -scope 'PROB_STATISTICS("bf-level")<10' in probcli
one can restrict the maximal depth of model checking
- new external functions NON_DET_STATE and GET_IS_DET("OpName") which can be used
to find non-deterministic states/operations in the state space (it can be used
in the GOAL predicate for model checking)
- SAFETY_MODEL_CHECK now adds at least one transition per covered optartion
and performance improvement for skip operations
- VisB: constant B expressions can now be used in for loops, added override attribute
- new external function INT_TO_ENUM, useful for iterations over deferred sets in VisB
- Variable values can be changed explicitly by user in Tcl/Tk Evaluation View
(using right click and choosing "Modify Value...")
- improvements in Z3 interface (quantifier instantiation, performance of preprocessing, ...)
- new z3 commands in REPL:
:z3-cns (constructive translation only), :z3-axm (axiomatic translation only),
:z3-core, :z3-cns-core, :z3-axm-core (compute unsat core),
:z3-free (ignore values for variables in current state)
- DPLLT solving algorithm available in REPL via :dpllt command
6.10.2021: 1.11.0
- ability to expand comprehension sets and lambdas in the various evaluation/state views
(Tk, ProB2-UI, Rodin)
- replay ProB2-UI JSON traces in probcli using -trace_replay json FILE or -det_trace_replay json FILE
- generate HTML VisB visualisations for the history using -visb VisBFILE HTMLFILE in probcli
- generate HTML VisB visualisations for history or current state in Tcl/Tk
- other VisB improvements: jquery is no longer required, ENABLED external function works, ...
- allow to use a DEFINITION to define enumerated set elements (e.g., SETS E == D DEFINITIONS D=={d1,d2})
- new external function STRING_REPLACE
- static keyword clash checking for Z, ... models
- improved error location feedback for Rodin models
- improved symbolic treatment of various subset and partial/total function/surjection checks
- TLA2B accepts FALSE as action
- improved constraint solving (register_predicate for non-WD predicates,
improved symbolic treatment of infinite sets,
improved reification of partial/total/surjective function and subset tests, non-empty-set attribute, ...)
- improved model checking performance, in particular for OPERATION_REUSE full:
invariants are also cached, improved hashing, new -op-cache-statistics command to inspect caching statistics
- reduced memory consumption during model checking with COMPRESSION for total function values
(e.g., bit vector values like {a|->TRUE, b|->FALSE})
- new preference JVM_PARSER_POSITION_INFOS which can be used to turn off position informations
in the generated .prob file (to reduce memory consumption)
- more compact position representation in abstract syntax tree, reducing runtime and memory
required to load .prob files for very large B machines
- extended LTL syntax (<=> and textual versions of operators:
and, implies, globally, finally, until, weakuntil, release, since, trigger, historically, once, yesterday, ...),
LTL formulas can access B DEFINITIONS,
and improved detection of simple LTL safety properties with improved performance
(ProB will no longer try to find a cycle after detecting a safety violation)
- command to find longest path in state space
(in Tk: Animate -> Find Existing State -> State with Longest Distance from Root)
- probcli command for repeated executions -execute-repeat Steps RepNr
(performs described number of execution Steps from root state RepNr times)
- detect keyword clashes and improved extended static checking (-lint probcli command):
detect obvious WD errors in symbolic values
- new Z3 (more constructive) translation running in parallel to old Z3 translation
21.1.2021: 1.10.2
- remove debug print
20.1.2021: 1.10.1
- improved symbolic treatment of partial and total function checks and domain/range
restriction/subtraction for infinite relations,
- automatic detection of sequence types encoded as {s|#n.(n:NATURAL & s:1..n->Type)}
- LibrarySVG.def external functions for VisB visualisations
15.12.2020: 1.10.0
- support Atelier-B real literals, REAL, floor, ceiling and real functions (can be turned off
with ALLOW_REALS preference)
- new external function library stdlib/LibraryReals.def containing RSIN, RCOS, RABS, RSQRT, ...
- some external functions from LibraryStrings, LibraryReals, LibraryMath are now automatically
available in the probcli and ProB Tcl/Tk REPL
- adapt WD-conditions for exponentiation in Event-B: negative base now raises WD error
- fix Z3 translation to work with Z3 4.8.8 and 4.8.9, support Z3 models with lambda
- add -no_state_errors flag for model checking in probcli and "Find Other Errors" flag
in ProB Tcl/Tk to allow to ignore state errors and general errors during model checking
(i.e., errors related to transitions, ASSERT statements, well-definedness, etc.)
- new ASSERT_CHECKING preference where one can disable checking ASSERT statements
- dot visualization for operation call graph of B machines
- static analysis of well-definedness: generate WD proof obligations, try and discharge them
and visualise non-discharged source locations in ProB Tcl/Tk,
for probcli: -well_definedness_check command;
- improved disprover for Rodin, making use of WD prover for certain POs
- new -lint command in probcli and ProB Tcl/Tk to perform additional static checks;
useful for Atom or VSCode integration
- ProB Disprover now makes use of new rule-based prover (optimised for WD proof obligations)
- improvements to CUSTOM_GRAPH_EDGES and CUSTOM_GRAPH_NODES: can use record which defines
default dot attributes like color, shape, style and description, e.g.,
CUSTOM_GRAPH_EDGES1 == rec(color:"red", style:"dotted", edges:Expression)
- new external functions for sequences (REPLACE) and strings (STRING_PADLEFT, STRING_IS_DECIMAL,
STRING_IS_ALPHANUMERIC, STRING_EQUAL_CASE_INSENSITIVE)
- new commands in probcli REPL: :reset to reset animator (without reloading),
:files to show files of machine, :machine to show machine stats.
- allow assigning to record fields (e.g., x'Field := E or x'F1'F2 := E)
- one can load DEFINITION files (.def) directly with probcli or ProB Tcl/Tk
- improved unsat core computation, :min-core command in REPL
- improved parser error messages for a few new common errors, allow description pragmas
for enumerated set elements
- invariant coverage table command to visualise which invariants are violated where in the state space
- improvements in Tk evaluation view: show top-level operator and only show operator
when expanding non-topmost formulas
- improved variable capture checking for DEFINITIONS
19.2.2020: 1.9.3
- improvements in kernel (reification of partial function, total_function, partial_surjection)
- the sequence operators size and rev can now be applied to STRINGS and conc to sequence of STRINGS
(unless STRING_AS_SEQUENCE preference is FALSE)
- new external functions STRING_TO_UPPER and STRING_TO_LOWER in LibraryStrings.def
- LibraryRegex no longer adapts character ranges according to locale
- add -execute_monitor to detect disabled operations which consume a lot of time during -execute
- use static read/write analysis to improve performance of -execute (avoid trying out
operations which are guaranteed not to be enabled)
- DO_NOT_ENUMERATE external function available
- preference JVM_PARSER_ARGS to pass additional JVM arguments for launching the parser
- detection of lambda expressions on by default (DETECT_LAMBDAS preference),
new enumeration order analysis which detects variables which should not be enumerated
because they are derived from other variables
- :abstract_constants command in probcli -repl
- :min Pred and :max Pred command in probcli -repl and ProB Tcl/Tk Eval Console to find a minimal respectively
maximal model for predicate Pred or function %(x,...).(Pred|OptimizingExpr)
- probcli releases memory after loading a file, when no other files are to be loaded and no memory intensive
tasks are asked for (--model-check).
Releasing memory can be forced with the -release_java_parser flag or in the probcli -repl using :trim.
- expansion times of comprehension sets can be monitored using preferences
PERFORMANCE_INFO and PERFORMANCE_INFO_LIMIT
- more precise source location feedback in some cases for errors, time outs and enumeration warnings
- new external function NORMAL for Gaussian distribution in LibraryRandom.def
11.11.2019: 1.9.2
- maintenance release for issue in the pretty printer
8.11.2019: 1.9.1
- add -release_java_parser command for probcli to reduce memory consumption for very large
B machines
- add constraint-based dynamic assertion check (called invariant theorem checking for Event-B/Rodin)
- improve pretty-printing formulas in particular in Event-B mode (use proper Event-B syntax for
lambda, quantification, prj1/2,...), useful for ProB for Rodin state view.
Complex invariants are printed in nested fashion.
- visualise states using Latex template
- improvements in kernel: cardinality stored as Prolog attribute
- improvements to Alloy2B translation
12.7.2019: 1.9.0
- allow btrue, bfalse and Unicode versions thereof (0x22A4,0x22A5) as predicates,
allow identifiers with Unicode letters and with Unicode subscripts and primes at end
- new external functions (stdlib/LibraryRegex.def) for matching, searching and replacing using
regular expressions
- new external function: BITS, STRINGIFY, INT_TO_HEX_STRING, SHA_HASH_HEX,
SUB_STRING
- allow ELSIF branches for expressions
- size, ^, ->, <- do some well-definedness checks if TRY_FIND_ABORT is TRUE
- operations view shows non-deterministically set variables also for
subsidiary called operations
- improve setting JAVA_PATH preference on Macs
- performance improvements in kernel: intersection, STRING_JOIN,
faster posting of CLPFD constraints, ...
- allow to refocus Tcl/Tk animator on current state, for targeted model checking
- model checking SCOPE predicate can be turned off using USE_SCOPE_DEFINITION
- show description pragmas (/*@desc "..." */) when right-clicking in
Tcl/Tk state view
- memoization of functions is possible using the /*@desc memo */ pragma in the ABSTRACT_CONSTANTS section
or setting the preference MEMOIZE_FUNCTIONS to TRUE
- allow Unicode to be used in projection diagrams, use Unicode by default
in dot formula visualisation and ProB Tcl/Tk evaluation view
- dot formula visualization improved (expand set comprehensions, ...)
- new table diagram showing variables written and read in guards
- find valid state command can now use current constant values
- the -timeout probcli option is now also applied to the -execute commands
- more support for Atelier-B Event-B machines: copying variables and invariants
from abstraction to refinement if possible
- new preference RANDOMISED_RESTART_INIT to use randomised restart for initialisation
and setup constants. Individual operations with name OP can also be executed with randomised
restart by using MAX_OPERATIONS_OP == -Nr, where Nr is the Nr of restarts.
- new SAFETY_MODEL_CHECK preference to store only one incoming transition for safety model checks
to reduce memory consumption
- improved well-definedness detection and providing precise error locations for many more errors
- improvements in Alloy support, many more Alloy specifications are now supported.
- improvements in ProB parser: improved error messages for many common mistakes.
1.10.2018: 1.8.2
- allow deterministic trace replay to reduce memory consumption
- fix potential variable clashes in nested B while loops with operation calls
- improvements in kernel (improve symbolic treatment of set difference, avoid enumeration warnings
for large but finite sets, ...)
- improved error location detection for some error messages; provide possible alternatives for
errors involving identifiers
- support for loading Alloy models
- improve pretty printing values in TLA+ mode
- changes for external functions: DEC_STRING_TO_INT raises WD errors to avoid spurious error messages,
improve READ_CSV to skip over empty lines
- support /*@symbolic */ pragma for UNION
- conversion to Unicode for B symbols in ProB Tcl/Tk Edit menu
1.8.1-rc4 (not officially released)
- support PNG images for ANIMATION_FUNCTION and ANIMATION_IMG, also look for images relative to
the file in wich the ANIMATION_IMG is declared.
Add horizontal scrolling for very wide visualizations and allow to scale visualization.
Allow to specify font and size for strings (TK_CUSTOM_STATE_VIEW_FONT_NAME/_SIZE)
- allow to choose dot layout engine via DOT_ENGINE preference
- support Atelier-B's "ref" keyword in Event-B (.sys) models
- better error messages for unknown identifiers (fuzzy matching and completion checking)
- support Jupyter kernel https://gitlab.cs.uni-duesseldorf.de/dgelessus/prob2-jupyter-kernel
- executing operations by predicate can now also specify post-conditions (e.g., on non-deterministically
assigned variables)
- CUSTOM_GRAPH_EDGES and CUSTOM_GRAPH_NODES can provide shape information and a much wider range of Tk/dot colours.
- add CODES_TO_STRING, HASH, ... external functions in LibraryStrings.mch
- improved error location feedback for expressions involving (nested) DEFINITION calls
- improvements in kernel (detection of infinite sets, symbolic treatments of set difference, ...)
- reduce console output in -silent mode
- add optional ndjson error logging via NDJSON_ERROR_LOG_FILE preference
20.03.2018: 1.8.0
- add terminal colour output in probcli, can be disabled by setting NO_COLOR environment variable
- improved performance of evaluation/state views in UI for large values
- changed treatment of reflexive closure: now corresponds to the more usual
mathematical definition: closure(X) = id(TypeOfX) \/ closure1(X)
The previous definition closure(X) = id(ran(X)\/dom(X)) \/ closure1(X) and
the definition in Atelier-B closure(X) = id(dom(X)) \/ closure1(X)
are not compatible with the following law in the B-Book on page 169
(r[a] <: a => closure(r)[a]=a)
Note that closure({1|->2}) and iterate({1|->2},0) are now infinite.
- improved constraint solving for closure/closure1 operators
- static symmetry breaking uses partition predicates of deferred sets
- allow LET expressions and predicates to introduce multiple, dependent identifiers in order
(for LET substitutions this is only allowed if the preference ALLOW_COMPLEX_LETS is TRUE)
- TYPE_CHECK_DEFINITIONS preference to type check definitions (also unused ones)
- improved static checking for INITIALISATION order
- add preference DETECT_LAMBDAS to detect set comprehensions that can be transformed into lambdas
- added bitwise external functions in LibraryBits.def
- add TYPED_STRING_TO_ENUM, SLEEP external functions
- added random_subset and random_permutation external functions in LibraryRandom.def
- improvements in constraint solving kernel, e.g., total function checking for range
- allow to replay JSON trace files and to export to JSON trace files in ProB Tcl/Tk
05.10.2017: 1.7.1
- new feature to export history to HTML file with graphical visualizations
- improved presentation of quantifiers in Tk Evaluation View
- improved presentation of non-deterministically assigned variables in operations view
(shown first for INITIALISATION, more variables shown for variables without parameters
and return values)
- made Z operation schema detection more flexible: schemas which work on part of
the variables are allowed and extended to schemas which do not change the other variables,
allow custom execution of Z operations by parameter values, improvements in kernel for Z types,
allow opening .zed files in addition to .tex files
- performance improvements in kernel
- added SOLVER_STRENGTH preference (to increase strength of propagations for large
sets, for reification of quantifiers, ...)
- external predicate SCCS for computing strongly connected components
11.07.2017: 1.7.0
- ProB now assumes strings, machine files,... are all encoded using UTF-8
- first (limited) support for VALUES clause for constants
- printf, PRINTF now take a B sequence as arguments (e.g., printf("~w -> ~w",[2,3]))
- result parameters of B operations can now also be read, as in Atelier-B
- Warnings for potential variable captures of DEFINITIONS are issued
- Parser now uses socket communication instead of standard input/output
- Parser supports RULE DSL language for easier data validation
- ALLOW_LOCAL_OPERATION_CALLS preference added, resulting in a topological
sorting of the operations in a machine
- improve RANDOMISE_ENUMERATION_ORDER for sets and for order of variables
with same type priority
- improve symmetry breaking for record variables and set extensions
- speed up KODKOD predicate analysis
- many improvements in kernel (UNION for singleton sets, member for domain/range restriction/subtraction,
detect useless quantifiers, ...)
- new external functions (WRITE_XML, INT_TO_DEC_STRING, STRING_CONTAINS_STRING, SHA_HASH, ...)
- Tk graphical visualization can now react to clicks (ANIMATION_CLICK and ANIMATION_RIGHT_CLICK Definitions)
- new features for Latex mode: LATEX_GREEK_IDENTIFIERS preference, better dot support, ...
- some sequence operators can be applied to STRINGs (when preference STRING_AS_SEQUENCE set to TRUE)
20.10.2016: 1.6.1
- Parser supports IF-THEN-ELSE and LET without parentheses,
IF-THEN-ELSE also allowed inside predicates
- add -latex command to process Latex files and integrate B/ProB results
- add -logxml FILE command to log probcli commands and result to XML file
- add performance message logging
- improvements in ProB kernel: AVL set-membership using CLPFD table constraint,
function application of partially known function using CLPFD element constraint,
better reification for quantifiers, better WD detection, better if-then-else
solving, performance messages
- add READ_XML external function to read in XML files and READ_CSV for files in CSV format
- add LibraryMeta external functions to inspect ProB and model state
- improve Kodkod backend: support more cardinality constraints, add preferences
KODKOD_SAT_SOLVER, KODKOD_SYMMETRY, KODKOD_MAX_NR_SOLS, KODKOD_RAISE_WARNINGS
- improvements in LTSMin bridge (guard splitting, partial order support)
- improve pretty printer: prints fewer parentheses
- better static name clash checking
- add :replay FILE command and :list command to probcli -repl
- fixed highlighting of syntax errors in ProB Tcl/Tk under Windows
- improve Atom editor support: provide full error spans
- add Definition call graph visualisation
- add -dot Diagram File and -dotexpr Diagram Expr File commands for probcli,
possible values for -dotexpr Diagram : expr_as_graph, transition_diagram
possible values for -dot Diagram :
machine_hierarchy, event_hierarchy, state_space, signature_merge,
dfa_merge, state_as_graph, invariant, properties, assertions, deadlock,
goal, enable_graph, dependence_graph, definitions, ....
22.04.2016: 1.6.0
- Parser supports full range of Atelier-B Unicode symbols for classical B machines,
better support for /*@label LBL */ pragma,
new description pragma /*@desc DESC */ following predicates or identifiers,
line comments now supported: // line comment
more precise error location within DEFINITIONS,
improved error messages for certain common mistakes (extra & or ;)
leaner error messages without duplicate information about location
fixed bug on Windows concerning transfer of error messages (e.g., no error locations were displayed)
- support for the Atelier-B tree operators
- parser and ProB support using IF-THEN-ELSE and LET for expressions (have to be surrounded by parentheses)
- directed model checking available: -mc_mode M with M:{hash,heuristic,random,breadth-first,depth-first,mixed}
- new probcli command -disable_timeout to disable time-outs in model checking and animation
(also results in performance improvements when time-outs not needed)
- new commands in probcli REPL:
:find LTL_Atomic_Property
:source and :origin to get information about identifiers
:e to open source file in external editor (and show error in Vim, Atom, BBedit,...)
:kodkod E to evaluate formula E using Kodkod
- Tk Coverage Table for expression accepts optional filter property (LTL atomic property)
- added Event Refinement Hierarchy Diagram (Visualize Menu in ProB Tcl/Tk),
state as dot graph diagram can represent records,
added scalable force directed (sfdp) visualization of state space
- ProB Tcl/Tk now has repeat last menu command (Cmd-Shift-R)
- Rodin Disprover checks for inconsistency in hypothesis in case proof found
(unless DOUBLE_EVALUATION preference is set to false)
- improvements in kernel (better detection of identical predicates, symmetry breaking
for X in card(X)>Nr, improved ground checks, improved constraint propagation for image,
-->> / +->>, >->>, records containing infinite sets, (non-)emptiness checks of set comprehensions,
improvement for quantifiers involving domain/range,...)
- some static symmetry detection for universal and existential quantification (for first two identifiers)
- improvement in memory consumption for storing state space
- CSE deals correctly with associativity and commutativity, fixed issue with computing
WD-guarded shared predicates
- ProZ is more flexible in detecting initialisation schemas (containing Init in name),
improved Z syntax highlighting, Z integer division is now floored division
- guards embedded within Classical B actions are used in evaluation view and for enabling analyses
- added CSV reader external function
- more stringent static checking of LET substitutions
- new symbolic model checking commands
- Z3 interface available (use :Z3 predicate in REPL)
- probcli supports dash (-) instead of underscore within commands
- type checker can sometimes give hints (adding {.} for relational image, using |-> instead of ->,...)
- $0 variable suffix can now be used within DEFINITIONS (PARSERLIB-47)
- SETUP_CONSTANTS and INITIALISATION shown names of constants and variables in operations view
- model checking test-case generation (-mcm_tests) xml files now include operation parameters
-----------------
19.02.2015 : 1.5.0
- improved RANDOMISE_ENUMERATION_ORDER preference (many more enumerations can
now happen with random ordering of elements)
- improved constraint solver: e.g., partitioning of predicates into components
can now inline simple equalities
- added MACE/SEM style static symmetry reduction for constants element of deferred sets (http://www.stups.uni-duesseldorf.de/ProB/index.php5/Symmetry_Reduction#Static_Symmetry_Reduction)
- improved prover/disprover capabilities; added -cbc_result_file FILE and -cbc_assertions_tautology_proof
commands to probcli; probcli can now load PO files generated by
ProB Rodin plugin and some SMTlib files (.smt2 extension)
- added first version of Common-Subexpression-Elimination (CSE)
- added bounded model checking command -bmc to probcli (http://www.stups.uni-duesseldorf.de/ProB/index.php5/Bounded_Model_Checking)
- cbc_tests has additional options: -cbc_cover_match E to match all events where E occurs
in the name, and -cbc_cover_final to specify that all target events should only be
used as final event in test cases (this option is also available in the Tcl/Tk dialog)
- reduce memory consumption of CTL model checker
- CTRL-C now works within probcli (in particular REPL)
- added Tree View for CBC Tests in ProB Tcl/Tk
- improved performance of CBC Test case generation using feasibility analysis and more enabling
analysis results
- added feasibility analysis (-feasibility)
- added MC/DC coverage analysis for guards and invariants
- added -scope PRED command
- added -all_paths FILE command
- the LTL model checker now supports fairness and deadlock and determinism properties
- improved TLC interface: better replay of traces, features to set number of workers,
enable symmetry detection and use ProB to set up constants
- Parser now looks in stdlib folder for included machines/definition files; the
ProB external function library machines come bundled with ProB in this way; the folder
can be set via the PROBPATH environment variable
- removed different parsers, removed preferences regarding
parsers. Now, the Java parser is just with sane defaults as the only option.
- switched to SICStus Prolog 4.3
---------------
18.08.2014 : 1.4.0
- Tcl/Tk new commands: find relative deadlock, find controller state violation,
Value Coverage (evaluate expression over whole statespace; possible CSV export),
evaluate expression over history
- Tcl/Tk: re-organize the menus and improved progress bar for model checking
- new command: evaluate expression over history and save as CSV (-csvhist in probcli or right-click on history in Tcl/Tk)
- CLPFD now turned on by default; improvement in some default preferences (editor on Mac,...)
- ProB now knows whether enumeration warning were triggered for computing enabled operations; in Tcl/Tk an orange "infinity" symbol lights up if this occurs
- improved treatment of enumeration warnings for infinite sets
- better enumeration strategy for large or infinite domain variables (trying to defer their enumeration)
- improved detection of infinite set comprehensions, which are kept symbolic
(e.g., {x,y,z| x*x + y*y = z*z} or {x,y,z| z:seq(NATURAL) & x^y=z} are
now automatically kept symbolic)
- the kernel can treat more operations symbolically, without the need to expand set comprehensions: composition ;, override <+, set difference and intersection
- TLC can be used as external model checker for classical B machines in Tcl/Tk
- additional external functions: ARGV, ARGC to provide command-line arguments to B machines, STRING_TO_ENUM,
READ_LINE, EOF, ...
- B machines can now be executed on Unix machines by using first Shebang line: #! PATH_TO_PROBCLI
- bug fixes in the kernel (mainly relevant in SYMBOLIC mode)
- bug fix in Event-B record detection for records with more than two fields
- REPL of probcli and ProB Tcl/Tk allows definitions of auxiliary variables using let X = Expr, added other commands like :b for browse of definitions,...
- probcli -repl now also accepts CTL and LTL formulas (with $ctl or $ltl prefix) and
it is possible to pretty print the B formulas in Unicode
- bug fixes in Tcl/Tk REPL (copy&paste) + Evaluation View uses Unicode
- variants and theorems in guards are shown in Evaluation View and ProB for Rodin state view
- improvements in constraint solver: domain, range, -->>, partition detection inside machines, ...
- constraint-based refinement checking
- Tcl/Tk GUI improvements: double click in History to go back
- performance improvements, in particular for WHILE loops
- control-flow graph and enabling analysis
- new -execute command with filtering of unused constants, faster than -animate (does not store intermediate states)
- improved performance of constraint-based test-case generation algorithm
- Graphical Visualisation: allow multiple ANIMATION_FUNCTION[0-9]*, allow them in XTL mode, support for more animation functions: showing textual representation of values if not integer or no image or string available, support for ANIMATION_STR_JUSTIFY_LEFT and ANIMATION_STR_JUSTIFY_RIGHT
-----------------
01.03.2013: 1.3.6
- improved constraint propagation for modulo and division
- new format for .eventb files generated from ProB-Rodin; contains well-definedness
condition information and fixes issue where model checker with Proof Info was unable
to find certain invariant violations after an undefined invariant was encountered
- probcli model checker (-mc) now also checks all states that were previously visited
by other commands such as trace checking (-t)
- other minor constraint propagation improvements ({x,y,..} <: 1..n supported better,...)
- various performance improvements (e.g., in Event-B removed redundant checking for
extended events)
- prj1(A,B)(x,y) --> it is now checked that x:A and y:B; same for prj2; this can be overridden by setting the IGNORE_PRJ_TYPES preference to TRUE
- CASE statement static checking for classical B has become more stringent: we require
that all cases are literals (to be compliant with Atelier-B)
- Eval console (both in probcli and ProB Tcl/Tk) now works with Kodkod (if Kodkod enabled);
various bug fixes and improvements in the Kodkod translation
- reduced statespace and DFA statespace now also works in CSP-M mode
- Eval console now also supports deferred set identifiers generated by ProB
- Tk REPL improvements: command-backspace clears, fix in copy&paste behaviour
- bug fix in ProB kernel; solutions could be lost in context of bool(.)
- improved Model Checking dialog: progress bar, number of checked nodes kept track of, ...
- constraint-based refinement checking, enabling analysis, test-case generation available in expert mode of Tcl/Tk
- new view neighbourhood in state space command
-----------------
30.09.2012: 1.3.5
- performance improvement in model checking and constraint solving (CLPFD mode)
- constant and operation value caching using the -cache DIRECTORY option
- new Kodkod backend; enable using -p KODKOD TRUE in probcli or Preference menu in ProB Tcl/Tk
- CSP|||B supports sequences and sets and performs (limited) static checking
that synchronisation channels are properly typed
- support for pragmas, e.g., /*@ symbolic */
- first version of physical unit inference and checking plug-in
- support for external functions (currently only those coded in Prolog)
- improved detection of infinite functions (e.g., disjunctions of lambda expressions
recognized as infinite if one of the disjuncts is)
- support for recursive functions
- support for the Event-B finite operator; within classical B the construct S:FIN(S)
is recognized as equivalent to finite(S)
- in addition to application f(x), we can now also compute the image f[S] and
the composition (R;f) for an infinite function f; provided S and R are finite.
- support for TLA, TLA2B translator can be installed from within Tcl/Tk version
- improved default hash on 64-bit systems
- Eval window now also recognises strings + faster syntax highlighting,
multiline comments highlighting on the fly; added more contextual menus in editor
and other panes
- improved "Current state as graph" display, grouping deferred and enumerated sets
- many new options for probcli, see http://www.stups.uni-duesseldorf.de/ProB/index.php5/Using_the_Command-Line_Version_of_ProB
- many more tests, bug fixes, performance improvements
-----------------
21.11.2011: 1.3.4
- Evaluation view (requires Tcl/Tk 8.5) providing hierarchical view and inspection of VARIABLES, CONSTANTS, INVARIANTS, PROPERTIES, ...; possibility to inspect complete value by double-clicking; possibility to save values of CONSTANTS and VARIABLES to file
- Eval window allowing to enter expressions and predicates for B, CSP, and Z (albeit B syntax has to be used when querying Z); can be opened by either double clicking in State Properties pane or menu command Eval... in Analyse menu.
- improved editor: current line number display + line numbers can be shown left, continuous syntax highlighting, parentheses highlighting
- support for CSP exception operator
- new feature: CSP in-situ refinement checking, divergence, determinism
and deadlock checking,
CSP assertions are parsed and can be checked,
new dialog box (inspired by FDR GUI) for checking CSP assertions in a file
- source code highlighting of well-definedness errors (does only highlight in the main file at the moment)
- the Analyse -> Analyse Predicate commands provide feedback when infinite sets (such as NATURAL) had to be expanded
- 64-bit version for Mac available, faster, better hashing + more memory available
- usage of SICStus 4.2; hopefully fixing issues with CLP(FD) crashes,...
- many improvements in constraint solving kernel
- improved performance of hash symmetry markers: reduction in size + performance
improvement
- improved feature: constraint-based invariant checking
- new feature: constraint-based sequence checking (in Verify -> Constraint-Based Checking menu)
- added possibility to specify an animation function in Z, too
- we allow the usage for x$0 in while loop invariants
- bug fixes in CSP-M, ...
-----------------
10.2.2011: 1.3.3
- new feature: constraint-based deadlock checking
- improved debugging of unsatisfiable PROPERTIES: ability to minimise (computing unsat core)
- improved boolean constraint solver, smt preference for reification of membership predicates
- improved usage of CLP(FD) solver, added reification for certain predicates
- updated parser to priorities in french version of Atelier B manual (priorities in english manual are wrong)
- improved performance when displaying long counter examples (>10,000 steps)
- record detection (compatible with Rodin Records plugin when using closed records; but also
works with hand-coded records); improved treatment of some infinite sets
-----------------
30.7.2010: 1.3.2
- Many improvements for Z mode: bags supported + many more Z operators ...
- 64 bit version available for LTL model checker, nauty library
- PROPERTIES are partitioned: better performance + debug feedback in case of inconsistency
- complement sets (INTEGER - S) can sometimes be represented symbolically
- ProB detects WD-error in some cases when card(.) applied to infinite set
- integration of CLP(FD) solver for integer values
- improved kernel performance for many kernel predicates, better waitflags store, optimized treatment for SIGMA(ID).(ID:SET|EXPR), and the same for PI
- improvement in many B operations for large sets/relations (especially involving intervals)
- optimized forall treatment now also available for multiple variables: !(x,y).(x|->y:SET => P)
- model checker/animator can make use of previously computed operation effects
- time-out per operation in B
- exhaustive kernel checks: much more unit tests + some fixes
-----------------
Dec 2009 : 1.3.1
- coloring of enabled operations: blue: skip operation; green: leads to open node; red: leads to error node
- added option to force depth-first in model checker
- timeout for invariant violation properly shown in status bar
- improved inference of minimum required cardinality of deferred sets; certain constants are automatically added as if we had a partially enumerated set (performance improvement + better readability in animations)
- detection of witness errors in multi-level animation mode for Event-B; many improvements to multi-level animation
- well-definedness errors are stored along with the state and shown in the Properties Pane
- adapted treatment of CSP interrupt operator, now conformant with ProBE (based on page 72
of Steve Schneider's book, Concurrent and Real-time Systems)
- support for Rodin 1.0 id, prj1, prj2, partition operators
- support for Atelier B .sys files, SYSTEM & EVENTS keywords (not yet VARIANT, WITNESS)
- added forward/backward buttons
- added option to use constants for deferred set elements in DOT view
- improved displaying of .eventb models in classical B style
- Execute Specific Operation ... works again and now can also be used to guide machine
initialisation and setting up of constants
- improved treatment formulas of the form: !x.(x:SET => PRED)
- performance improvements insided the kernel (Siemens San Juan case study: went from 17 minutes to 5 minutes; CruiseFinite1 went from 12 seconds to 5 seconds).
-----------------
March 20,2009: 1.3.0
ProB 1.3.0-Final is available for download. Highlights: New parser and integrated typechecker, install as AtelierB plugin, improved kernel with support for large sets/relations, improved CSP support, faster LTL model checker, Undo/Redo in text editor, graphical formula viewer, user definable custom animations with gifs.
- improved performance of signature-merge and DFA reduction viewing
- added support for let (a,b,c) = E style expressions in CSP
- added possibility to link Event-B models with CSP
- can now animate .eventb files generated from Rodin EventB models
- added parallel product
- added AVL representation for more efficient representation of large sets
- added new phase of kernel to priortise computation with fully known values
- added support for STRING datatype (enumeration still limited to {STR1,STR2})
- improved internal representation for BOOL type
- speed improvement inside the B kernel
- improved handling of abort conditions (application of function outside domain,
division/mod by 0, first/last/... of empty sequence)
- improved hashing inside model checker
- graphical visulisation of INVARIANT and operation preconditions
- added user-definable custom .gif Animation via ANIMATION_FUNCTION, ANIMATION_IMGn, and
ANIMATION_STRn declarations in the DEFINITIONS section
- added support for lambda expressions and currying, not yet fully tested
- added nametype and subtype support for CSP
- fixed a problem when using dotty viewer in Windows for B machines/CSP specs whose
paths contained spaces; updated the dotty defaults, added new colours and shapes
- PRE conditions of operations are propagated down to refinements and implementations if
possible (that is, a conjunct is propagated down if the variables it refers to also
exist in the refinement/implementation)
- While loops: Invariant now also checked upon loop exit; multiple assignments to same
variable also checked for INITIALISATION
- Menu Command Key shortcuts now work
- fixed bug with x::NAT1,...
- added (partial) type checking on substitutions and highlighting of type (and some other errors)
in the source code; reduced number of error messages when type errors occur
- LTL model checking for all platforms, improved C-version (1-2 orders of magnitude faster)
- LTL formulas with patterns
- possibility to define LTL Assertions in the DEFINITIONS clause and command for checking them
- more CSP-M features (records, recursive datatypes, tuples, non-associative tuples,...)
- Debug Operations... command in Analyze menu
- bug fixes in kernel (NatRange, empty closure sets,...)
- moved to SICStus 4.0.2 (a bug in earlier version of SICStus could affect ProB with
sets of sets in some circumstances)
- improved type inference ( x|->y|->z : SomeRel,...)
June, 2007: 1.2.7
- LTL Model checking (only works in Sicstus4 built binaries)
- move to Sicstus4 on Mac and Linux: no more 256 MB limit!, speed improvements in
model checker (currently slow down in animation when things get printed on screen
due to a problem in Sicstus4)
- Almost fully CSP-M (FDR) compliant parser and animator; dropped support for old CIA-CSP
syntax; visual highlighting of channel outputs (when single clicking on enabled operations in Pane)
- Refinement checking for CSP-M, taking tau actions into account
-----------------
March 8, 2007: 1.2.6
- added support for parameter passing to Included/Imported/... machines
- added support for machine renaming (e.g., INCLUDES c1.M, c2.M)
-----------------
February 16, 2007: 1.2.5
- a new, improved version of ProZ included
- incorporated fuzz binary in ProB distribution (thanks to Mike Spivey)
- added timeout feature + preference
- added buttons for timeout, max. nr of operations reached and invariant violation
- improved partial function/surjection/... so that infinite domains can be dealt with
properly without expansion (NATURAL, NATURAL1,... closures,...)
- added support for iterate(r,n) operator on relations
-----------------
December 4, 2006: 1.2.4
- added support for WHILE loops and IMPORTS in Implementations
- improved mixed DF/BF search (especially for infinite state spaces)
- added support for pred,succ applied to numbers
-----------------
November 22, 2006: 1.2.3
- added check for cyclic dependencies in machine hierarchy + check for
multiple inclusions; added topological sort to determine correct
initialisation order (before all initialisations were executed in
parallel; now a machine can use the values of variables in used/included/seen
machines for its own initialisation)
- struct can be used for Struct
- added graph canonicalisation option in Advanced Preferences
- added symmetry markers in Advanced Preferences
- fixed normalisation for set_up_constants
- improved type inference when enumerated elements of SETs used
- debug properties now shows SETS sizes and MININT and MAXINT
October 2, 2006: 1.2.2
- added a debug PROPERTIES feature; accessible when setting up of constants
fails
- added support for B4Free EventB syntax: MODELS in place of MACHINE
and WHEN P THEN A END in place of SELECT P THEN A END
- prj1,prj2 can now be used freely (before could only be used when applied
directly to arguments)
- added support for ASSERT P THEN S
- improved type inference for explicit sets and sequences (x = {1,2} is now typed);
or, => and <=> are also traversed
- added menu command to view operation and their variable dependency as a graph
- fixed type inference issue for Refinement machines
- rearranged ProTest submenu
-----------------
August 31, 2006: 1.2.1
- fixed bug in type inference (occured in some circumstances with closures
containing operators * and - [where ProB is not sure about the type
until the operands are known])
- added error messages for Type Errors when comparing two objects for
equality
-----------------
August 24, 2006: 1.2.0
- CSP,XTL files can now be opened from the Open... command and are added to
the Recent Files history
- improved refinement checker in presence of constants: intialisation and
set_up_constants get merged for refinement check
- allowed parameters of type "element of SET" and BOOL
- added support for MAXINT, MININT in expressions
- NAT is treated differently from NATURAL (i.e., ProB checks that < MAXINT);
same for INT and INTEGER
- added view state as graph
- added permutation reduction
- new jbtools parser:
- fixed performance problem
- support for function application with multiple args f(a,b) instead of f(a|->b)
- support for definitions with arguments
- support for records: Struct, rec, '
- support for some Event B syntax: SYSTEM, EVENTS, INITIALIZATION
- added option to view top-level ANY arguments of EVENT B operations
as arguments
-----------------
February 24, 2006: 1.1.9
- fixed a problem whereby multiple variables in Set comprehensions, Lambdas,...
were incorrectly bracketed: {x,y,z| ...} now generates couple(couple(X,Y),Z)
terms rather than couple(X,couple(Y,Z))
- CartesianProduct is now also kept symbolic (in addition to other basic types)
-----------------
February 14, 2006: 1.1.8
- fixed a bug in the parser whereby some syntax errors lead to a looop
in the Tcl
- improved the treatment of universal quantification: if the condition
of the quantification only has typing information then the forall is not
delayed but expanded straight away, example:
!(rr, ss) . (rr : ROAD & ss : RouteElement =>
connectsAt(rr |-> ss) = {1})
- added the support for recursive closures and functional style programming
using set comprehensions:
fact4 = {x,y| x:NAT & y:NAT & (x=0 => y=1) & (x>0 => (y=x*fact4(x-1)))} &
fact4: INT <-> INT
- improved treatment of existential quantifiers: they no longer cause unnecessary
enumeration and can now be used inside lambda expressions and set comprehensions
for local variables without much overhead
- fixed a problem in the kernel where symbolic closures were prematurely
expanded
- CSP/B Integration: fixed a problem whereby arguments from the CSP were not
passed directly to the B interpreter (i.e. unification was applied after
computing the B operational semantics, resulting in unnecessary work).
- improved type inference for refined machines: type inference for operation
arguments will be applied at all levels and results merged
- added the advanced option to ignore hash collisions
-----------------
September 23, 2005: 1.1.7
- added the possibility to hide the B Source Pane (Animation preference)
- added the option to treat outermost PRE conditions not as SELECT, but
as PRE which can abort; abort state now leads to invariant violation
- the preference file is now loaded/saved in the home directory if the
applications' preference file is not writable
- added the modulo operator "mod" to the CSP syntax, fixed problem that
arguments to == and != were not evaluated
- added "New..." command to File menu
- added Files menu; allow to edit related Machines + CSP file
- improved typing for refinement machines: types is obtained from
ancestor machines as well
-----------------
June 16, 2005: 1.1.6
- improved handling of set comprehensions when not kept as closures
(also uses b_compiler.pl to reduce the number of variables one has to wait on)
-----------------
1.1.5
- improved single failures checking (dramatically when non-determinism large)
- made trace checking more flexible for setup_constants
- fixed bug which prevented use of sequences in expressions such as xx:: seq(S)
-----------------
March 18, 2005: 1.1.4
- boolean values are now displayed TRUE/FALSE (rather than true/false as before)
- fixed bug for nested PRE's (jbtools parser does not allow them anyway; but
one can tweak the XML files to obtain them)
- added option in CSP (when guiding B) to query value of B variables and constants
- improved animation for large sets/functions, improved type inference for
equalities
- allowed B machines to have no state and no initialisation
- ability to select operations and arguments for reduced state view
-----------------
December 13, 2004: version 1.1.3
- speed improvement: typing for operations is now cached
- bug fix in Analyse Properties (ProB would claim no properties exist even though
there was a properties clause)
- better type extraction: types can now be extracted from equalities (e.g. x = 2..5)
- improvements to refinement check: on the fly checking is possible, better
detection when ancestor machine is not completely explored,
new refinement check dialog box with better feedback,...
- improvements to CSP guide: error channel (error-> ... is detected similar
to invariant violation by the model checker), constants from global SETs
can be used in CSP,...
-----------------
August 19, 2004: Version 1.1.2
- ProB now remembers when not all transitions were computed for a node
(because the max number of enablings or initialisations in the preferences
is set too low); feedback is provided after model checking or in compute coverage
- the LET x BE x=E IN ... END statement is now supported
- added support to animate CSP files, with a brand new parser, and added the
option to guide B machines using CSP files
- fixed problem in error_manager where displaying error_messages (with
clpfd variables or integers) could cause a type error exception
-----------------
July 29, 2004: Version 1.1.1
- Windows version now compiled against Tcl Tk 8.4
- fixed bug for recent documents list when file name contains spaces;
Note: on Windows file names with spaces can still cause problems when
viewing with dotty (but using PostScript viewer seems to work)
- added advanced Find (allowing to redefine GOAL predicate)
- Viewer: added option to colour nodes which satisfy GOAL
- added a new view option: subgraph which can reach invariant violation
- improved initialisation in presence of parts that cannot be satisfied
(i.e., initialisation will succeed partially and user gets better feedback about
what went wrong)
- fixed bug in find_non_resetable_node when constants were present (only states after
set_up_constants were marked as initial, but not those after initialise_machine)
-----------------
July 2, 2004: Version 1.1
- added Recent Files list
- ProB now finds out its own directory to locate the icons and .jar files; it should
no longer be necessary to change into the ProB directory before executing the binary
- fixed a bug whereby execute_trace_to_node could lead to the wrong node in the
presence of non-determinism (e.g., model checking could present a correct counter
example trace but leading to a wrong node, i.e. one satisfying the invariant)
- added an option to open ProB in a small window (useful for dataprojectors)
- added reduced state space viewing options
-----------------
June 16, 2004: Version 1.0.6
- ProB now supports CHOICE with more than two choices
- added simple type error detection at runtime for arguments of operations +
some type checking for operation arguments, variables, constants
- trying to assign to constants is detected and an error raised
- added support for calling operations that return values: yy <-- CalOp(...)
- improved enumeration for TotalFunction
- added menu item "Refinement Check agains Ancestor" + added single failures refinement option
-----------------
May 11, 2004: Version 1.0.5
- added support for ASSERTIONS clause (can be analysed in Analyse menu, can
be searched for in Temporal Model check + can be checked using Constraint Based
Checking)
- fixed problem where multiple edges could be drawn (if print_self_loops=true)
- added support for partial bijection (>+>>)
- added improved treatment for size(Seq) if Seq is var and size known
-----------------
March 31 2004: Version 1.0.4
- fixed bug whereby "not( xx : EXPR)" could loop if EXPR was not
a basic expression (such as POW, ...)
- added option to open external editor
- added option to export to Promela/Spin
- added option to export to CSP/FDR
- fixed the problem with spaces in path for dotty, PS Viewer, ...
- added menu command to analyse Properties + show inferred typing information
- adapted menu structure so that on Mac it appears in the top menu bar (and not within
the Windows; thanks to Mauricio Varea for doing this).
-----------------
March 26 2004: Version 1.0.3
- added support for VAR v1,...vn IN ...
- fixed a bug in the type extraction which would somtimes remove expressions with
SetMinus in it (e.g., xx:POW(A-B) would extract a type for xx but the expression
would be incorrectly removed).
- allowed perm(.) to be used in other contexts than xx : perm(.) in non-symbolic mode;
the same will be done for other sequence constructors.
- the full detail of a syntax error can now be inspected
- fixed a bug in Image of Relation (could generate multiset rather than set)
- fixed equal_object + not_equal_object so that it works on two closures
- option to view the conjuncts of the invariant that have been filtered (because
of abstract variables in ancestor specifications that are no longer available in
the current machine)
-----------------
March 23 2004: Version 1.0.2
- added support for direct product ><
- fixed problem with dot graphical viewer if display leaves was set to false =
added new option to not view self-loops
- prevented lazy expansion for CartesianProduct (as the parser cannot distinguish
CartesianProduct from multiplication, this would sometimes lead to problems;
in the long run this will be fixed more systematically by a better type inference)
- fixed a problem with 'Minus' (sometimes the jbtools parser indicates integer minus but it is
actually SetMinus)
- variables given a type but not declared in VARIABLES are now reported (same for Constants)
- better support for Refinement (SETS and Constants are now properly imported) +
Invariant is imported from ancestor machine(s) and filtered
- added platform specific preferences (for PS viewer,...)
- fixed bug in kernel that could spuriously produce ill-typed instantiations (term(_))
and lead to warning messages being printed (not_equal_object)
-----------------
March 16 2004: Version 1.0.1
- ProB now recognises when a variable is not initialised (rather than failing
and saying the machine cannot be initialised)
- ProB now remembers the latest directory for opening (fix for Windows)
- Paths in the preferences can now be "Pick"ed (but we still need to address
a problem with paths containing spaces: for the moment all paths should
not contain spaces otherwise ProB will not be able to call the auxilary
programs)
-----------------
March 15 2004: Version 1.0.0
- added a Beginner mode for ProB + made several menu commands more robust
- new, improved menu structure
- added a B Syntax summary sheet in About menu
- model checking now puts the trace into the history
- improved type extraction for ANY + error message displayed if no typing
- added support for EXTENDS
- added colour syntax highlighting
- allowed simple editing and saving of B Machines
- added highlighting of syntax errors
- small bug fix for union_generalized (over sets of sets)
- added support for conc(ss) (concatenation of sequences of sequences)
- added generalized union and intersection over predicates: UNION(gg).(cond|expr) and INTER(gg).(cond|expr)
-----------------
February 2 2004: Version 0.9.8
- added first support for multiple machines (USES, INCLUDES, SEES, PROMOTES)
but without renaming and visibility checking
- added an option to view the module hierarchy of multiple machines
- added Safes_Chapter10 sample machines from Steve Schneider to test out the above
- added lazy symbolic closures for binary type constructors (-->,...)
- added support for <-> inside expressions (rather than as type)
- replaced error message for /|\ prefix by warning (in AtelierB it is ok to have index > size of sequence)
- added preference option to turn on/off lazy symbolic closures
- fixed several bugs related to symbolic closures not being expanded,...
- added support for type checking in expert mode only for the moment
- bug fixes for symbolic closure in not equals /=
-----------------
January 28 2004: Version 0.9.7
- added an option to check for updates
- starting using symbolic "closure" representation of expensive structures
(POWersets, ISeq, Seq, ... over some domain)
- major reworking of the kernel: got rid of special representation for sequences
(sequences are now represented as functions from integers to a range) + supported
new symbolic "closure" representation
- small improvements in interface: self-check only possible before opening a machine,
analyse invariant will no longer throw error messages if called before machine
has been initialised.
- added a few more machines (Laws/....) to check that ProB is functioning properly
-----------------
January 20 2004: Version 0.9.6
- improved type inference for CartesianProduct: xx,yy: T1 * T2 => xx:T1 & yy:T2
- added support for CASE statement
- fixed problem in SELECT statement (ELSE statement was always possible; now negation
of all other conditions checked)
-----------------
January 14 2004: Version 0.9.5
- added support for parameters which are scalars: parameters which are
all UPPERCASE are treated as sets, the rest as scalars
- added support for PrependSequence, AppendSequence, PrefixSequence, SuffixSequence
- more machines from Steve Schneider's book added
-----------------
January 13 2004: Version 0.9.4
- added TotalSurjection and PartialSurjection
- added "Permutation Sequence": perm
- added support for closure1 operator [transitive closure]
(Note: the 'transitive and reflexive closure' operator requires information about
the types of its argument; ProB does not have this information available and
the type is not present in the B; more work is needed)
- added some new machines taken from Steve Schneider's book on B
(http://www.palgrave.com/science/computing/schneider/).
These machines are distributed with kind permission by
Steve Schneider, and have been tested with ProB. In some
circumstances, minor changes were made to the machines to
make them more suitable for use with ProB.
-----------------
December 30 2003: Version 0.9.3
- added support for sequential composition of statements (;)
- added support for calling operations (which do not return values)
- added support for min,max and relational composition (;)
- added missing enumeration for initialisation of machine
- got rid of error message when true was evaluated within negation
- added support for PI (var) . ( | )
- some support for treating sequences as sets (element of sequence, dom, ran of sequence,
using sequence as function and applying)
- fixed bug in strict subset of <<:
- fixed bug for extension sets: {aa,aa} is now converted into {aa}
- fixed bug when checking for "not partial function"
- State pane can now scroll horizontally
-----------------
December 16: Version 0.9.2
- more efficient checking for cartesian product: xx : A * B
- constants are extracted from *both* abstract and concrete constants
- preferences manager: natural number preferences can be set to 0 & 1
- internal: additions to prototype Z mode (enumerate sets)
-----------------
December 11: Version 0.9.1
- added clearer message about multiple machines not yet being supported
- fixed a bug concerning "filter failed message" for ForAll & Exists
- provide better error messages when java ConsoleParser, dot, dotty, PSview do not work
-----------------
December 9:
- introduce version numbering for ProB
- new version: 0.9.0
-----------------
December 8:
- improved the preferences management: preferences are now saved; paths to PS & Dot viewers
can be typed in
- added support for injective sequences iseq and iseq1 (xx : iseq1(S) or xx /:iseq(R) ...)
- several improvements to the kernel, all self-checks now pass (but a few still have mutliple
solutions which is not a problem)
- find valid initial state now takes constants into account
===============
December 1:
- added support for SIGMA
- parameters are supported (handled as SETS)
- .ref and .imp files can be opened; however ProB does not yet recognise the variables
coming from the abstract machine (error messages will be printed when loading the machine;
all unrecognised variables are assumed coming from the abstract machine and the bits of
the invariant using that are removed.)
- added a first version of refinement checking (to do a refinement check: 1. load the specification
machine, 2. explore it, e.g., using temporal model checking and then 3. "Save the state for later
refinement"; then 4. load the machine you believe to be a refinement; 5. explore the machine as much
as you can, e.g., using temporal model checking; then 6. do the refinement check and select the
_refine_spec.P file you generated above in 3.).
- Note: some self-checks fail on this release; but this should not be a problem and will be fixed
soon.
===============
November 28:
- fixed the Cancel button in the Model check dialog
- added a find non-resetable and find non-deterministic nodes option
===============
November 26:
- added domain_restriction <| and range_restriction |>
- type inference now recognises subset <:
- better error feedback to TclTk GUI
- outgoing transitions are no longer recomputed when revisiting a state
===============
November 24:
- various speed improvements (unnecessary backtracking in kernel removed)
- ProB is now more stringent about typing of set comprehensions, lambda abstractions and
operations
- a few bug fixes
- new preference dialog
- one can now set an upper bound for max number of initialisations and enablings that are
computed
- ProB now detects when part of a parallel assignment within the initialisation
- an experimental mode has been added where set comprehensions and lambda abstractions are
not expanded, but compiled into closures (not yet fully functional)
===============
November 17:
- fixed a bug in how partial functions were enumerated (bug was introduced in last version).
===============
November 11:
- added first support for CONSTANTS and PROPERTIES section
- initialisation now shows chosen values in animator
===============
November 10:
- added support for TotalBijection + NonEmptySubsets POW1
===============
November 10:
- a single command line argument can now be supplied: ProB will try to open that file
Improved efficiency of enumeration; operation arguments are now also typed and
properly enumerated, Warning message printed if an operation argument is not typed;
the "only label base types" option may thus become superfluous
- fixed a problem with treating nested functions (e.g., xx :: a -> (b -> c) did not
work properly before), the problem of multiple versions of the same value should
also have disappeared
- note that the jbtools parser (and Atelier B) treats a -> b -> c as (a->b)->c; so you have to use
brackets if that is not what you wanted (which is likely; but that is the standard
definition for B)
===============
November 7:
- added support for generalized union (union), intersection (inter), FinitePowerSet (FIN),
ForAll statements with multiple variables (!(xx,yy).(...) ) .
Improved the Temporal model check dialog box.
Added: "Ignore Types in Invariant" option in the Animate menu.
Added hashing function to speedup lookup in larger state spaces.
===============
October 29:
- added a new feature: one can ask ProB to only find one way for enabling
every operation; also: the "only label base types" option has been turned
off by default.
===============
October 27:
- fixed a problem in the code for assignment from a set (xx :: COLOURS or
yy:: POW(ID) ) which only worked for simple types or sets
===============
October 14:
- fixed the Windows .exe file to work (hopefully) on more platforms
replaced the ProWin.zip file
===============
October 10:
- corrected a bug that prevent the use of the constraint based checker (which
however still needs some work to be made more robust on larger machines)
===============
October 6:
- made type extraction from invariant more flexible: previously defined variables are now allowed
- added support for integer_set assignments: xx::NAT, xx::INT, ...
- added a preferences manager (but preferences cannot yet be edited)
===============
October 3:
- added support for division
- added msvcr70.dll file for Windows distribution
===============
First Release:
Version 0.7 - Alpha Release
Released on October 1 2003