3.0.0 (09/12/2013)
FDR3 is a complete rewrite of FDR2 that includes a number of exciting new
features.
- A brand new refinement checking engine that:
- Is multi-threaded, allowing it to make full use of multiple cores.
- Has been heavily optimised, meaning that single core performance tends to
be around double that of FDR2.
- Includes alternative data structures for storage of states.
- Has a fully integrated type-checker, that permits the vast majority of
reasonable CSP programs, whilst keeping errors readable.
- A compiler that optimises the representation of some CSP processes
(compared to FDR2) and also compiles machines in parallel.
- A completely redesigned GUI that includes:
- A redesigned and more powerful Debug Viewer that,
in particular, explicitly indicates how events synchronise, even through
renaming.
- A fully integrated version of Probe.
- A full interactive prompt, allowing for
easy experimentation with CSPM.
- An enhanced version of CSPM with:
Compared to FDR2 there are the following differences:
- The compression function
model_compress has been removed.
- The batch mode has been removed and replaced with a new output format (see
Machine-Readable Formats).
- Only the Traces, Failures and Failures-Divergences models are supported.
Support for the other models that FDR2 supported will return in a subsequent
release.
Compared to 3.0-beta-7, the following changes have been made:
- Enhanced the refinement checker to terminate as soon as a counterexample as
found.
- Fixed an issue where the debug viewer could sometimes elide rows that were
important.
- Fixed an issue that caused machines compressed using
dbisim and
wbisim to have more transitions than necessary.
3.0-beta-7 (15/11/2013)
- Created RPM and Apt repositories to allow for easier installation on Linux.
We strongly recommend that all existing users install FDR3 in this way, if
possible. Instructions for doing so can be found on the FDR3 home page.
- Improved the performance of the on-disk storage option during refinement
checks. Several new options have been added to control it, including:
refinement.storage.file.path,
refinement.storage.file.cache_size,
refinement.storage.file.checksum, and
refinement.storage.file.compressor.
- Modified the behaviour of
wbisim to be full weak bisimulation and
renamed the old version of wbisim to dbisim, which computes
a delay bisimulation. wbisim can compress more than dbisim,
but in the worst case takes twice as long to compute.
- Adapted the compiler to elide some unnecessary taus, thus reducing the state
space size of some processes. This change is to match a feature in FDR2.
- Improved the performance of
sbisim.
- Improved the performance of checks that use
chase and
prioritise.
- Parallelised divergence checking. This allows multiple threads to proceed in
parallel, checking for divergences that start from different nodes. This will
does not parallelise divergence checks that start from a single node.
- Improved the usability and stability of the
debug viewer.
- Added the
cd command to the session window that changes
the current directory.
- Fixed several crashes in the graphical user interface.
- Fixed a few performance issues and one incorrect error message that sometimes
appeared when evaluating complex CSPm scripts that make use of large recursive
datatypes.
- Fixed ghosting that could occur in the debug viewer.
3.0-beta-6 (18/10/2013)
- Many bugs have been fixed in the graphical user interface, including:
- Fixed several issues that caused FDR3 to steal focus on Ubuntu.
- Refusal sets are now correctly calculated.
- Fixed an alignment issue with behaviours in the debug viewer.
- Fixed a bug that caused the user interface to lockup if Run All was clicked
whilst another assertion was running.
- Removed a warning that QT emitted on startup.
- Fixed an issue that prevented the user interface from shutting down on
Ctrl+C.
- Fixed a crash when unchecking
Show Taus.
- Added support for opening files either by dragging them to the application
icon (Mac OS X only), or by opening them using the operating system’s file
browser.
- Improved the performance of refinement checks on large machines with multiple
processor sockets.
- Optimised the
diamond compression.
3.0-beta-5 (12/09/2013)
- Many improvements to the Debug Viewer, including:
- All behaviours are now always correctly aligned in the debug viewer (i.e.
it is now always the case that events in the same column are synchronised).
- Improved the presentation of divergence and deadlock counterexamples.
- Names of named compressed processes, such as
normal(P), are now
displayed.
- Added an option to hide taus in the trace.
- Added the ability to highlight a row and column.
- Added a new Transition Popover that appears when hovering over an event in
the debug viewer. If the event is a tau this will display the hidden event
that was performed. In all cases it will display what leaf machines
synchronise to perform the event.
- When zoomed in, the machine name for a given row is now always visible, even
after scrolling.
- Fixed a crash that could occur when dividing loop counterexamples.
- Added reporting of transition rates during refinement checks.
- Improved the presentation of the speed and memory graphs that appear in the
refinement status popover.
- Added machine-readable output to the command-line tool; see
Machine-Readable Formats for further details. This replaces FDR2’s
batch mode.
- Added two new commands,
counterexamples command that pretty-prints a textual representation of the
counterexamples to the given assertion to the prompt, and
statistics command that prints statistics
about a completed or running refinement check to the prompt.
- Improved the performance of strong bisimulation, typically resulting in a
fourfold speedup.
- Fixed parsing of expressions that mix hiding and parallel operators (such
as
X \ Y ||| Z).
- Fixed an issue that prevented the file-backed storage from allocating a file
that could appear on extremely large checks.
- Fixed a crash caused by cancelling a check during evaluation.
- Fixed a hang caused by a cancelling a check during compilation.
3.0-beta-4 (09/08/2013)
- Add support for checking determinism using the failures model.
- Added support for simple profiling of CSPM scripts.
- Added an option to disable runtime bounds checks for performance reasons
(see
cspm.runtime_range_checks).
- Added some parallelisation to the CSPM evaluator, resulting in a speed up
when complex CSPM expressions are evaluated as part of checking an assertion.
- Allow refinement checks to use on-disk temporary storage (see
refinement.storage.file.path).
- Renamed the
refinement.compressor option to
refinement.storage.compressor.
- Added a Node Inspector.
- Added an efficient representation of key-value maps (see
Map Functions) to CSPM.
- Allow more resizing of the main window.
- Added an option to close all windows whenever a load or reload command is
executed (see
gui.close_windows_on_load).
- Allow multi counterexamples to be viewed in the Debug Viewer by
setting the option
refinement.desired_counterexample_count.
- Added the ability to view refusals when viewing minimal acceptance information
in the Debug Viewer.
- Added an indication to windows that were created using previous versions of a
file (i.e. before a reload/load).
- Changed the behaviour of print statements to allow them to be evaluated on
demand, rather than always evaluating them when a file is loaded.
- Enhanced the graph viewer to allow layout to be cancelled.
3.0-beta-3 (17/7/2013)
- Added charts for memory and checking speed to the
refinement status popover.
- Enhanced type annotations to allow types
defined inside modules to be used.
- Added support for nested parametrised modules.
Note: instance declarations must now occur lexically after the module that is
being instantiated.
- Added support for type annotations to mention datatypes defined in modules.
- Allow refinement checks etc. to be cancelled.
- Improved performance of processes that contain large numbers of transitions.
- Improved some of the error messages emitted by the compiler.
- Fixed parsing of minuses immediately followed by a newline.
- Fixed a bug that could potentially caused a compiled machine to be reused
even if it had not been compiled in the correct semantic model.
- Prevent a crash that could occur if load/reload was executed whilst a
refinement check was running.
3.0-beta-2 (15/6/2013)
- Made the compiler emit an error if
prioritise is applied to a process
in such a way that makes the result semantically invalid.
- Add support for print statements.
- Reduce memory consumption during refinement checks by around 1/3.
- Added an auto-updater for Mac OS X and alert Linux users to new releases.
- Fixed a crash that could occur when loop counterexamples were divided.
- Enhanced the process graph viewer to allow
behaviours from the debug viewer to be viewed.
- Fixed a bug that prevented the Mac OS X version from being opened.
- Fixed some problems with parsing files with includes inside modules.
- Expanded
Lambda to allow multiple arguments to be specified.
- Increased the resilience of the parser when dealing with malformed includes.
3.0-beta-1 (23/5/2013)
- Add a rewritten compiler (the component which produces LTSs from processes).
This should result in reduced memory usage during compilation, as well as
reduced compilation time. Further, it fixes a number of bugs that prevented
various processes from being compiled.
- Allow multiple assertions to be compiled simultaneously in the GUI.
- Added more feedback in the GUI on how compilation is proceeding.
- Add support for parametrised modules.
- Fixed the definition of
WAIT in timed sections.
- Fixed the evaluation of empty replicated operators in timed sections.
3.0-alpha-6 (02/4/2013)
- Added support for manual type annotations, to
aid with code documentation and to make the type-checker give more accurate
errors.
- Fixed a crash that could occur when dividing repeat behaviours through
compressions.
3.0-alpha-5 (26/3/2013)
- Add more information to the machine popover to allow long traces to be easily
viewed.
- Enhanced the range of programs that can be successfully type-checked.
- Allow the previous and next word keyboard shortcuts to be used from the GUI
terminal.
- Fixed several issues that would mean
wbisim return processes that were
not semantically equivalent to the original process.
- Fixed an issue with timed CSP that would result in incorrect processes being
generated.
- Fixed the low-level implementation of
Alphabetised Parallel and
prioritise.
- Fixed a crash that could occur when a behaviour involving
chase was
divided.
3.0-alpha-4 (15/3/2013)
- Fixed a bug that caused high-level machines with compressed process arguments
to have incorrect minimal acceptances. This may have caused some assertions to
erroneously pass.
- Add support for tock-CSP via timed sections,
Synchronising External Choice and Synchronising Interrupt.
- Enhanced the refinement status popover
to include storage statistics, in addition to details on the ply. Also fix a
bug where the per node storage estimate was under-reported.
- Added support for different compression algorithms which can be used during
the refinement checking stage, including LZ4HC and zlib (see
refinement.storage.compressor).
- Enhanced the refinement engine to reconstruct counterexamples in parallel.
- Added support for the
chase, deter, lazyenumerate,
prioritise and wbisim compressions.
- Fixed the low-level implementation of
Rename and Linked Parallel,
which may have caused incorrect transitions to be reported in Probe under
certain circumstances.
- Added support for determinism checking in the failures-divergences model.
3.0-alpha-3 (19/2/2013)
- Added basic support for the failures-divergences model, including divergence
freedom checks and failures-divergences refinement checks. Note that the
current implementation has not been optimised to take advantage of multiple
cores.
- Added support for
ranged set and
ranged list comprehensions, such as
<1.. | p == 1> and {1..2 | p == 1}. Both finite and infinite variants
are supported for both the lists and the sets.
- Implemented
diamond compression.
- Implemented
tau_loop_factor compression.
- Added a popover to display performance
statistics about refinement checks.
- Fixed loading of files where the path includes
~ in FDR3.
- Improved tab completion of file names in the prompt.
- Fixes FDR3 running on older Mac’s without
POPCNT.
- Fixed the use of the forward delete key, and other deletion shortcuts, at the
prompt.
- Fixed an issue where the node highlighting in Probe was
not updated after navigating away.
- Fixed a crash that occurred when launching FDR3 with too many arguments.
- Correctly return a trace error if an assertion can fail because of both an
acceptance and a trace error.
- Allowed the semantic model that a process is compiled in to be specified when
using the
graph command.
3.0-alpha-2 (11/1/2013)
- Improved the pretty printing of processes in Probe.
- Improved the performance of Probe.
- Added a manual.
- Allowed
extensions and productions to be type-checked.
- Added a new primitive datatype:
Char that represents a character,
along with associated character and string literals.
- Added two new functions:
error and show that display a given
string as an error and pretty print a value, respectively.
- Restricted the use of prefixing to make it compatible with FDR2.
- Fixed several minor GUI issues.
- Fixed a type-checker issue that allowed incorrect programs that used
Extendable to pass.
- Fixed evaluation of replicated link parallel of an empty sequence.
- Fixed evaluation of prefixing where
? occurred before $.
3.0-alpha-1 (21/12/2012)
The initial alpha release.