CSP-M Syntax

Details of supported 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
  • `{-# assert_ltl "f" "comment" #-}` where f is an LTL-formula and comment is an arbitrary comment, which is optional
  • `{-# assert_ctl "f" "comment" #-}` where f is a CTL-formula and comment is an arbitrary comment, which is optional