ProB supports machine readable CSP[1] as supported by FDR and ProBE. CSP files can be animated and model checked on their own simply by opening a file ending with ".csp".
You can also use a CSP file to guide a B machine by first opening the B machine and then using the "Open Special" sub-menu of the File menu:
ProB now supports FDR and ProBE compatible CSP-M syntax, with the following outstanding issues
Also, in the first phase we have striven for compatibility and coverage. We still need to tune the animator and model checker for efficiency (there are few known bottlenecks which will be improved, especially with deeply nested CSP synchronization constructs).
To use this feature of ProB: first open a B Machine, then select "Use CSP File to Guide B..." or "Use Default CSP File" in the "Open Special" submenu of the File menu (you must be in normal user mode to see it).
The CSP file should define a process called "MAIN". This process will be executed in parallel with the B machine. The synchronization between the B machine and the CSP specification is as follows:
CSP [| {op1,...,opn} |] Bwhere op1,...,opn are the visible operations defined in the B machine.
add!1 -> will match add(1,1) or add(1,2) or ... (supposing add has 2 parameters in B) add -> will match add(1,2), add(2,1), ...
add!1!2 -> will only match add(1,2)
lookup!X!2 will match lookup(X) --> 2Note however, that for non-deterministic operations you generally should only retrieve the output value using a ? and not match against it using a !. Otherwise, the non-determinism of the B operation will be treated as an external choice for the CSP. So, if lookup is non-deterministic then we should do lookup!X?Res -> Res=2 & Cont rather than lookup!X!2 -> Cont.
For the syntax definition see CSP-M Syntax