This page explains the input language of the SCOOP tool. It corresponds to prCRL, a probabilistic process-algebraic
language that was introduced in the paper

Additionally, since recently SCOOP is enable to deal with MAPA specification (a paper on this is work-in-progress). This language is precisely the same as prCRL, except that it additionally allows Markovian actions. Below we will indicate the additions of MAPA with respect to prCRL.### Processes

The main part of a specification contains
of a definition of processes.
Each process is of the form
`X` is the process' name, and `a`, `b`, and `c` are process variables of the
types `A`, `B`, and `C`, respectively. These types can
be a range of integers of the form `{i..j}`, `Bool`, or a user-defined type.
The section on data specification below goes into more details.
Finally, `RHS` is the so-called right-hand side of the process,
defining its behaviour by means of a process term.

Several processes can be specified in the same input file, by just placing several of the above-mentioned process specifications below each other. Obviously, each process should have a unique name.### Process terms

The behaviour of each process is defined by a process term. We allow
the following basic constructs (where `p` and `q` are also process terms):

So, an example of a process definition could be:`x` is `T`, this process may write its variable `y`.
After each write, `x` becomes `F` (false) with probability 1/2 and stays `T` with
probability 1/2. Moreover, at any point in time the process might output any number between
10 and 20 and leave the values of `x` and `y` untouched.
### Expressions

As already indiced above, expressions are used quite often when defining a
process. They can be used to either specify an actual parameter of a process instantiation,
a condition, an action parameter, or a probability distribution. Basically,
each expression is either a variable name or constant (denoted by a single string),
or a function application (denoted by a string followed by a list of expressions
in a comma-separated list between parentheses):
`T` and `F`) and numbers (denoted by either an integer (`17`), fraction (`3/7`), or float (`0.25`)).
Additionally, SCOOP supports queues and vectors over the basic data values (with `empty` as the basic empty queue/vector).

There are several built-in functions that can be used in expressions. The following functions all take two number-valued expressions, and result in a number:

The following functions take two number-valued expressions, and result in a boolean value:

The following functions take any number of boolean-valued expressions, and result in a boolean value:

The following function takes one boolean-valued expression, and result in a boolean value:

The following function takes one boolean-valued expression and two arbitrary arguments:

The following function takes any number of boolean-valued expressions, and results in a number:

The following function takes any number of pairs of boolean-valued expressions and numbers, and results in a number:

Finally, the following function can be applied to any two arguments:

For modelling ease, we support the following in-fix operators as synonyms for many of the functions above:`x > y > z` is not a valid expression).

The following functions can be used to work with queues/lists (adding an element puts in on top, so head(add(q,e)) = e):

As we will see below, the user can define additional functions. (Note that, however, in that case the translation to PRISM does not work anymore, as it does not support more functions than these.)### Data specification

**Data types**

By default, SCOOP can handle the data types`Bool`, `{i..j}` (for any integers `i <= j`) and `Queue`.
However, for ease of modelling we allow the user to define additional data types and functions
on them. Data types can either be of the form `{i..j}`, or a list of strings.
They are defined using the keyword `type`:
**Functions**

For any of the types that were either built-in or user-defined, additional functions can be provided. This functionality is still quite basic: we only allow a function to be defined by listing its complete mapping using the keyword`function`. When defining a function for more
than more argument, they are separated by an asterisk:
**Constants**

Additionally, we allow to specify constants:`type Data = {1..D}`), as well as in other constants that are defined below them in the specification.
Constants don't have to be closed expressions; they can be expressions that can only be evaluated in a context. For instance,
we can define `constant C = x > 4` and in a process definition use `sum(x:Die, C => ...`).

We also support constants that are process specific, as will be discussed below in the "Putting it all together" section.### Putting it all together

The above ingredients can be used to model some system. For this, the input
file should contain at least a list of processes and an initial state.
Moreover, information about hiding, renaming, encapsulation and communication can be provided.

**Hiding, renaming, encapsulation and communication**

As defined in the ACSD-paper as*extended prCRL*, we also allow
hiding, renaming, encapsulation and communication.

To signal that actions can communicate (in ACP style), provide a list of the following format to denote that the action`send` and `receive`
may occur at the same time and be visible as an `interact` action,
and for `read` and `write` can occur as `correspond`:
`send` and `receive` action,
any pair of them can communicate. There will not be any synchronisation by
more than two processes (for this, see the alternative method of parallel composition below).

Hiding renames certain actions to`tau`, and is performed on the final LPPE by including in the specification something like:
`rename` operator in the initial state definition, as defined below.

**Initial state**

An initial process should be provided, indicating the initial conditions for the specification, and defined using the`init` command. We allow several
processes to be provided, to denote that they should all be executed in parallel:

We also allow hiding, renaming and encapsulation to be defined within the initial state definition, hiding, renaming or encapsulating only for a subset of the parallel processes (corresponding to the way introduced in the paper):**Process-specific constants**

We also allow constants that are specific to a single process. Consider for instance the following specification:`mutex` case study.

**Alternative method of parallel composition**

Instead of composition processes in parallel in the manner described above (ACP style), it is also possible to apply CSP-style parallel composition (by using the`-shared` flag, as
described on the 'features' page). That way, all shared actions
are forced to communicate. Also if more than two processes share an action,
they are all forced to synchronise on it together.

This method can even be combined with communication of different actions by the method described above, as for instance in this example:`a` action, resulting in a combined `a` action.
Then, they synchronise on their `b` and `c` action, yielding a `d` action.
Hence, this system produces the trace `a, d, a, d, ...`.
### Global variables

For ease of modelling in the presence of parallel composition, we support global variables.
These variables will be added to the (M)LPPE after parallel composition, and are therefore shared by all processes.
They can be declared as follows:
`n`, of type `{1..6}` and with initial value `1`. It can then be used in
process descriptions in the same way as any other variable:
`setGlobal`:
`print(1), tau, print(2), tau, print(2), tau, ...`.
For more efficiency, an update of global variables can also be assigned to a visible action, as follows:
`print(1,1), print(2,2), print(2,2), ...` and does not have any internal transitions anymore.

If two parallel processes communicatie on an action, their individual updates of the global variables are merged. For instance, consider the following example:`print(1,1), printX(2,2), printY(2,2)`
and `print(1,1), printY(2,2), printX(2,2)`. Clearly, things go wrong
if both processes update the same global variable and try to assign it
different values; in that case, an error message is shown.
### Syntactic sugar

For ease of modelling, some syntactic sugar can be used:

### Extra meta information for IMCA export

When exporting to the input format of the IMCA tool, a set of states
should be specified (to compute the expected reachability time
for, for instance). This can be achieved by using the `reach` command
in a prCRL of MAPA specification. It takes a number of actions and/or rates,
and is used while generating the IMCA input to select as goal states
all states that enable at least one of these actions/rates:

Alternatively, you can use the`reachCondition` command. Instead of taking a list of actions,
this command takes a boolean expression. Then, the goal states of the MA
in the IMCA output will be all states that satisfy this condition:
`reach` and `reachCondition` are used, the union
of the goal states they produce will be used.
### Extra meta information for PRISM export

When exporting an LPPE to a PRISM model (**not possible for MAPA specifications**), it might be necessary to supply additional information
to SCOOP in order to be able to verify properties. The language allows the user
to list a number of actions, which will be made into boolean state variables of the PRISM model.
These variables will be set to "True" directly after a transition corresponding to the action,
and set back to "False" after every other transition. Moreover, after a transition of an
observable action `act`, another state variable `actValue` will be set to the parameter
of the action. For this, the following information should be provided in the model file:

If you only want to verify a single basic Until formula, you can specify this also in the model file, and provide the "-checkuntil" flag to SCOOP. Then, a dedicated observer module will be added to the PRISM model, observing whether or not the until formula is satisfied. For this, you just have to model check for "P=? [F "satisfied" ] in PRISM. In the model, supply for instance the following formula to check that no leader action occurs before a leader(1) action is observed:### Restrictions

To support the linearisation process, a few restrictions are in place when
specifying in prCRL. First of all, the algorithms presented in the ACSD-paper
assumed that all variables that are defined in a specification are uniquely named.
SCOOP is a bit more flexible, and only has the following restriction with
respect to this:

Moreover, as SCOOP introduces a variable named`pc` to function as
a program counter, this variable name is restricted. Additionally, the keywords
`init`, `hide`, `encap`, `comm`, `rename`, `function`, `constant`,
`type`, `psum`, `sum`, `bool`, `observe`, and `until`
cannot be use as variable names.
### Examples

"A linear process-algebraic format for probabilistic systems with data" (published at ACSD 2010)

Here we will introduce the precise syntax that is expected by SCOOP. As it is very close to the syntax described in the paper (Definition 2), we refer there for a formal exposition of the semantics.Additionally, since recently SCOOP is enable to deal with MAPA specification (a paper on this is work-in-progress). This language is precisely the same as prCRL, except that it additionally allows Markovian actions. Below we will indicate the additions of MAPA with respect to prCRL.

- X(a:A, b:B, c:C) = RHS

Several processes can be specified in the same input file, by just placing several of the above-mentioned process specifications below each other. Obviously, each process should have a unique name.

X[x,y] | Instantiate the process X, where the actual parameters are given by the expressions x and y (so the types of x and y should correspond to the types of the process variables of the process X). | |

X[a := x, b := y] | Instantiate the process X, where the process parameter a is instantiated by the expression x, and b is instantiated by the expression y (so the types of x and y should correspond to the types of a and b). It is not required to specify the value of every parameter; the unspecified will then just remain unchanged. | |

c => p | Behave as p in case the expression c evaluates to T (true), otherwise do nothing (so c should be boolean). | |

p ++ q | Nondeterministically behave as either p or q. | |

sum(d:D, p) | Nondeterministically choose a value for variable d of type D, and then behave as p (which may contain this variable; in that case, the chosen value is substituted). | |

a(b,c).psum(d:D, f : p) | Do the interactive action a (parameterised by the expressions b and c), probabilistically choose a value for variable d of type D, and behave as p (which may contain the variable d; in that case, the chosen value is substituted). Each value of type D has a probability to be chosen determined by f (an expression that may contain d; again, in that case the chosen value will be substituted). | |

<lambda>.p | Do the Markovian action lambda, and then behave as p. (only in MAPA) |

So, an example of a process definition could be:

- X(x:Bool, y:{1..3}) = x => write(y) . psum(p:Bool, 1/2 : X[p,y])

++ sum(z:{10..20}, write(z) . psum(i:{1..1}, 1 : X[x,y]))

- x
- T
- 27
- plus(a,6)
- and(eq(y,3), not(leq(z,x)))
- size(add(q, hello))

There are several built-in functions that can be used in expressions. The following functions all take two number-valued expressions, and result in a number:

plus(m,n) | Adds two numbers m, n. | |

minus(m,n) | Subtracts a number n from a number m. | |

multiply(m,n) | Multiplies two numbers m, n. | |

divide(m,n) | Divides a number m by a number n. | |

power(m,n) | Takes the nth power of a number n. | |

min(m,n) | Takes the minimum of two numbers m, n. | |

max(m,n) | Takes the maximum of two numbers m, n. | |

mod(m,n) | Computes a number m modulo a number n (for this, both should be integer). |

The following functions take two number-valued expressions, and result in a boolean value:

leq(m,n) | Checks whether m is smaller than or equal to n. | |

lt(m,n) | Checks whether m is smaller than n. | |

geq(m,n) | Checks whether m is greater than or equal to n. | |

gt(m,n) | Checks whether m is greater than n. | |

eq(m,n) | Checks whether m is equal to n (where, for instance, 5 is considered to be equal to 5.0 and to 20/4). |

The following functions take any number of boolean-valued expressions, and result in a boolean value:

and(a,...,z) | Checks whether a, ..., z all evaluate to T. | |

or(a,...,z) | Checks whether at least one of a, ..., z evaluates to T. |

The following function takes one boolean-valued expression, and result in a boolean value:

not(a) | Checks whether a evaluates to F. |

The following function takes one boolean-valued expression and two arbitrary arguments:

ifthenelse(a,b,c) | Yields b when a evaluates to T, otherwise it yields c. |

The following function takes any number of boolean-valued expressions, and results in a number:

count(a,...,z) | Yields the number of parameters that are true. |

The following function takes any number of pairs of boolean-valued expressions and numbers, and results in a number:

count(b1,n1,b2,n2 ,...) | Yields the number of parameters b_i that are true, each weighted by n_i. |

Finally, the following function can be applied to any two arguments:

eq(a,b) | Yields T when a and b evaluate to the same thing (syntactically), otherwise it yields F (except when a and b are both numbers; in that case the function behaves a described above, also equating syntactically different but mathematically identical numbers). |

For modelling ease, we support the following in-fix operators as synonyms for many of the functions above:

`^`(`power`)`*`(`multiply`),`/`(`divide`)`+`(`plus`),`-`(`minus`)`<`(`lt`),`<=`(`leq`),`>`(`gt`),`>=`(`geq`)`=`(`eq`),`!=`(`not o eq)``!`(`not`)`&`(`and`)`|`(`or`)

The following functions can be used to work with queues/lists (adding an element puts in on top, so head(add(q,e)) = e):

add(q,e) | Adds the element e to the queue q. | |

add(q,e,n) | Adds n times the element e to the queue q. | |

head(q) | Provides the head of the queue q. | |

tail(q) | Provides the tail of the queue q. | |

get(v,n) | Provides the element of the vector v at position n. | |

set(v,n,e) | Changes the element of the vector v at position n to e. | |

size(q) | Computes the size of the queue/vector q. |

As we will see below, the user can define additional functions. (Note that, however, in that case the translation to PRISM does not work anymore, as it does not support more functions than these.)

By default, SCOOP can handle the data types

- type Die = {1..6}
- type Ids = (one, two, three)

For any of the types that were either built-in or user-defined, additional functions can be provided. This functionality is still quite basic: we only allow a function to be defined by listing its complete mapping using the keyword

- function next = (one -> two, two -> three, three -> one)
- function power = (1*1 -> 1, 1*2 -> 1, 1*3 -> 1,

2*1 -> 2, 2*2 -> 4, 2*3 -> 8)

3*1 -> 3, 3*2 -> 9, 3*3 -> 27)

Additionally, we allow to specify constants:

- constant N = 5

We also support constants that are process specific, as will be discussed below in the "Putting it all together" section.

As defined in the ACSD-paper as

To signal that actions can communicate (in ACP style), provide a list of the following format to denote that the action

- comm (send, receive, interact), (read, write, correspond)

Hiding renames certain actions to

- hide send, receive

- encap putInChannel, getFromChannel

- rename (send, receive), (drop, timeout)

An initial process should be provided, indicating the initial conditions for the specification, and defined using the

- init X[1,2] || Y[] || Z[one]

We also allow hiding, renaming and encapsulation to be defined within the initial state definition, hiding, renaming or encapsulating only for a subset of the parallel processes (corresponding to the way introduced in the paper):

- init hide(send, receive: W[] || X[]) || encap(test : hide(throw : Y[] || rename((a,b) : Z[])))

We also allow constants that are specific to a single process. Consider for instance the following specification:

- X = print(name).X[]
- init X(name=proc1) || X(name=proc2)

Instead of composition processes in parallel in the manner described above (ACP style), it is also possible to apply CSP-style parallel composition (by using the

This method can even be combined with communication of different actions by the method described above, as for instance in this example:

- X = a.b.X[]
- Y = a.c.Y[]
- init X || Y
- comm (b,c,d)
- encap b,c

- global n : {1..6} = 1

- X = print(n).X[]

- X = print(n).setGlobal(n,2).X[]

- global n:{1..2} = 1
- global m:{1..2} = 1
- X = print(n,m){n := 2, m := 2} . print(n,m) . X[]
- init X

If two parallel processes communicatie on an action, their individual updates of the global variables are merged. For instance, consider the following example:

- global n:{1..2} = 1
- global m:{1..2} = 1
- X = print1(n,m){n := 2} . printX(n,m).X[]
- Y = print2(n,m){m := 2}. printY(n,m).X[]
- init X || Y
- comm (print1,print2,print)
- encap print1, print2

Notation | Short for | |

a | a() | |

a(b,c).p | a(b,c).psum(i0:{1..1}, 1 : p) | |

a(b,c).psum(p1 -> p ++ ... ++ pn -> r) | a(b,c).psum(i0:{1..n}, ifthenelse(eq(i0,1),p1,...) : ifthenelse(eq(i0,1),p,...)) |

- reach leader(1), <5>

Alternatively, you can use the

- reachCondition (x > 2 & y < 5) | z = 10

- observe leader : {1..2}

If you only want to verify a single basic Until formula, you can specify this also in the model file, and provide the "-checkuntil" flag to SCOOP. Then, a dedicated observer module will be added to the PRISM model, observing whether or not the until formula is satisfied. For this, you just have to model check for "P=? [F "satisfied" ] in PRISM. In the model, supply for instance the following formula to check that no leader action occurs before a leader(1) action is observed:

- until [ !(leader) U leader(1) ]

- It is not allowed to have a condition containing some variable
`d`being immediately followed by a summation that re-binds`d`(either directly, or by instantiating a process that does so in the first step). - It is not allowed to bind a variable name to more than one type (in two processes that can reach each other).

Moreover, as SCOOP introduces a variable named

- The Itah-Rodeh leader election protocol (prCRL)
- The Franklin leader election protocol (prCRL)
- The sliding window protocol (prCRL)
- A simple die-throwing game (prCRL)
- Knuth's die-simulating coin (prCRL)
- A perfect strategy for roulette? (prCRL)
- A nondeterministic polling system (MAPA)
- A mutual exclusion protocol (MAPA)