Full ProB release history until release 1.6.0:
RELEASE HISTORY
===============
1.6.1-beta
- fixed highlighting of syntax errors in ProB Tcl/Tk under Windows
- Parse supports IF-THEN-ELSE and LET without parentheses, IF-THEN-ELSE also allowed inside predicates
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