From 6316b69f31b74b839c01c008a8d90e6f853d0bce Mon Sep 17 00:00:00 2001 From: Faried Abu Zaid Date: Fri, 9 Feb 2024 14:23:02 +0100 Subject: [PATCH] Update installation instructions --- README.md | 32 +++++++++++++------------------- 1 file changed, 13 insertions(+), 19 deletions(-) diff --git a/README.md b/README.md index 5b08bc3..0b542a9 100644 --- a/README.md +++ b/README.md @@ -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