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:
**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:**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:### 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:**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).`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:
### 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:

**Parameter elimination**

To have SCOOP detect and remove parameters that are never used, apply the argument "-parelm":**Dead variable reduction**

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

**Confluence reduction**

We implemented confluence reduction, using the techniques introduced in the TACAS 2011 submission*pairs* of global variables, add the argument "-strong":
**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:### Verbose output

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

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:### Summary

Given a file

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

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

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

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`

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

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`

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`

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

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`

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

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

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

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

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`

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`

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`

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

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

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

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

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`

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

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`

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