Merge pull request #7 from aai-institute/add-content

Add workshop content

.github/workflows/test_and_render.yaml

@@ -32,16 +32,16 @@ jobs:
         run: pip install -e .
       - name: Run tests
         run: pytest
-      - name: Build docs
+#      - name: Build docs
 #       NOTE: feel free to delete the if-else and just keep the else line. It's simply a special case to make the
 #       automatically generated thesan_output fully representative. In normal cases, the notebooks are rendered
 #       locally and html is committed
-        run: |
-          if [ $(basename "$PWD") = "thesan_output" ]; then 
-            bash build_scripts/build_docs.sh --execute
-          else
-            bash build_scripts/build_docs.sh --skip-nbconvert --skip-jupyter-book
-          fi
+#        run: |
+#          if [ $(basename "$PWD") = "thesan_output" ]; then 
+#            bash build_scripts/build_docs.sh --execute
+#          else
+#            bash build_scripts/build_docs.sh --skip-nbconvert --skip-jupyter-book
+#          fi
       - name: Prepare Pages
         if: github.ref == 'refs/heads/master'
         run: mv docs/_build/html/* public/

AGENDA.md

@@ -1,27 +1,15 @@
 # Agenda
 
-Welcome to the TfL training tfl-training-probabilistic-model-checking!. 
+Welcome to the TfL training Verifying Systems in the Face of Uncertainty! 
 
-Here the Agenda for the next days: 
-
-TODO: replace by real agenda
+Here the Agenda for the today: 
 
 | Day No. | Title                                             | Duration |   Schedule    |
 |:-------:|---------------------------------------------------|:--------:|:-------------:|
-|    1    | Greeting and setting up the execution environment |  10 min  | 09:00 - 09:10 |
-|    1    | Introduction to the awesome topic                 |  30 min  | 09:10 - 10:30 |
-|    1    | Coffee Break                                      |  15 min  | 10:30 - 10:45 |
-|    1    | Second part                                       |  90 min  | 10:45 - 12:15 |
-|    1    | Lunch Break                                       |  60 min  | 12:15 - 13:15 |
-|    1    | Third part                                        |  60 min  | 13:15 - 15:00 |
-|    1    | Coffee Break                                      |  15 min  | 15:00 - 15:15 |
-|    1    | Hold it...                                        |  45 min  | 15:15 - 17:00 |
-|    2    | A new day's topic                                 |  60 min  | 09:00 - 10:30 |
-|    2    | Coffee Break                                      |  15 min  | 10:30 - 10:45 |
-|    2    | Continued                                         |  90 min  | 10:45 - 12:15 |
-|    2    | Lunch Break                                       |  60 min  | 12:15 - 13:15 |
-|    2    | Third part                                        |  60 min  | 13:15 - 15:00 |
-|    2    | Coffee Break                                      |  15 min  | 15:00 - 15:15 |
-|    2    | Last part                                         |  45 min  | 15:15 - 16:45 |
-|    2    | Concluding Remarks                                |  15 min  | 16:45 - 17:00 |
-
+|    1    | Greeting and setting up the execution environment |  15 min  | 09:00 - 09:15 |
+|    1    | what is probabilistic model checking?             |  60 min  | 09:15 - 10:15 |
+|    1    | Demo                                              |  30 min  | 10:15 - 10:45 |
+|    1    | Coffee break                                      |  15 min  | 10:45 - 11:00 |
+|    1    | Fault trees                                       |  45 min  | 11:00 - 11:45 |
+|    1    | Parameter synthesis                               |  30 min  | 11:45 - 12:15 |
+|    1    | Hands-on exercise                                 |  30 min  | 12:15 - 12:45 |

CONTRIBUTING.md

@@ -1,7 +1,8 @@
 # tfl-training-probabilistic-model-checking - developing the training
 
 This repository was created from an aAI internal
-[template](https://github.com/appliedAI-Initiative/thesan)
+[template](https://github.com/appliedAI-Initiative/thesan) and is based on content from
+the [storm developers](https://www.stormchecker.org/)
 
 
 ## Overview of the features

Dockerfile

@@ -1,4 +1,4 @@
-FROM jupyter/minimal-notebook:python-3.9.7
+FROM jupyter/minimal-notebook:python-3.11
 
 # keep env var name in sync with config_local.yml
 ARG PARTICIPANT_BUCKET_READ_SECRET
@@ -14,27 +14,19 @@ you might find the corresponding value inside config.yml under the 'secret' key.
     fi
 
 USER root
-RUN apt-get update && apt-get upgrade -y
 
 # pandoc needed for docs, see https://nbsphinx.readthedocs.io/en/0.7.1/installation.html?highlight=pandoc#pandoc
 # gh-pages action uses rsync
-RUN apt-get -y install pandoc git-lfs rsync
+RUN apt-get update -qq  && apt-get upgrade -y && apt-get -y install pandoc git-lfs rsync
 
 USER ${NB_UID}
 
-WORKDIR /tmp
 COPY build_scripts build_scripts
 RUN bash build_scripts/install_presentation_requirements.sh
 
 COPY requirements-test.txt .
 RUN pip install -r requirements-test.txt
 
-
-# NOTE: this breaks down when requirements contain pytorch (file system too large to fit in RAM, even with 16GB)
-# NOTE: this might break down when requirements contain pytorch (file system too large to fit in RAM, even with 16GB)
-# If pytorch is a requirement, the suggested solution is to keep a requirements-docker.txt and only install
-# the lighter requirements. The install of the remaining requirements then has to happen at runtime
-# instead of build time (usually as part of the entrypoint)
 COPY requirements.txt .
 RUN pip install -r requirements.txt
 
@@ -58,3 +50,142 @@ ENTRYPOINT ["/tmp/code/entrypoint.sh"]
 WORKDIR "${HOME}"
 
 COPY --chown=${NB_UID}:${NB_GID} . $CODE_DIR
+
+# Storm related setup
+USER root
+
+ENV DEBIAN_FRONTEND=noninteractive
+
+# Install dependencies
+# - ca-certificates is needed for cloning from Github
+# - all other dependencies are the recommended packages for Storm (see https://www.stormchecker.org/documentation/obtain-storm/dependencies.html#-debian-and--ubuntu)
+RUN apt-get install --fix-missing -y --no-install-recommends \
+    ca-certificates \
+    build-essential \
+    git \
+    cmake \
+    libboost-all-dev \
+    libcln-dev \
+    libgmp-dev \
+    libginac-dev \
+    automake \
+    libglpk-dev \
+    libhwloc-dev \
+    libz3-dev \
+    libxerces-c-dev \
+    libeigen3-dev
+
+
+# Specify number of threads to use for parallel compilation
+# This number can be set from the commandline with:
+# --build-arg no_threads=<value>
+ARG no_threads=1
+
+
+# Build Carl
+############
+# Explicitly build the Carl library
+# This is needed when using pycarl/stormpy later on
+WORKDIR /opt/
+
+# Obtain Carl from public repository
+RUN git clone https://github.com/moves-rwth/carl-storm.git carl
+
+# Switch to build directory
+RUN mkdir -p /opt/carl/build
+WORKDIR /opt/carl/build
+
+# Configure Carl
+RUN cmake .. -DCMAKE_BUILD_TYPE=Release -DUSE_CLN_NUMBERS=ON -DUSE_GINAC=ON -DTHREAD_SAFE=ON
+
+# Build Carl library
+RUN make lib_carl -j $no_threads
+
+# Build Storm
+#############
+WORKDIR /opt/
+
+# Obtain storm from public repository
+RUN git clone https://github.com/moves-rwth/storm.git storm --branch 1.8.1
+WORKDIR /opt/storm
+
+# Switch to build directory
+RUN mkdir -p /opt/storm/build
+WORKDIR /opt/storm/build
+
+# Configure Storm
+RUN cmake .. -DCMAKE_BUILD_TYPE=Release -DSTORM_DEVELOPER=OFF -DSTORM_LOG_DISABLE_DEBUG=ON -DSTORM_PORTABLE=ON -DSTORM_USE_SPOT_SHIPPED=ON
+
+# Build external dependencies of Storm
+RUN make resources -j $no_threads
+
+# Build Storm binary
+RUN make storm -j $no_threads
+
+# Build additional binaries of Storm
+# (This can be skipped or adapted dependending on custom needs)
+RUN make binaries -j $no_threads
+
+# Set path
+ENV PATH="/opt/storm/build/bin:$PATH"
+
+# Install dependencies
+######################
+# Uncomment to update packages beforehand
+# RUN apt-get update -qq
+
+
+RUN apt-get install -y --no-install-recommends \
+    maven \
+    uuid-dev \
+    python3 \
+    python3-pip
+# Packages maven and uuid-dev are required for carl-parser
+ENV CMAKE_PREFIX_PATH="/opt/carl/build:$CMAKE_PREFIX_PATH"
+
+# Build carl-parser
+###################
+WORKDIR /opt/
+
+# Obtain carl-parser from public repository
+RUN git clone -b master14 https://github.com/ths-rwth/carl-parser.git
+
+# Switch to build directory
+RUN mkdir -p /opt/carl-parser/build
+WORKDIR /opt/carl-parser/build
+
+# Configure carl-parser
+RUN cmake .. -DCMAKE_BUILD_TYPE=Release
+
+# Build carl-parser
+RUN make carl-parser -j $no_threads
+
+# Build pycarl
+##############
+WORKDIR /opt/
+
+# Obtain latest version of pycarl from public repository
+RUN git clone https://github.com/moves-rwth/pycarl.git
+
+# Switch to pycarl directory
+WORKDIR /opt/pycarl
+
+# Build pycarl
+RUN python3 setup.py build_ext -j $no_threads develop
+
+# Build stormpy
+###############
+WORKDIR /opt/
+
+# Obtain stormpy from public repository
+RUN git clone https://github.com/moves-rwth/stormpy.git --branch 1.8.0
+WORKDIR /opt/stormpy
+
+# Build stormpy,
+RUN python3 setup.py build_ext -j $no_threads develop
+
+USER ${NB_UID}
+WORKDIR "${HOME}"
+
+EXPOSE 8888
+CMD [ "jupyter", "notebook" ]