Line 90: | Line 90: | ||

* `transparent f` where f is a unary function which will then on be ignored by ProB | * `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_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 | * `{-# assert_ctl "f" "comment" #-}` where ''f'' is a CTL-formula and ''comment'' is an arbitrary comment, which is optional |

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 = ProcessExpression`

- `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`

- `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

- `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

- `-- comment until end of line`
- `{- arbitrary comment -}`

- `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