Skip to content

Commit

Permalink
Merge pull request #14 from aai-institute/fariedabuzaid-patch-1
Browse files Browse the repository at this point in the history
Update installation instructions
  • Loading branch information
fariedabuzaid authored Feb 9, 2024
2 parents 0d2f76f + 6316b69 commit 1f0963b
Showing 1 changed file with 13 additions and 19 deletions.
32 changes: 13 additions & 19 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,33 +4,27 @@ Welcome to the TransferLab training: Probabilistic Model Checking with Storm.
The content was created by two major researchers in the field, Prof. [Joost-Pieter Katoen](https://moves.rwth-aachen.de/people/katoen/) and Assoc. Prof. [Sebastian Junges](https://sjunges.github.io). The course contains a mix of lectures and hands-on exercises covering
the fundamentals of probabilistic model checking as well as practical applications using the model checker Storm.

## Getting started

## During the training
If you want to execute the notebooks, we recommend to use docker. You can
eigther download a pre-build image from ghcr or build the image locally.

If you are currently participating in the training, you can find the agenda in
the file `AGENDA.md`. Everything is already set up, so feel free to follow the
trainer's presentation or to explore the notebooks and source code on your own.
1. Option a) Pull the pre-build image from [ghcr.io](ghcr.io/aai-institute/tfl-training-probabilistic-model-checking:main)
```shell
docker pull ghcr.io/aai-institute/tfl-training-probabilistic-model-checking:main
```
Option b) Build the image with

## After the training

You have received this file as part of the training materials.

There are multiple ways of viewing/executing the content.

1. If you just want to view the rendered notebooks, open `html/index.html` in
your browser.
2. If you want to execute the notebooks, we recommend to use docker. You can
build the image locally. First, set the variable
`PARTICIPANT_BUCKET_READ_SECRET` to the secret found in `config.yml`, and then
build the image with
```shell
docker build --build-arg PARTICIPANT_BUCKET_READ_SECRET=$PARTICIPANT_BUCKET_READ_SECRET -t tfl-training-probabilistic-model-checking .
docker build --build-arg -t tfl-training-probabilistic-model-checking .
```
You can then start the container e.g., with

2. You can then start the container e.g., with
```shell
docker run -it -p 8888:8888 tfl-training-probabilistic-model-checking jupyter notebook
```
4. The data will be downloaded on the fly when you run the notebooks.
3. Run the first notebook **welcome_run_me_first.ipynb** within jupyter. This will dowload the data for
the workshop and finilize the setup.

Note that there is some non-trivial logic in the entrypoint that may collide
with mounting volumes to paths directly inside
Expand Down

0 comments on commit 1f0963b

Please sign in to comment.