added slides pdf

docker_build.sh

@@ -1 +1 @@
-sudo docker build -t gsw_ai_lab .
+sudo docker build -t tempest_in_action .

docker_run_jupyter.sh

@@ -1,4 +1,4 @@
-DOCKER_IMAGE=gsw_ai_lab
+DOCKER_IMAGE=tempest_in_action
 IMAGE_VERSION=latest
 CONTAINER_NAME=tempestpy_jupyter
 

dockerfile

@@ -1,14 +1,5 @@
 FROM movesrwth/storm-basesystem:ubuntu-22.04 as build
 
-#COPY ./tempest-devel /opt/tempest
-#COPY ./tempest-py /opt/tempestpy
-#COPY ./pycarl-2.0.4 /opt/pycarl
-#COPY ./carl /opt/carl
-
-# RUN rm -r /opt/tempest/.git
-# RUN rm -r /opt/tempestpy/.git
-# RUN rm -r /opt/Minigrid2PRISM/.git
-
 RUN apt-get update
 RUN apt-get install -y python3.10
 
@@ -31,22 +22,9 @@ WORKDIR /opt/tempest/build
 RUN cmake .. -DCMAKE_BUILD_TYPE=Release -DSTORM_DEVELOPER=OFF -DSTORM_LOG_DISABLE_DEBUG=ON -DSTORM_PORTABLE=OFF -DSTORM_USE_SPOT_SHIPPED=ON
 RUN make resources storm binaries -j $no_threads
 
-
-RUN apt-get install -y maven
-RUN apt-get install -y uuid-dev
-
-# COPY ./carl-parser /opt/carl-parser
-
-# # Switch to build directory
-# RUN mkdir -p /opt/carl-parser/build
-# WORKDIR /opt/carl-parser/build
-
 # Configure carl-parser
 RUN cmake .. -DCMAKE_BUILD_TYPE=$build_type
 
-# Build carl-parser
-# RUN make carl-parser -j $no_threads
-
 # Manage python packages
 WORKDIR /opt/
 RUN apt-get install -y python3-venv
@@ -87,13 +65,6 @@ WORKDIR /opt/Minigrid2PRISM/build
 RUN cmake ..
 RUN make -j $no_threads
 
-# build minigrid
-#COPY ./Minigrid /opt/Minigrid
-#RUN rm -r /opt/Minigrid/.git
-#WORKDIR /opt/Minigrid
-#RUN pip install .
-
-
 
 RUN apt-get update && apt-get install ffmpeg libsm6 libxext6 -y
 

notebooks/GSW_Playground.ipynb → notebooks/Playground.ipynb

@@ -281,8 +281,8 @@
     "    return [1.0] * 7\n",
     "\n",
     "def main():\n",
-    "    # Edit 'environments/Minigrid/minigrid/envs/GSW_Playground.py' to alter the environment\n",
-    "    env = \"MiniGrid-GSW-v0\"\n",
+    "    # Edit 'environments/Minigrid/minigrid/envs/Playground.py' to alter the environment\n",
+    "    env = \"MiniGrid-Playground-v0\"\n",
     "\n",
     "    # TODO Change the safety specification\n",
     "    formula = \"Pmax=? [G !AgentIsOnLava]\"\n",

notebooks/environments/Minigrid/minigrid/__init__.py

@@ -22,11 +22,11 @@ except Exception:  # nosec
 
 def register_minigrid_envs():
 
-    # GSW Playground
+    # Playground
     # ----------------------------------------
 
     register(
-        id="MiniGrid-GSW-v0",
+        id="MiniGrid-Playground-v0",
         entry_point="minigrid.envs:Playground",
         kwargs={},
     )
@@ -812,10 +812,10 @@ def register_minigrid_envs():
     # Playground
     # ----------------------------------------
 
-    register(
-        id="MiniGrid-Playground-v0",
-        entry_point="minigrid.envs:PlaygroundEnv",
-    )
+    #register(
+    #    id="MiniGrid-Playground-v0",
+    #    entry_point="minigrid.envs:PlaygroundEnv",
+    #)
 
     # PutNear
     # ----------------------------------------

notebooks/environments/Minigrid/minigrid/envs/__init__.py

@@ -15,7 +15,7 @@ from minigrid.envs.lavagap import LavaGapEnv
 from minigrid.envs.lavafaulty import LavaFaultyEnv
 from minigrid.envs.windycity import WindyCityEnv, WindyCityAdvEnv, WindyCity2Env, WindyCitySmallAdv
 from minigrid.envs.lavaslippery import LavaSlipperyEnv1, LavaSlipperyCliff, LavaSlipperyHill, LavaSlipperyMaze
-from minigrid.envs.GSW_Playground import Playground
+from minigrid.envs.Playground import Playground
 from minigrid.envs.adversary_debug import AdversaryDebug
 from minigrid.envs.adversary_simple import AdversarySimple
 from minigrid.envs.adversarydoorpickup import AdversaryDoorPickup
@@ -30,7 +30,7 @@ from minigrid.envs.obstructedmaze import (
     ObstructedMaze_Full,
     ObstructedMazeEnv,
 )
-from minigrid.envs.playground import PlaygroundEnv
+#from minigrid.envs.playground import PlaygroundEnv
 from minigrid.envs.putnear import PutNearEnv
 from minigrid.envs.redbluedoors import RedBlueDoorEnv
 from minigrid.envs.unlock import UnlockEnv