# 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, CSPM, 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 CSPM 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 CSPM 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 CSPM which allows some performance problems with CSPM scripts to be diagnosed.

The documentation is organised into four main sections.