Input language of the SCOOP tool

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

       "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.

Processes

The main part of a specification contains of a definition of processes. Each process is of the form
  • X(a:A, b:B, c:C) = RHS
where 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):
   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 => pBehave as p in case the expression c evaluates to T (true), otherwise do nothing (so c should be boolean).
p ++ qNondeterministically 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>.pDo 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]))
As long as its variable 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):
  • x
  • T
  • 27
  • plus(a,6)
  • and(eq(y,3), not(leq(z,x)))
  • size(add(q, hello))
The basic data values are booleans (denoted by 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:
   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)
Here, the order of the list denotes the precedence of the operators (all operators on the same line have the same precedence). All operators are left-associative, except for the boolean comparators that are not associative at all (so 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):
   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.)

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:
  • type Die = {1..6}
  • type Ids = (one, two, three)
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:
  • 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)
Constants
Additionally, we allow to specify constants:
  • constant N = 5
Constants can be used in type definitions (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:
  • comm  (send, receive, interact), (read, write, correspond)
If there are several processes that enable a 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:
  • hide  send, receive
To encapsulate actions (i.e., disable them), just add:
  • encap  putInChannel, getFromChannel
To rename actions, you can use:
  • rename  (send, receive), (drop, timeout)
This global renaming occurs after parallel composition; it can therefore not be used for synchronisation. To apply renaming of a single process, use the 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:
  • init X[1,2] || Y[] || Z[one]
Note that for processes having parameters, an initial value for these variables should be provided.

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[])))
Process-specific constants
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)
This can for instance come in handy if there are several identical processes, that want to communicate their state via global variables and need to know which global variable is their own. See for instance the 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:
  • X = a.b.X[]
  • Y = a.c.Y[]

  • init X || Y
  • comm (b,c,d)
  • encap b,c
Here, first the two processes synchronise on the 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:
  • global n : {1..6} = 1
This yields a global variable named 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:
  • X = print(n).X[]
Global variables can be updated using a special action setGlobal:
  • X = print(n).setGlobal(n,2).X[]
It yields a tau-transition that changes the value of the global variable to the specified value. Hence, the example above models a system that outputs 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:
  • global n:{1..2} = 1
  • global m:{1..2} = 1

  • X = print(n,m){n := 2, m := 2} . print(n,m) . X[]

  • init X
This way, the system just outputs 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:
  • 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
This system yields the traces 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:

   Notation                                        Short for
   aa()
   a(b,c).pa(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,...))

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:
  • reach leader(1), <5>
Note that, if in some state s1 there are two Markovian transitions to one state s2, their rates are added and only one transition between s0 and s1 will appear in the IMCA output. Therefore, these individual rates are not present anymore, and will not yield goal states when used in a reach command.

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:
  • reachCondition (x > 2 & y < 5) | z = 10
If both 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:
  • observe leader : {1..2}
Note that a type should also be mentioned, to make sure that SCOOP is able to provide the right information to PRISM. To observe more than one action, just provide several of these statements.

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) ]

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:
  • 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).
Violation of either of these rules will be detected during linearisation, and an appropriate error message will be provided. To keep the algorithm as close to the paper as possible, and to not have the resulting LPPE deviate from the specification too much, a suggestion to rename the variables is made (instead of doing this automatically).

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