This page explains the features of SCOOP, that can be invoked by means of command-line arguments. Note that options can be combined, by just providing several arguments. At the end of this page, we summarise all the flags that can be used.

Mode of operation

SCOOP can handle both prCRL (for modelling PAs) and MAPA (for modelling MAs). You need to indicate which mode you want to use, via the flags -pa and -ma. Based on your choice, some other flags are disabled. In the flag summary on the bottom of this page, this is indicated.

Linearising a specification

Displaying the (M)LPPE
Given a file model.prcrl or model.mapa containing a specification according to the correct prCRL or MAPA syntax, the corresponding (M)LPPE is obtained using:

• scoop -pa -lppe < model.prcrl
• scoop -ma -mlppe < model.mapa

By default, the prCRL/MAPA style of parallel composition is used: actions only synchronise if specified as such. To additionally force synchronisation over shared actions, use the "-shared" flag:

• scoop -ma -mlppe -shared < model.prcrl

By default, the (M)LPPE is shown in a user-friendly way, omitting the data specification and displaying only the updates of each process instantiation instead of all its variables. Also, expressions are made more readable by displaying eq(x,y) as x = y, and(x,y) as x & y, etcetera. To obtain the output in the original syntax, such that it could be fed to SCOOP again, use:

• scoop -pa -lppe -prcrl < model.prcrl
• scoop -ma -mlppe -mapa < model.mapa

Exporting to PRISM
To enable symbolic computation of the state space corresponding to the input model, we support exporting an LPPE to the PRISM input language. Note that this only works when the LPPE corresponding to the specification does not contain user-defined functions and only contains (possibly user-defined) data types of the form {i..j} (or boolean). The PRISM input is obtained using:

• scoop -pa -prism < model.prcrl

To add an observer module for an until formula that you provided in the model, use:

• scoop -pa -prism -checkuntil < model.prcrl

Instantiating constants
To support experimenting with different variations of a model, we allow its specification to use constants that are not instantiated in the data part of the model. In this case, the values of the constants should be provided as a command-line argument to SCOOP:

• scoop -pa -lppe -constant-N=3 -constant-K=5 < model.prcrl
• scoop -ma -lppe -constant-N=3 -constant-K=5 < model.mapa

Generating a state space

Properties of the state space
Except just generating an (M)LPPE, SCOOP is also capable of instantiating it to a probabilistic automaton or Markov automaton. When being just curious about the size of the PA or MA, use the following command to obtain the number of states and transitions:

• scoop -pa -size < model.prcrl
• scoop -ma -size < model.mapa

To actually see a list of the states and transitions, issue:

• scoop -pa -statespace < model.prcrl
• scoop -ma -statespace < model.mapa

Exporting the state space
To obtain the state space in the more practical AUT format (for instance, to analyse it using CADP or a similar tool), use either one of the following commands.
In the first case, an actual PA including probabilities is generated due to the "-aut" flag, in the BCG format explained here. Since the BCG format does not support an explicit nondeterministic choice between sets of probabilistic transitions (as is the case for PAs), additional states are introduced to first take a nondeterministic choice between the actions and then in additional states performing the probabilistic choices.
In the second case, using the "-noprob" flag, every probabilistic choice is reinterpreted as a nondeterministic choice, still allowing for instance reachability analysis using standard non-probabilistic tools.
The third example also adds the "-cadp" flag, renaming all tau-actions to i, and rounding down all probabilities (which is needed for analysis with the CADP toolset). The fourth example shows how to export to a PRISM transition matrix using "-trans".
In case the model is deterministic, in the sense that each state enables only one action, it can be interpreted as a DTMC. Using the "-dtmc" flag this is checked, and if used in combination with the "-aut" flag (as in the fifth example), a more efficient AUT file can be generated (in which the additional states, as examples above, are not needed anymore).

• scoop -pa -aut < model.prcrl
• scoop -pa -aut -noprob < model.prcrl
• scoop -pa -aut -cadp < model.prcrl
• scoop -pa -trans < model.prcrl
• scoop -pa -aut -cadp -dtmc < model.prcrl

The first three examples can also be used for MAPA models, obtaining a state space where the rates encoded by an action rate. By default, Markovian transitions in states that also allow interactive transition are omitted, due to the maximal progress assumption. To suppress this feature, use the "-keeprates" flag:

• scoop -ma -aut -keeprates < model.mapa

Finally, it is possible to output the state space of a prCRL or MAPA specification to a format for analysis with the IMCA tool. This tool is enable to handle MAs in their full generality, and can compute expected time to reach, unbounded reachability and long run average. To use this feature, supply a "reach" specification in the model (see the "input language" page) and apply the "-imca" flag:

• scoop -pa -imca < model.mapa
• scoop -ma -imca < model.mapa

Optimisations

Basic reduction techniques
By default, the implementation tries to remove variables that are constant, summations that can only yield a single value, and summands with a condition that can never be satisfied. Moreover, it tries to simplify expression by for example reducing x > 5 & True to x > 5 and plus(2,1) to 3. These techniques can be suppressed by the -nobasics flag:

• scoop -pa -lppe -nobasics < model.prcrl
• scoop -ma -lppe -nobasics < model.mapa

Additionally, parameter elimination, dead variable reduction, confluence reduction, transition merging and maximal progress reduction can be enabled on-demand, as explained below.

Parameter elimination
To have SCOOP detect and remove parameters that are never used, apply the argument "-parelm":

• scoop -pa -lppe -parelm < model.prcrl
• scoop -ma -lppe -parelm < model.mapa

Dead variable reduction
We implemented dead variable reduction, using the techniques introduced in the paper

       "State Space Reduction of Linear Processes Using Control Flow Reconstruction" (published at ATVA 2009)

To apply dead-variable reduction, use the argument "-dead" with either "-mlppe", "-lppe" or "-prism", and/or with one of the state space generation methods:

• scoop -pa -lppe -size -dead < model.prcrl
• scoop -ma -aut -size -dead < model.mapa

Note that dead variable reduction subsumes parameter elimination.

Confluence reduction
We implemented confluence reduction, using the techniques introduced in the TACAS 2011 submission

       "Confluence reduction for probabilistic systems"

To apply confluence reduction, use the argument "-conf" with one of the state space generation methods. Note that, as confluence does not change the LPPE but is used to reduce the state space on the fly during its generation, it has no effect on "-lppe".

• scoop -pa -conf -aut < model.prcrl

To count the number of states and transitions that were visited during state space generation using confluence reduction, issue:

• scoop -pa -conf -visited < model.prcrl

By default, confluence is detected using some fairly simple heuristics, such as checking for each global variable whether or not it has at least one possible value for which two summands are both enabled. To additionally check for independence of summands by checking whether this holds for all pairs of global variables, add the argument "-strong":

• scoop -pa -conf -strong -aut < model.prcrl

In prCRL mode, by default the TACAS 2011 notion of confluence reduction is used. This technique does not preserve divergences, and hence may increase the minimum reachability probabilities. With the "-divergence" flag, a tau-labelled self-loop is added to all representatives that enable a confluence transition. That way, divergences are preserved. In MAPA mode, this feature is enabled by default, since the omission of divergences may suddenly enable rate transitions that were disabled before due to the maximal progress assumption.

• scoop -pa -conf -divergence -aut < model.prcrl

Confluence can also be used together with the "-prism" flag, to make some syntactic optimisations to the PRISM model based on confluence (this feature is still in beta stage). If SCOOP detects that there are possibly cycles of confluent tau summands, this option is not allowed. However, these cycles can be removed using the "-removecycles" flag:

• scoop -pa -prism -conf < model.prcrl
• scoop -pa -prism -conf -removecycles < model.prcrl

Maximal progress reduction (only in MA mode)
If a Markovian summands is only enabled when also at least one interactive summand is enabled, it can be omitted due to the maximal progress assumption. To apply this reduction, use the "-maxprogress" flag:

• scoop -ma -mlppe -maxprogress < model.mapa

Verbose output

Sometimes it might be interesting to get some additional output. For this, issue "-verbose", for instance:

• scoop -pa -conf -verbose < model.prcrl
• scoop -ma -mlppe -verbose < model.mapa

When applied together with "-conf", it shows the summands that were detected to be confluent. Moreover, it is shown whether or not confluence reduction and/or dead variable reduction were used. Also, when applied together with "-lppe" or "-mlppe", it shows the number of summands and parameters, and the (M)LPPE size.

Especially when analysing many models by a script, it might be useful to add the name of the model to the output. For this, besides "-verbose", also "-source" should be used:

• scoop -pa -size -verbose -source=leader-2-16 < model.prcrl
• scoop -ma -size -verbose -source=leader-2-16 < model.mapa

Summary

-pa		Interpret the input as prCRL
-ma		Interpret the input as MAPA
-constant-N=k		Instantiate the constant N by the value k
-size		Output the size of the underlying PA/MA
-statespace		Output the states and transitions of the underlying PA/MA
-aut		Output the underlying PA in probabilistic AUT format
-noprob		Omit probabilities from the AUT format
-cadp		Output probabilities as fractions and rename tau to i
-verbose		Provide more verbose output
-parelm		Apply parameter elimination
-dead		Apply dead variable reduction
-nobasics		Suppress all basic reduction techniques (constant elimination, summation elimination, expression simplification)
-conf		Apply confluence reduction
-strong		Use stronger heuristics when detecting confluence reduction
-removecycles		Remove potential cycles of confluent summands
-visited		Output the number of visited states and transitions
Only in PA mode:
-lppe		Output an LPPE
-prcrl		Use precise prCRL syntax for outputted LPPE
-prism		Output a PRISM model
-checkuntil		Generate a PRISM module to check a PCTL Until formula
-trans		Output the underlying PA as a PRISM transition matrix
-dtmc		Interpret model as DTMC and produce more efficient AUT file
-divergence		Let confluence reduction preserve divergences
Only in MA mode:
-mlppe		Output an MLPPE
-mapa		Use precise MAPA syntax for outputted MLPPE
-keeprates		Do not apply the maximal progress assumption during state space generation
-maxprogress		Apply maximal progress reduction