Amber is an academic prototype to decide the probabilistic termination behavior of Prob-solvable loops.
Run Amber with Docker
The repository comes with a Dockerfile. This is the easiest way to run Amber.
Make sure Docker is installed on your local machine (docs.docker.com/get-docker/).
Execute the following command, to run a docker container containing Amber and connect to the container:
docker run -ti marcelmoosbrugger/amber
Now you can run Amber on a given benchmark file with the following command:
If you want to use your own benchmarks within the Docker container please see the Docker documentation on volumes (docs.docker.com/storage/volumes/).
Amber needs the following dependencies:
- Python version ≥ 3.8 and pip
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 firstname.lastname@example.org:probing-lab/amber.git cd amber
- Create a virtual environment in the
pip3 install --user virtualenv python3 -m venv .venv
- Activate the virtual environment:
- Install the required dependencies with pip:
pip install -r requirements.txt
If the previous command failed, try the following instead:
python -m pip install -r requirements.txt
Having all dependencies installed, you can run Amber for example like this:
python ./amber.py --benchmarks benchmarks/past/2d_bounded_random_walk
A more extensive help can be obtained by:
python ./amber.py --help
Run Automatic Tests
You can run all automatic tests with:
python -m unittest
Writing your own Prob-solvable loop
A Prob-solvable loop consist of initial assignments (one per line), a loop head
while P > Q:
and a loop body consisting of multiple variable updates (also one per line).
The loop guard
P > Q consists of two polynomials
Q over the program variables.
- format: `var = value
- comment: not all variables have to have initial value specified
x = 123
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 + 1followed by
y = y + x^2is allowed. However,
x = x + yfollowed by
y = y + 1, or
x = x^2is not allowed.
x = x @ 1/2; x + u
An example program would be:
# this is a comment y = 0.01 x = 5 while x > 0: y = 2*y x = x + 200*y**2 @ 1/2; x - y**3
More examples can be found in the