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