Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update installation instructions #14

Merged
merged 1 commit into from
Feb 9, 2024
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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
Loading