ProB Release History: Difference between revisions

Full ProB release history until release 1.8.0:

RELEASE HISTORY
===============

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