# User Manual

## Model formulation

Models are given in an extended version of
the `PRISM`

language. For an overview of the `PRISM`

language,
please refere to their homepage. `PARAM`

extends
the `PRISM`

language by the possibility to specify a
`<parameter>`

via

param float <parameter>;

and later usage of such parameters in the probability distributions
in the commands of the model. In `PARAM`

2, parameters can
be assigned an interval `[<p1>,...,<p2>]`

of valid
values using the syntax

param <parameter> : [<p1>..<p2>];

By default, the interval is assumed to be `[0,1]`

.

`PARAM`

1 supports discrete-time Markov chains and a
(with some restrictions) continuous-time Markov chains. `PARAM`

2 also support discrete-time Markov decision processes. We also allow
the definition of reward structures, but the usage for several reward
structures is not supported for earlier versions of `PARAM`

.

Properties are given in PCTL using the notion of `PRISM`

`PARAM`

1 supports non-nested PCTL formulae of the
following form, where <A> and <B> are expressions over the model
variables and <bound> is a natural number:

`P=? [ <A> U <B> ]`

(unbounded until)`P=? [ <A> U<=<bound> <B> ]`

(bounded until)`R=? [ F <A> ]`

(expected accumulated reward)

For the expected accumulated reward, you must make sure that always
finally the set of states in which `<A>`

holds will
be reached. Otherwise, the result is undefined.

`PARAM`

2 also supports nested PCTL. We aim at completeness
there, however as there was only limited testing on the new version,
there are still some restrictions.

## Usage

`PARAM`

is invoked from the command line by

<param> <model-file> <property-file> <options>

where `<param>`

is the command to start `PARAM`

,
`<model-file>`

is the model file and
`<property-file>`

is the formula file, with the
restrictions described above. Depending on the `PARAM`

version, there are different possible options for <options>. Please
use

<param> --help

to print a list of available options. Notice that the set of command line
options is not stable, and new command line options may be added or existing
ones changed, as the development of the tool continues. After calling
`PARAM`

, the result of the analysis is written to the file
`result.out`

, if not specified differently.