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.