FDR Documentation¶

Welcome to the documentation for FDR 4.2.

FDR is a refinement checker for the process algebra CSP. It allows processes to be defined in a machine-readable version of CSP, CSP_M, and is then able to check various assertions about these processes. FDR includes two main tools:

• The FDR4 tool, which is a graphical program that is able to: load CSP_M files; check assertions about processes including extensive debugging support when an assertion fails; and has a number of additional views that allow CSP processes to be investigated.
• The command line tool is able to simply check assertions from a given CSP_M file. This tools is able to be run on a cluster, enabling massive problems to be tackled. It is also able to produce machine-readable output, which allows FDR to be integrated into other tools.

It also includes a number of utility tools:

• cspmprofiler is a profiler for CSP_M which allows some performance problems with CSP_M scripts to be diagnosed.

The documentation is organised into four main sections.

• The FDR User Interface contains an introduction to the FDR tool itself and gives a thorough overview of the user interface, including a getting-started guide.
• CSPM gives an overview of CSP_M, as supported by FDR, including API documentation for the built-in functions, and documentation of the supported assertions (both their syntax and semantics).
• The FDR Command-Line Interface introduces the command-line tool and explains how FDR can be run on a cluster, enabling massive problems to be tackled.
• integrated documents how FDR can be integrated into other tools.