Mora

Mora is an automated tool for generating invariants of probabilistic programs. Inputs to Mora are so-called Prob-solvable loops that are probabilistic programs with polynomial assignments over random variables and parametrized distributions. Combining methods from symbolic computation and statistics, Mora computes invariant properties over higher-order moments of loop variables, expressing, for example, statistical properties, such as expected values and variances, over the value distribution of loop variables.

Installation

Mora needs to following dependencies:

Python version ≥ 3.8 and pip
scipy
diofant
lark-parser

To install these you can do the following steps.

Make sure you have python (version ≥ 3.8) and pip installed on your system. Otherwise install it in your preferred way.

Clone the repository:

git clone git@github.com:probing-lab/mora.git
cd mora

Create a virtual environment in the .venv directory:

pip3 install --user virtualenv
python3 -m venv .venv

Activate the virtual environment:
```
source .venv/bin/activate
```

Install the required dependencies with pip:

pip install scipy
pip install diofant==0.11
pip install lark-parser

Run Mora

Having all dependencies installed, you can run Mora for example like this:

python ./run.py --benchmarks benchmarks/binomial --goal 1

If you run the command from the example above, Mora will compute the invariants for the first-order moments (expected values) of the program variables of the program contained in the file benchmarks/binomial.

The general command for running Mora is:

python ./run.py --benchmarks <list of files/file pattern> --goal <list of goals>

A more extensive help can be obtained by:

python ./run.py --help

Run Tests

Automatic tests can be run with

python -m unittest

Writing your own Prob-solvable program

A Prob-solvable program consist of initial assignments (one per line), a loop head while true: and a loop body consisting of multiple variable updates (also one per line). In the variable updates as well as the initial assignments, random variables can be used.

Initial assignments:

format: var = value
comment: not all variables have to have initial value specified
example: x = 123

Random variables:

format: var = RV(distribution, parameter1, [parameter2, ...])
comment: distributions supported at the moment are uniform and gauss
example: u = RV(uniform, 0, 1)

Variable updates:

format: var = option1 @ probability1; option2 @ probability2 ...
comment: last probability can be omitted, it’s assumed to be whatever values is needed for probabilities to sum up to 1.
comment: variables can depend only on previous variables non-linearly, and on itself linearly - e.g. x = x + 1 followed by y = y + x^2 is allowed. However, x = x + y followed by y = y + 1, or x = x^2 is not allowed.
example: x = x @ 1/2; x + u

An example program would be:

# this is a comment
x=0
while true:
    u = RV(uniform, 0, b)
    g = RV(gauss, 0, 1)
    x = x - u @ 1/2; x + u @ 1/2
    y = y + x + g

More examples can be found in the benchmarks folder.