Help

CSP-M: Difference between revisions
(Update paper link)
 
(12 intermediate revisions by 4 users not shown)
Line 1: Line 1:
[[Category:User Manual]]
[[Category:User Manual]]
__NOTOC__
__NOTOC__
ProB supports machine readable CSP<ref>M. Butler and M. Leuschel: ''Combining CSP and B for specification and property verification''. FM 2005, LNCS 3582, Springer-Verlag, 2005 [http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=1]</ref>, 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".
ProB supports machine readable CSP<ref>M. Butler and M. Leuschel: ''Combining CSP and B for specification and property verification''. FM 2005, LNCS 3582, Springer-Verlag, 2005 [https://www3.hhu.de/stups/downloads/pdf/LeBu05_1.pdf]</ref> 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:
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:
* use CSP file: uses the CSP file to control the current B machine (see below)
* 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
* use default CSP file: trys to use a CSP with the same name as the current B machine to control it
Line 10: Line 10:


ProB now supports FDR and ProBE compatible CSP-M syntax, with the following outstanding issues
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
* currying and lambda expressions have only been partially tested
* extensions and productions are not yet supported (but {| |} is)
* extensions and productions are not yet supported (but {| |} is)
* mixing of closure with other set operations (especially diff) not yet fully supported
* the priority of rename compared to external choice is unfortunately different than in FDR; please use parentheses
* 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.
* mixing of closure with other set operations (especially diff) is not yet fully supported
* 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}.
* 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 but 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).
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).


== Guiding B Machines with CSP ==
== Guiding B Machines with CSP ==
Line 26: Line 26:
The CSP file should define a process called "MAIN".
The CSP file should define a process called "MAIN".
This process will be executed in parallel with the B machine.
This process will be executed in parallel with the B machine.
The synchronisation between the B machine and the CSP specification is as follows:
The synchronization 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:<pre> CSP [| {op1,...,opn} |] B</pre> where op1,...,opn are the visible operations defined in the B machine.
* CSP events that have the same name as B Operations will synchronize 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:<pre> CSP [| {op1,...,opn} |] B</pre> where op1,...,opn are the visible operations defined in the B machine.
* CSP events do not need to provide all arguments of B operations:  
* CSP events do not need to provide all arguments of B operations:  
  add!1 -> will match add(1,1) or add(1,2) or ...  
  add!1 -> will match add(1,1) or add(1,2) or ...  
Line 33: Line 33:
  add -> will match add(1,2), add(2,1), ...  
  add -> will match add(1,2), add(2,1), ...  
  add!1!2 -> will only match add(1,2)</pre>
  add!1!2 -> will only match add(1,2)</pre>
* B Output arguments are specified at the end
* B Output arguments are specified at the end<pre>lookup!X!2 will match lookup(X) --> 2</pre>Note 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.
lookup!X!2 will match lookup(X) --> 2
* If you have a variable called vv, then you can use vv?VAL to get the value of vv. You can also use, for example, 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. For example, use vv!3?Y to check whether tuples (3,Y) are in the relation vv (there will be one possible synchronisation per such value).
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
* see the file "bookstore_guide.csp" in the provided Machines directory for an example.
    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.


== Details of supported CSP-M syntax ==
For the syntax definition see [[CSP-M Syntax]]
 
Note: you can use the command "Summary of CSP syntax" in ProB's help menu
to get an up-to-date list of the supported syntax, along with current limitations.
 
=== PROCESS DEFINITIONS ===
* `Process = ProcessExpression`
 
=== PROCESS EXPRESSIONS ===
* `STOP`      deadlocking process
* `SKIP`      terminating process
* `CHAOS(a)` a: set of channel expressions
 
* `ch->P`    simple action prefix where ch is a channel name possibly followed
            by a sequence of outputs "!v" and input "?VAR", where v is a value
            expression and VAR a variable identifier
* `ch?x:v->P` action prefix with set of accepted values
 
* `P ; Q`    sequential composition
* `P ||| Q`  interleaving
 
* `P [] Q`    external choice
* `P |~| Q`  internal choice
 
* `P /\ Q`    interrupt
* `p [> Q`    untimed timeout
 
* `P [| a |] Q`      parallel composition with synchronisation on set of channel expressions a
* `P [ a || a' ] Q`  alphabetised parallel
* `P [ c<->c' ] Q`  linked parallel
* `P \ a`            hiding of channel expressions in c
* `P [[ c<-c' ]]`    renaming of channels c into c'
 
* `if B then P else Q`
 
* `b & P`    guard using a boolean expression b
 
* `[]x:v@P`      replicated external choice (x: variable, v: set value expression)
* `|~|x:v@P`      replicated internal choice (x: variable, v: set value expression)
* `|||x:v@P`      replicated interleave (x: variable, v: set value expression)
* `;x:s@P`        replicated sequential composition (s: sequence expression)
* `||x:v@[a']P`  replicated alphabetised parallel
* `[| a |]x:s@P`  replicated sharing
* `[c<->c']x:s@P` replicated linked parallel (sequence s must be non empty)
 
* `let  f1=E1 ... fk=Ek within P` 
=== BOOLEAN EXPRESSIONS ===
*  `true`
*  `false`
* `b1 and b2`    (`b1 && b2` also accepted but not in CSP-M)
* `b1 or b2`    (`b1 || b2` also accepted but not in CSP-M)
* `b1 <=> b2`    equivalence
* `b1 => b2`    implication
* `not b`
* `v==w`        equality of values
* `v!=w`        disequality of values
* `v<w,v>w`    strict ordering
* `v<=w,v>=w`  non-strict ordering  (v=<w also accepted)
 
* `member(v,w)` set membership check
* `empty(a)`    set emptiness check
 
* `null(s)`    sequence emptiness check
* `elem(x,s)`  sequence member check
 
=== VALUE EXPRESSIONS ===
* `v+w`, `v-w`    addition and subtraction
* `v*w`        multiplication
* `v/w`        integer division
* `v % w`      division remainder
 
* `bool(b)`    convert a boolean expression into a boolean value
 
* `{v,w,...}`  enumerated sets
* `{m..n}`      closed range
* `{m..}`      open range
* `union(v,w)`  set union
* `inter(v,w)`  set intersection
* `diff(v,w)`  set difference
* `Union(A)`    generalized union of a set of sets
* `Inter(A)`    generalized intersection
* `card(a)`    cardinality of a
* `{x1,...,xn | x<-a,b}`
* `Events`      all channel expressions on all declared channels
* `{| ... |}`  closure of set of channel expressions
* `Set(a)`   all subsets of a
 
 
* `<>`          empty sequence
* `<v,w,...>`  explicit sequence
* `<m..n>`      closed range sequence
* `<m..>`      open range sequence
* `<....>^s`    sequence concatenation (first or last arg has to be an explicit sequence for patterns)
* `#s`, `length(s)`
* `head(s)`
* `tail(s)`
* `concat(s)`
* `set(s)`      convert sequence into set
 
=== COMMENTS ===
* `-- comment until end of line`
* `{-  arbitrary comment -}`
 
=== PRAGMAS ===
* `transparent f`  where f is a unary function which will then on be ignored by ProB


====== Command Line option for guided CSP||B ======
From the command line, you can specify a CSP File that should be used to guide the B machine with
-csp-guide <Filename>
(This feature is included since version 1.3.5-beta7.)


== References ==
== References ==
<references />
<references />

Latest revision as of 15:33, 4 February 2021


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:

  • 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

  • currying and lambda expressions have only been partially tested
  • extensions and productions are not yet supported (but {| |} is)
  • the priority of rename compared to external choice is unfortunately different than in FDR; please use parentheses
  • mixing of closure with other set operations (especially diff) is 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 but 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 synchronization 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 synchronization between the B machine and the CSP specification is as follows:

  • CSP events that have the same name as B Operations will synchronize 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, 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.
  • If you have a variable called vv, then you can use vv?VAL to get the value of vv. You can also use, for example, 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. For example, use 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

Command Line option for guided CSP||B

From the command line, you can specify a CSP File that should be used to guide the B machine with 

-csp-guide <Filename>

(This feature is included since version 1.3.5-beta7.)

References

  1. ↑ M. Butler and M. Leuschel: Combining CSP and B for specification and property verification. FM 2005, LNCS 3582, Springer-Verlag, 2005 [1]
Retrieved from "https://prob.hhu.de/w/index.php?title=CSP-M&oldid=4765"