Release Notes

4.2.2 (09/10/2017)

  • Fixes a bug in the compiler that would cause already compiled machines to be reused. This could cause some refinement checks to given incorrect results if they were run after other checks in the same session, but only when the state machines involved were extremely small.

4.2.1 (19/09/2017)

  • Fixes a bug in diamond that would erroneously mark divergent processes as non-divergent.
  • Add optional cspm stack tracing to record errors.

4.2.0 (20/12/2016)

This release includes a large number of internal changes that affect the way FDR is organised, and lay the groundwork for future extensions that are currently being worked on.

3.4.0 (09/03/2016)

  • Added refines --remote which can automatically run refines on a remote server (but using a local file), connecting to it via SSH.
  • Added the ability for refines to read its input from stdin.
  • Added a licensing system that requires you to provide a name and email address before using FDR.
  • Improved the presentation of loop counterexamples in the GUI.
  • Enhanced the API to add:
    • A method load_strings_as_file that allows a file to be loaded from a set of files.
    • Methods task_id that return the task id for long running tasks, such as refinement checks. This can be used to provide better progress reporting.
  • Fixed an issue where some recursive datatypes would erroneously fail to satisfy the Eq constraint.
  • Fixed an error that could cause duplicate states to be created by wbisim.
  • Fixed an error that could occur when evaluating polymorphic functions that used dot in a particular way.
  • Fixed an error that could cause superfluous compressions to be performed.
  • Fixed several crashes that could occur when debugging counterexamples in the GUI.

3.3.1 (17/06/2015)

  • Fixed a problem that prevented FDR3 from being opened under Windows.
  • Added support for a new machine-readable output format, framed_json (refines --format).
  • Added a new method reveal_taus_in_trace to the DebugContext object in the API.

3.3.0 (15/06/2015)

  • Greatly improved performance when evaluating CSPM. 3.3.0 can evaluate CSPM scripts in half the time that FDR 3.2.0 could.
  • Added a new assertion, intended for unit-testing, to assert that a machine has a trace.
  • Refinement checking performance has been further improved on large machines with 16 or more cores; checks can be between 10-20% faster.
  • Added a new time-sampling profiler for CSPM that replaces the previous profiler.
  • Removed popovers from various places in the GUI. They have been replaced by a combination of easier-to-use windows.
  • Updated to QT5 which fixes various issues with the GUI.
  • API: added support for dynamically created assertions.
  • API: fixed the hash implementation on various objects.
  • Added a new built-in process, RUN.
  • Added a new built-in process, DIV.
  • Added a new operator Project that is like Hide, but instead allows you to specify what events should be left unhidden, rather than what must be hidden.
  • Added a new flag refines --reveal-taus to the command-line version that prints the visible event corresponding to any tau in a counterexample trace that resulted from a hiding.
  • Banned the use of Double Pattern within prefix statements, due to the complexity of correctly and efficiently supporting it.
  • Renamed the type constraint Inputable to Complete.
  • Fixes several performance issues with very large renamings, and with calls to CHAOS(X) where X is very large.
  • Fixed two issues with the low-level version of Alphabetised Parallel.
  • Fixed a issue on Windows whereby the command line version would appear to finish early and would give the wrong return code.
  • Fixed an issue with Probe where it would appear to hang.
  • Fixes several issues where type-incorrect scripts would pass the typechecker.
  • Fixed a crash during division of some chase counterexamples.
  • Fixed a crash that could occur compiling complex processes using the recursive high-level strategy.

3.2.1 – 3.2.3 (06/01/2015)

  • Fixed an issue that prevented graphs from being viewed under Linux and Mac OS.
  • Fixed a performance problem with compiling certain large non-recursive processes.
  • Fixed a issue that prevented type signatures that used datatypes from being used.

3.2.0 (30/01/2015)

  • Added an beta Windows release, which is compatible with Windows 7 and above.
  • Vastly improved partial-order reduction performance. This improves the performance by at least one order of magnitude. On certain examples, the performance improvements is two orders of magnitude.
  • The performance of dbisim and wbisim has been improved by a factor of 2-4, depending on the example.
  • Added a machine structure viewer to the user interface that shows the structure of a process.
  • Added a communication graph viewer that allows the communication graph of a process to be visualised.
  • Added a new version of prioritise, prioritisepo that takes a partial order to prioritise the events over.
  • Added a function mapDelete that deletes a key from a map.
  • Changed the machine-readable command-line interface to also serialise the results of evaluating print statements Print Statements.

Bug Fixes:

  • Fixed a bug that prevented the C++ API being used under Mac OS X.
  • Improve the compiler performance on certain examples with nested uses of the sequential composition operator.
  • Fix some problems with the deduction of which MPI version is being used.
  • Fixed a bug where the cluster version would never terminate if counterexamples were not being tracked.
  • Fixed parsing of string literals.
  • Fixed pretty-printing of map values.
  • Fixed a bug where type signatures that were too liberal were erroneously accepted.
  • Fixed a bug with pattern matching of complex nested datatypes.
  • Fixed a bug that occurred when parametrised modules were instantiated with the wrong number of arguments.
  • Fixed a bug that occurred when subtypes were instantiated with the wrong number of arguments.
  • Fixed type-checking of parameterless modules in various obscure cases.
  • Fixed an issue that caused terms of the form chase(chase(...(chase(P)...) to appear when probing chase(P).

3.1.0 (11/08/2014)

Major New Features:

  • Added a cluster based refinement-checking algorithm that is able to scale linearly to clusters of at least 1024 cores, providing a suitable interconnect is available. See Cluster Refinement Checking for further details.
  • An API for C++, Java, and Python has been made available, allowing FDR to be easily embedded into external tools.
  • Added a function failure_watchdog that constructs the failures watchdog for the given specification process.
  • Added a function trace_watchdog that constructs the trace watchdog for the given specification process.
  • Improved the output of the type checker so that it provides more useufl information regarding why a program is type incorrect.

Performance Improvements:

  • Reduced the runtime for FDR across a range of problems by between 25 and 50%.
  • Improved the performance of FDR on machines with 8 or more cores by between 10 and 20 percent, depending on the problem and the machine. After this change we have observed FDR3 scaling linearly to 40 cores.
  • For some problems, reduced the memory consumption by 25%.
  • For deadlock freedom and divergence freedom assertions, reduced the runtime by anywhere between 10 and 80%.
  • Improved the performance of explicate by a factor of 3.
  • Improved the performance and memory usage of the on-disk storage engine.

Miscellaneous Features:

  • Added experimental support for partial order reduction which can automatically reduce the state space size on some problems. See Partial Order Reduction for more details.
  • Added an refines --archive that archives all CSP files required to load a particular CSP file into a single, easy to transfer file.
  • Improved counterexample division so more counterexamples can be divided.
  • Added an option refinement.track_history that allows history tracking to be disabled. This will mean that FDR consumes less memory at the cost of not being able to reconstruct counterexamples if an error is found.
  • Modified the option refinement.storage.file.path to allow a comma-separated list of paths to be specified. FDR evenly distributes writes over the paths that have sufficient space available.

Bug Fixes:

  • Fixed an issue that prevented graphs containing tick from being rendered under Linux.
  • Fixed a crash that would randomly occur when an assertion was started.
  • Fixed a bug that caused a crash when a compressed process was probed when debugging a refinement check.
  • Fixed performance issues that could arise when given extremely large CSP files with over 100,000 lines of code.
  • Fixed a memory usage issue with very long running checks.
  • Fixed several problems with type-checking parameterised modules.
  • Fixed an issue that would cause FDR to go into an infinite loop when compiling some processes with lots of singleton taus.

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.