CSP-M

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" submenu of the File menu:

• use CSP file: uses the CSP file to control the current B machine (see below)
• use default CSP file: trys to use a CSP with the same name as the current B machine to control it

Limitations of CSP-M Support

ProB now supports FDR and ProBE compatible CSP-M syntax, with the following outstanding issues

• assert declarations are ignored
• currying and lambda expressions have only been partially tested
• extensions and productions are not yet supported (but {| |} is)
• mixing of closure with other set operations (especially diff) not yet fully supported
• input patterns can only contain variables,tuples,integers and constants (ch?(x,1) is ok, ch?(y+1,x) not). Also, for a record all arguments must be provided (e.g., for datatype r.Val.Val you have to write r?x?y you cannot write r?xy). Finally, for the moment within "ch? x.y:Set" the ":Set" associates only with y; if you want to check that "x.y" is in Set you need to write: "ch?(x.y):Set.
• channel declarations can either use associative dot tuples or non-associative tuples, not yet both. Also, sets of tuples as channel types will not work the same way as in FDR. I.e., for channel a:LinkData you should not use LinkData = {0.0, 0.1, 1.0, 1.1} but rather nametype LinkData = {0,1}.{0,1}.

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 synchronisation constructs).

Guiding B Machines with CSP

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 synchronisation between the B machine and the CSP specification is as follows:

• CSP events that have the same name as B Operations will synchronise with B; CSP events that have the same name as a B Variable or Constant can be used to inspect the current value of these, all other CSP events can happen independently of B. In CSP terms the CSP and B are composed as follows:

   CSP [| {op1,...,opn} |] B

  where op1,...,opn are the visible operations defined in the B machine.
• CSP events do not need to provide all arguments of B operations:

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)

• B Output arguments are specified at the end

  lookup!X!2 will match lookup(X) --> 2

  Note, however, 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.
• If you have a variable called vv then you can use vv?VAL to get the value of vv. You can also use, e.g., vv!X to check that the value is equal to X. If vv is a relation or function, then you can also use two values on the channel to check for particular tuples in the relation. E.g., vv!3?Y to check whether tuples (3,Y) are in the relation vv (there will be one possible synchronisation per such value).
• see the file "bookstore_guide.csp" in the provided Machines directory for an example.

For the syntax definition see CSP-M Syntax

References