CSP-M Syntax - Revision history

Ivaylo Dobrikov: /* PRAGMAS */

2015-07-21T11:56:44Z

PRAGMAS

← Older revision		Revision as of 11:56, 21 July 2015
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 an CTL-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

Ivaylo Dobrikov: /* PRAGMAS */

2015-07-21T11:56:14Z

PRAGMAS

← Older revision		Revision as of 11:56, 21 July 2015
Line 89:		Line 89:
	== PRAGMAS ==		== PRAGMAS ==
	* `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_ctl "f" "comment" #-}` where ''f'' is an CTL-formula and ''comment'' is an arbitrary comment, which is optional

Jens Bendisposto at 15:17, 18 January 2010

2010-01-18T15:17:21Z

← Older revision		Revision as of 15:17, 18 January 2010
Line 1:		Line 1:
	~~--NOTOC__~~		__NOTOC__
	= Details of supported CSP-M syntax =		= Details of supported CSP-M syntax =

Jens Bendisposto at 15:17, 18 January 2010

2010-01-18T15:17:07Z

← Older revision		Revision as of 15:17, 18 January 2010
Line 1:		Line 1:
			--NOTOC__
	= Details of supported CSP-M syntax =		= Details of supported CSP-M syntax =

Jens Bendisposto: Created page with '= 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 cur…'

2010-01-18T15:16:47Z

Created page with '= 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 cur…'

New page

= 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