|
|
{ "cells": [ { "cell_type": "markdown", "metadata": {}, "source": [ "## Example usage of Tempestpy" ] }, { "cell_type": "code", "execution_count": 1, "metadata": { "vscode": { "languageId": "plaintext" } }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "pygame 2.6.0 (SDL 2.28.4, Python 3.10.12)\n", "Hello from the pygame community. https://www.pygame.org/contribute.html\n" ] }, { "name": "stderr", "output_type": "stream", "text": [ "2024-09-24 13:31:25.321557: E external/local_xla/xla/stream_executor/cuda/cuda_fft.cc:485] Unable to register cuFFT factory: Attempting to register factory for plugin cuFFT when one has already been registered\n", "2024-09-24 13:31:25.336097: E external/local_xla/xla/stream_executor/cuda/cuda_dnn.cc:8454] Unable to register cuDNN factory: Attempting to register factory for plugin cuDNN when one has already been registered\n", "2024-09-24 13:31:25.340241: E external/local_xla/xla/stream_executor/cuda/cuda_blas.cc:1452] Unable to register cuBLAS factory: Attempting to register factory for plugin cuBLAS when one has already been registered\n", "2024-09-24 13:31:25.350298: I tensorflow/core/platform/cpu_feature_guard.cc:210] This TensorFlow binary is optimized to use available CPU instructions in performance-critical operations.\n", "To enable the following instructions: AVX2 FMA, in other operations, rebuild TensorFlow with the appropriate compiler flags.\n", "2024-09-24 13:31:26.198496: W tensorflow/compiler/tf2tensorrt/utils/py_utils.cc:38] TF-TRT Warning: Could not find TensorRT\n", "error: XDG_RUNTIME_DIR not set in the environment.\n" ] } ], "source": [ "from sb3_contrib import MaskablePPO\n", "from sb3_contrib.common.wrappers import ActionMasker\n", "from stable_baselines3.common.logger import Logger, CSVOutputFormat, TensorBoardOutputFormat, HumanOutputFormat\n", "\n", "import gymnasium as gym\n", "\n", "from minigrid.core.actions import Actions\n", "from minigrid.core.constants import TILE_PIXELS\n", "from minigrid.wrappers import RGBImgObsWrapper, ImgObsWrapper\n", "\n", "import tempfile, datetime, shutil\n", "\n", "import time\n", "import os\n", "\n", "from utils import MiniGridShieldHandler, create_log_dir, ShieldingConfig, MiniWrapper, expname, shield_needed, shielded_evaluation, create_shield_overlay_image\n", "from sb3utils import MiniGridSbShieldingWrapper, parse_sb3_arguments, ImageRecorderCallback, InfoCallback\n", "\n", "import os, sys\n", "from copy import deepcopy\n", "\n", "from PIL import Image" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "vscode": { "languageId": "plaintext" } }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "Starting the training\n" ] }, { "data": { "image/jpeg": "/9j/4AAQSkZJRgABAQAAAQABAAD/2wBDAAgGBgcGBQgHBwcJCQgKDBQNDAsLDBkSEw8UHRofHh0aHBwgJC4nICIsIxwcKDcpLDAxNDQ0Hyc5PTgyPC4zNDL/2wBDAQkJCQwLDBgNDRgyIRwhMjIyMjIyMjIyMjIyMjIyMjIyMjIyMjIyMjIyMjIyMjIyMjIyMjIyMjIyMjIyMjIyMjL/wAARCAGAAYADASIAAhEBAxEB/8QAHwAAAQUBAQEBAQEAAAAAAAAAAAECAwQFBgcICQoL/8QAtRAAAgEDAwIEAwUFBAQAAAF9AQIDAAQRBRIhMUEGE1FhByJxFDKBkaEII0KxwRVS0fAkM2JyggkKFhcYGRolJicoKSo0NTY3ODk6Q0RFRkdISUpTVFVWV1hZWmNkZWZnaGlqc3R1dnd4eXqDhIWGh4iJipKTlJWWl5iZmqKjpKWmp6ipqrKztLW2t7i5usLDxMXGx8jJytLT1NXW19jZ2uHi4+Tl5ufo6erx8vP09fb3+Pn6/8QAHwEAAwEBAQEBAQEBAQAAAAAAAAECAwQFBgcICQoL/8QAtREAAgECBAQDBAcFBAQAAQJ3AAECAxEEBSExBhJBUQdhcRMiMoEIFEKRobHBCSMzUvAVYnLRChYkNOEl8RcYGRomJygpKjU2Nzg5OkNERUZHSElKU1RVVldYWVpjZGVmZ2hpanN0dXZ3eHl6goOEhYaHiImKkpOUlZaXmJmaoqOkpaanqKmqsrO0tba3uLm6wsPExcbHyMnK0tPU1dbX2Nna4uPk5ebn6Onq8vP09fb3+Pn6/9oADAMBAAIRAxEAPwDDooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKACiiigAooooAKKKKAPMtU1TUI9XvUS/ulRZ3CqszAAbjwOaqf2vqf8A0Ebv/v8At/jRq/8AyGr/AP6+JP8A0I1ToAuf2vqf/QRu/wDv+3+NH9r6n/0Ebv8A7/t/jVOigDWmaQHh1jTu561DGxz+4nLHuknf6VJKoM2ViLvjq33RTHDMMyIky/3o+q1+lYqVR15STejevvafNWS87Rmv5mccbWEkY5/fzlT2SPt9amhaQnl1kTs461EgZRmNEhX+9J1anxKBNloij46r900YWVT28ZNvVrX3tfm7p+V4wX8rCVrDpmkB4dY07uetQxsc/uJyx7pJ3+lSSqDNlYi746t90UxwzDMiJMv96PqtGKlUdeUk3o3r72nzVkvO0Zr+ZhG1hJGOf385U9kj7fWpoWkJ5dZE7OOtRIGUZjRIV/vSdWp8SgTZaIo+Oq/dNGFlU9vGTb1a197X5u6fleMF/Kwlaw6ZpAeHWNO7nrUMbHP7icse6Sd/pUkqgzZWIu+OrfdFMcMwzIiTL/ej6rRipVHXlJN6N6+9p81ZLztGa/mYRtYSRjn9/OVPZI+31qaFpCeXWROzjrUSBlGY0SFf70nVqfEoE2WiKPjqv3TRhZVPbxk29Wtfe1+bun5XjBfysJWsP1TVNQj1e9RL+6VFncKqzMABuPA5qp/a+p/9BG7/AO/7f40av/yGr/8A6+JP/QjVOvzU7C5/a+p/9BG7/wC/7f40f2vqf/QRu/8Av+3+NU6KANfVNU1CPV71Ev7pUWdwqrMwAG48Dmqn9r6n/wBBG7/7/t/jRq//ACGr/wD6+JP/AEI1ToAuf2vqf/QRu/8Av+3+NH9r6n/0Ebv/AL/t/jVOigDX1TVNQj1e9RL+6VFncKqzMABuPA5qp/a+p/8AQRu/+/7f40av/wAhq/8A+viT/wBCNU6ALn9r6n/0Ebv/AL/t/jR/a+p/9BG7/wC/7f41TooA19U1TUI9XvUS/ulRZ3CqszAAbjwOaqf2vqf/AEEbv/v+3+NGr/8AIav/APr4k/8AQjVOgC5/a+p/9BG7/wC/7f40f2vqf/QRu/8Av+3+NU6KANfVNU1CPV71Ev7pUWdwqrMwAG48Dmqn9r6n/wBBG7/7/t/jRq//ACGr/wD6+JP/AEI1ToAuf2vqf/QRu/8Av+3+NH9r6n/0Ebv/AL/t/jVOigD6Wooor80PyAKKKKAONooor9LP18KKKKACiiigAooooA8n1f8A5DV//wBfEn/oRqnVzV/+Q1f/APXxJ/6Eap0AFFFFAGncFd+15GYdok6mo8KpBKtbt2Ycg/WrEiStIdm1ARy+Mk00wyoP3cm8HqsnOa/TMThak606ig2r72/K759P7ril0TONSVrXIcKxJCtcN3Y8AfSpLcrv2pIyjvE/UU4QyuP3kmwDosfGKdGkqyDftcAcPjBFGGwtSFWFRwaV97fnZ8+v95yT6pBKSta5HcFd+15GYdok6mo8KpBKtbt2Ycg/WrEiStIdm1ARy+Mk00wyoP3cm8HqsnOaMThak606ig2r72/K759P7ril0TBSVrXIcKxJCtcN3Y8AfSpLcrv2pIyjvE/UU4QyuP3kmwDosfGKdGkqyDftcAcPjBFGGwtSFWFRwaV97fnZ8+v95yT6pBKSta5HcFd+15GYdok6mo8KpBKtbt2Ycg/WrEiStIdm1ARy+Mk00wyoP3cm8HqsnOaMThak606ig2r72/K759P7ril0TBSVrXIcKxJCtcN3Y8AfSpLcrv2pIyjvE/UU4QyuP3kmwDosfGKdGkqyDftcAcPjBFGGwtSFWFRwaV97fnZ8+v8Aeck+qQSkrWuVNX/5DV//ANfEn/oRqnVzV/8AkNX/AP18Sf8AoRqnX5mdgUUUUAXNX/5DV/8A9fEn/oRqnVzV/wDkNX//AF8Sf+hGqdABRRRQBc1f/kNX/wD18Sf+hGqdXNX/AOQ1f/8AXxJ/6Eap0AFFFFAFzV/+Q1f/APXxJ/6Eap1c1f8A5DV//wBfEn/oRqnQAUUUUAXNX/5DV/8A9fEn/oRqnVzV/wDkNX//AF8Sf+hGqdABRRRQB9LUUUV+aH5AFFFFAHG0UUV+ln6+FFFFABRRRQAUUUUAeZapqmoR6veol/dKizuFVZmAA3Hgc1U/tfU/+gjd/wDf9v8AGjV/+Q1f/wDXxJ/6Eap0AXP7X1P/AKCN3/3/AG/xo/tfU/8AoI3f/f8Ab/GqdFAGvqmqahHq96iX90qLO4VVmYADceBzVT+19T/6CN3/AN/2/wAaNX/5DV//ANfEn/oRqnQBc/tfU/8AoI3f/f8Ab/Gj+19T/wCgjd/9/wBv8ap0UAa+qapqEer3qJf3Sos7hVWZgANx4HNVP7X1P/oI3f8A3/b/ABo1f/kNX/8A18Sf+hGqdAFz+19T/wCgjd/9/wBv8aP7X1P/AKCN3/3/AG/xqnRQBr6pqmoR6veol/dKizuFVZmAA3Hgc1U/tfU/+gjd/wDf9v8AGjV/+Q1f/wDXxJ/6Eap0AXP7X1P/AKCN3/3/AG/xo/tfU/8AoI3f/f8Ab/GqdFAGu8jrPsyAHX5D6GoxcN5aO3ADbZB6H1p0xDzJH0CfOx9KhOWRiB81w2APQDvX6ZisTWhUmqc3ZN2/B28/ftHzUmuhxxSsrkrSyASqMF0O4cdVpyzEzKM/JIuVPvURcK7yD7sS7B/tGkWM5hg7r87H09qmOKrqolGTeumu/vWX3pyV+0FIOVWJ9U1TUI9XvUS/ulRZ3CqszAAbjwOaqf2vqf8A0Ebv/v8At/jRq/8AyGr/AP6+JP8A0I1Tr81Owuf2vqf/AEEbv/v+3+NH9r6n/wBBG7/7/t/jVOigDX1TVNQj1e9RL+6VFncKqzMABuPA5qp/a+p/9BG7/wC/7f40av8A8hq//wCviT/0I1ToAuf2vqf/AEEbv/v+3+NH9r6n/wBBG7/7/t/jVOigDX1TVNQj1e9RL+6VFncKqzMABuPA5qp/a+ "image/png": "iVBORw0KGgoAAAANSUhEUgAAAYAAAAGACAIAAAArpSLoAAAda0lEQVR4Ae2d/ZXbxhVHsT76O2lAUgFJA1o34DQgNRCoAK0aUAOWChDTgNWAlQKsbSApwNoG4gacH/nE0SxIgsR7+JgB75w9K3zMe5i5Q10PBqB107ZtQ4EABCCwBIEflrgo14QABCCwJYCA+BxAAAKLEUBAi6HnwhCAAALiMwABCCxGAAEthp4LQwACCIjPAAQgsBgBBLQYei4MAQggID4DEIDAYgQQ0GLouTAEIICA+AxAAAKLEUBAi6HnwhCAAALiMwABCCxGAAEthp4LQwACCIjPAAQgsBgBBLQYei4MAQggID4DEIDAYgQQ0GLouTAEIICA+AxAAAKLEUBAi6HnwhCAAALiMwABCCxGAAEthp4LQwACCIjPAAQgsBgBBLQYei4MAQggID4DEIDAYgQQ0GLouTAEIICA+AxAAAKLEUBAi6HnwhCAAALiMwABCCxGAAEthp4LQwACCIjPAAQgsBgBBLQYei4MAQg8qR3BZvPxdBc+Nc2Lpnl2uoLOfG2a+6Z52Vvn1MkK8rft61Ot5/gKCGw+bibtRfu6nTT/HALabCZldFRA75vmQ9M87Ni9aRr9HGpI6lEd/ag83dW5221f8qum/JPyb9uW/D2fmKn5NEc//j0NKuzU+m7BpAa55u3OPpr+qEgxz5tGcpFxrGhDuzpo9lE1qUohClR4f6k9f3/vOAuBWQmsSUAdNfzWNF+a5vfd1EZMk4Zy9WhmpAqqpspnNVR7/lk/WFwMApcQWI2AXmWzHlPP7a7/NqnJNWSzHlOPOUUVVbmjISXMS+35876wDYFSCKxGQFpF1k+uHrvPklZUcg111KMKd/u7s6Qhy5YPUu35876wDYFSCMyxCD1LX3NlSD2a5thMR791b6WZjuTSWeIx9dzvmqdqEpN+VEc19dMptefvdIddCBRBYDUzIKPZWV2WNfR4S4r5cX+TZdWkHilGB3VKFVRNRQ56ns2GrGbnd+35O91hFwILE1iNgDpqsPusX3b3Vj8/1lCuHp1SoKr9frBWreN5qT1/3he2IVAKgdUI6O3+nquzxCPQd481ZLMeU49OWdGdl27Tcg0pYV5qz5/3hW0IlEJgNQKyFRwZJD3Y0n2WHl1p14pco1mMvNNRjyqomiqr5BpSwrzUnj/vC9sQKIXAahah85XjfHVZ35awBWYJSMV+G32pR6fsbWn7UoWOKI9pyOqk37XnTx1hAwIFEfihoLaM0JR8dfnFbnFHvw/fcpZoZBndVelUqqZbs85a9WGDas9/2COOQGBJAqsRUEcN9kKQHm/puLZzDeXqOax2SkO151/yQ8a1IXCKwGoEpJspuUOiMafojikVbecasllPfzWlUsK81J4/7wvbECiFwGoE9PNj9Wi9+a5pbvaPwIQ7aShXT081JcxL7fnzvrANgVIIrEZAurGyWY855fl+CqOZi7YlIx1XUZ0LqylhXmrPn/eFbQiUQmA1AhLQjnr04FyTHXuanmvowmqHI3Rh4IXV5s9/eEWOQGBhAqsRkJ6jp1mPpPP7/vtfeuCl7VxDF1ZTwrzUnj/vC9sQKIXAmgQkpkk9+Q2UtnMNXVjtUEAXBl5Ybeb8ahUFAsURWI2A9H2uPx+/Bq21npv92rO4m4ZU58JqSpiX2vPnfWEbAqUQWI2AEtD8hR0dvOS9np5qKW3aqD1/6ggbEFiewJoElKtB/5ONn3eTHa1D6+WgXEN5NZ1SBc2JVPno/7gjH6E8sMb8eV/YhkARBFYjoLvs/+8jm9ijKCHWjZjEkWtI37eQj0w95hRVU7hCcg3pSF5qz5/3hW0IlELgh1IaMkI7bFaS1KOMWujVrkquoY56VCGtB+ca2sU9+lV7/kedYQcCJRBYjYD0nCtXj3af7f4/G3robloRbdNQmvVYfVV4tV+ithGx+sqQF+1WnT/vC9sQKIXAagSUgMoUUs/b/TfddfzD45ehdSSpR6dUNCc6/Mb87syRX7XnP9IlDkFgKQJrElBHDVr30WTn98dvIWp2o5/n+y9q2HtDaZGoX0O151/qM8Z1IXCSwGoEpNuoNOsx9eiGS0WzIYkj15DNejqvLOaLRKYhJcxL7fnzvrANgVIIPCmlIdF22L9sIa2YdzrpTEM6m+yjI4clLRKpmiVMdWrPnzrCBgQKIrAmAXWUcUjZNHR4vHNEGjq0mJJXnb/TR3YhUASB1dyCFUGTRkAAAoMI3LRtOyiAynUR2Gw+Ttrgtn09aX6Sr5vAHLdgm81mOogSKPl78U4rIF0a/j38V/D57Old/BS3YHGGVWTQ2975c7273esIqeU6lV4H10tS2tWrCVa0oV0dtNLJsz/MnxBwEUBALmz1BUkc+tEbCVa0rSd9yTKmFbPMw66mDJVqWuV8N+XZ1+JPCLgIICAXtvqC9AqCir2FoA3bTZbJz+oJoF4Nv9/rKZ0yPaXdXT5+QSBGAAHF+FUTbVrR7MYmL1KPvlt7yjKpjrqndxdy6XTyVNN/GlomAQRU5rhM0SrTytFJ0FHL9Osp5ZmiqeS8FgII6FpGevd2pe6tmARdz4hX0FMEVMEgjddEJkHjsSTTGAQQ0BgUq8mRVnD0YEvlbvdbt1pW7Lsm6d7Kztqu7tHys508+wT8CYGBBBDQQGB1V9eTLNON7sVU7DG8bWvXrGRLztq16VI6a5VNQ50821wUCDgIICAHtHpDbDojxWhGo2JzHBONnJLO6pR0I1XpSVmqo8UjyUhzH5VU0/LsjvELAsMJIKDhzGqNOKqYU04x76TZkBnnqKpqxUG7SyCAgEoYhXna0Jm2pKmNrn7UTUx/5hmXq74KArqS4T+qGKY/VzL65XYTAZU7NqO2rGf6o+uks9pm9WdU8CTrJYCAevFwEgIQmJIAApqSbkG50/e5dC+mYsvJd/sGprM6kN7xSXV6vjW2T8CfEHARQEAubPUFRb7tZXoyW3Xy1AeCFhdFAAEVNRyTNiZNcw4nQR2tMAmadCBI/p0AAvrOYu1bRy2jtw3tFeejerLFaYFhErT2T8dC/UNAC4Ff5rJHLXP03opJ0DIjdG1XRUBXNeKaBOndHxVNfFTsexW2rd3866baNTGls1bZvi/WybPNRYGAgwACckCrNyS942OusedcpiR16uiXUW3SpGWj/GwnT71AaPnCBBDQwgMw7+VtUmNO0ZVtiefoN7xMMXKTTXzSm4qa+6h08uyO8QsCwwkgoOHMao1I0xbTh7zT8wX3VEe9Pfo1jvRNsVpx0O4SCCCgEkZhnjaYU5j+zEObq1xEAAFdhKn+Skx/6h/DNfYAAa1xVI/0KS3i2Ll89UdH8rP9qz95zSOX4RAEBhF4Mqg2laslYI+97C5MnbBdW2C2XR2xBWYt7mg73alpW0tF+a7qpzzV8qDhZRBAQGWMw+StkEf0k4o9+Uq7v6StnYbyXUkqeUq1OnmyODYhMJwAt2DDmREBAQiMROCmbduRUpGmRAKbzcdJm9W2ryfN//HpZtL8rx/4/E8K+EzyOW7BNpsJP0MSKPl7B3laAenSk/L/+K63c2OcnLT9K/h8jsH4ZA5uwU6iWdcJfZHiVdYjrSLnC8k6Zd+0UBW9dqhdPQuzog3t2v/BQ0c6efa1+BMCLgIIyIWtviCJQz9p7VnbeqCeLGNaMcs87GomPVmgPX1Xt2035akPBC0uigACKmo4pmuMPUdPHrHdZJn8rJ556Stg+hK86SmdMj2l3emaSuYrIoCArmSwTSua3djkRerR+z6nLJPqCI5eDsql08lzJfTo5lQEENBUZMvLa1o5Ogk6apl+PaU85XWUFtVDAAHVM1bRlnYmL0yCokCJjxNAQHGGFWWodRL09X/Nl/Qg7jRv1bmwmhJSSiCAgEoYhdnakCZBepilokmQim61rNh3NdK9lZ21Xd2j5Wc7efYJJvvz7efmx381t5uTfpF3dFZ1LqymhJQSCMzxImIJ/aQNOwKaRZhuXux27TmXbeuAWcmWnLVr06V01iqbhvI8/96lmvbXm9vm6x/N/cPWLy+eNu9/am7tm7N6Vve1ufu "text/plain": [ "<PIL.Image.Image image mode=RGB size=384x384>" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "\n", "\n", "Computing new shield\n", "LOG: Starting with explicit model creation...\n", "Elapsed time is 0.058641910552978516 seconds.\n", "LOG: Starting with model checking...\n", "Elapsed time is 0.0003376007080078125 seconds.\n", "LOG: Starting to translate shield...\n", "Write to file shielding_files_20240924T133128_pk5u63e5/shield.\n", "Elapsed time is 0.013018369674682617 seconds.\n" ] }, { "data": { "image/png": "iVBORw0KGgoAAAANSUhEUgAAAYAAAAGACAYAAACkx7W/AAAug0lEQVR4Ae2dz64ky1Wvq03rIKSDQFh3gyVzLA884gHu5j7Enl0/QfEAHM/6AXoGfgDXE5jZHiEeAPYdMWKEhOVjS8f3ICwjjoQ4MmryV9WrO3bsysp/kRlrZXwhVWdlZMRaEV+s+q2szNzVr47H47sDBQIQgAAEmiPwreZmzIQhAAEIQOBMgARAIEAAAhBolAAJoNGFZ9oQgAAESADEAAQgAIFGCZAAGl14pg0BCECABEAMQAACEGiUAAmg0YVn2hCAAARIAMQABCAAgUYJkAAaXXimDQEIQIAEQAxAAAIQaJQACaDRhWfaEIAABEgAxAAEIACBRgmQABpdeKYNAQhAgARADEAAAhBolAAJoNGFZ9oQgAAESADEAAQgAIFGCZAAGl14pg0BCECABEAMQAACEGiUAAmg0YVn2hCAAARIAMQABCAAgUYJkAAaXXimDQEIQIAEQAxAAAIQaJQACaDRhWfaEIAABEgAxAAEIACBRgmQABpdeKYNAQhAgARADEAAAhBolAAJoNGFZ9oQgAAESADEAAQgAIFGCZAAGl14pg0BCECABEAMQAACEGiUAAmg0YVn2hCAAARe10bw5vGx6hC++ur7h/vD08AY/qY7ft+9/nSgnR3+RfdGNv+vVSzc7tf/v9z98UI2dIfAfAJfff+r+Z0L9Lz72d3h7cNDAUvzTFRPABr2V1/VW4T7w/+/Qe6vu2M/7l6/fN/mL7utXn2JQMKv9nqpfLd7qf3n2plR9u9fwX88nWawKdPldDziv2H+h++XiaOoVpq+BKRz+utFwiuR/1H3kvhbSwn7Z91Lgi6xt6L3qtMxE3/1UV/ZkC3ZHFva8m90x9Ip1c782raU3bF2zK9tx/Yr1c782raU3bF2zK9tx/Yr1a6W31LjL2Gn2QRwffGvCe/fd5z/oXt90b10Nq+SJoJc+NVGbdVHfeVpbCJo1//19ejQrVRyf/n+Sm4/mM395fsfGq70JveX76/k9oPZ3F++/6HhSm+29rfSNBabbTIBXF/8H3Yw0zN+E/4/fw/ZzuLzRGBn/Cb8JuLqpr7XEoF85aV1/x+/Z+VkSu9fX3/893FphX/peUaw11wC6A9y3bDVKxd+u7wjIVfJE8E14Vfbz7uX+qqkicD8XI58/NfqW/V/IdG/Ph9JLXk3ZH/o+BLf6jtkf+g4/pcRWJvvstFt37upBHB78SXAP+1edsZvwv9ZV6ez/P/z/lieCNIzfh1Tf7VNLxOliUA+5Csvrfv/yOP2On1sN/XdWLtj2+F/GoGxXMe2m+Z9OPlOtbeH9s0kgPFBlQu/llnirCd6nrpXngi6qvNlHhN+tVFbE/lriUB9+krr/i9cxq9XH8fn9VPtTW3/3NvLvan2prZ/6fF5zVR7U9s/9/Zyb6q9qe1fenxeU9rec+tx95pIAOMW/5rw2uUdnbXr+F91rzwR5MKvNmqrPl90L9lQGUoErfu/UEr/HbduaY/r7+famdsvH8VcO3P74f85gVIcn1vdx97uE8D4xf9Rt6ISaRUT/vTyjuo/7155Injq6pQUTPjVxkp+v0D18iFfeWndf87jsj9+/eh/jQD8rlGhzgjsOgFMC36J/jXh13V9PaGjZGAlTQTXhF9t1Se/X/BFV2d+zJZtrV5t0sTTin/j8HI7bR0/9p/b76OFy7u5dub2w/9zAnM5zu333Pu+93abAKYvvi7l5MJrl3f0Uww6Q7czegsKJQK9rFh/tVWf/H6B9ZfdvLTuP+fxfH/qek5t/9zby72p9qa2f+nxec1Ue1PbP/f2cm+qvantX3p8XjPV3tT2z721s7fLBLBs8dMneZ66SJA1Xc/Xtu8PulLht78ctj6ykSeCrqq3tO6/F8zgI5TWUyu1Rhlrd2y7qWMca3dsO/xPJbC/9rtLAPOD/5rw2jP5eqJHx7UvD2ki0Fm9zvhN+Pv6PHVtbiWC1v13eEaUofUdOj7Cxc0mQ/aHjt80PuLgkP2h4yNc3GwyZH/o+E3jIw4O2R86PsJFU012lQCWLb5uzj51L1kxEc8v1Wg/TwS58A/1kQ+72dy9/VBa9/8BxOCbvnXuqx80OLFBn5+++onmB5v3+emrHzQ4sUGfn776ieYHm/f56asfNNhwg90kgOWLr5u5ufD/oqv7vHu9er/VvkqaCOb0ka+8tO4/53F7P1/vfP927+VHc3/5/nIPty3k/vL9272XH8395fvLPdy2kPvL92/35qgR2EUCKLP4upRjZ+8m/J91dXa2rq32lRDSRDCnj3zlpXX/OY/hfVt32w73KNvC/Nq2rPVha+bXtsM9yrYwv7Yta33Ymvm17XAPWuQEwieAsot/Tfj1eKbO8rVVyRPBnD4XSy//nWNrTp+Xni81c2zN6dPnf3p92fXH/1QCrfOfystb+9AJoGzw6bHN9Ixfgv9F99ITPjrL11b7eSKY00e+8tK6/5wH+xCAwNoEwiaAsuIvzCbKqfDnl2q0nycC9Z3ax3yprxWrm2pL/af2MV/mW1urm2pLfaf2MV/qS4EABGoRCJkAyou/8Ou5/XfdSwJvwm+PZr7q6uzGb/f2wx+Eqf2cPvKVl9b95zzYhwAE1iYQLgGsI/45ZhN+Pbf/9P6gttpPE8H7Q+fNnD5p//T9HFtz+qQ+0/dzbM3pk/rkPQQgsDWBUAlgffHPRcx+5E1n+boRrBHkiSDvozZqqz5/1b3yXw9V+76S22rNfx8X6iEAgTUIhEkA64v/5x1fO+M34bUnXITezvzzRGB9TPhNxNVHNmUjTwSqz0vr/nMe7EMAAmsT+NbaDkrYX1/8bZTXhF/HdNNSQq6SJ4Jrwq+26Y3OPBGcDV35p3X/V5BQBQEIrEbAfQLYTvx18zc94xdzuyH8w+79Z93LhFzHLBGkZ/zWX23Vx54aUnsV6y+7eVGd9bdjqpONFvzbnNlCAAJbEXCdALYT/xy3Ce+PugP2Wz9q8+Pu9Vn3MiFXnYoJt46pjYpGn/5onGyOLa37H8uJdhCAwBICbhNAHfG/Jry65q+z/C+6l553V0kTgZJBKvz2TLz6qO+URNC6/w4XBQIQ2IyAywRQR/x1mSU94zfh16UeFbuckycCO+M34TcRVx+7TJQnAvnKS+v+cx7sQwACaxN4vbaDqfbriL9Gqd/8V5GQm+ifK7J/LBGoXSr+qu8rlgj0rUB9zFfa3upa9Z+y4D0EILAFAVcJoJ74C7UE2ER4DHpLBGPaWhslgr7k0rp/Y8QWAhDYioCbS0B1xX8r3PiBAAQg4IfAq+Px+K7mcN48Ph7ePjzUHAK+KxI4nX5S0fvhcDz+RVX/OK9LQPpTu9TUPxeXgI6n0/lZmRoL0SXAw6nzX6u07v9wqJsAtO6sf7vx350BVFv/py727u7uaknP2a+bS0CCQWmZgP5yOn866vOuTq+0qE36V9b6GwzV6Qa7Fb1XnY5ZuWbfjrGFwLYEvOidmwQg/F6gbBsKeLsQkEDrpcdorWhfT02l4m5CbuKuP7ZTXZootG99u7fnYnWpfTvGFgLbEfCkc64SgJbAE5ztQgJPz//IznjokViVVNytzh7B1VNV991LkWOJIm1jiSKt65pSIFCBgDd9c5cAtCbeIFWIkwZdmpDrjN7O0iX8+oG8IXFP2wudHtHNBf+afbWlQGAbAh51zWUC0HJ4hLVNmLTsxYTczu7FwoTcvgXcEvexiSK13zJv5r4VAa965jYBaGG8QtsqaNrzc+0snW8B7cXBvmbsWcdcJwCFgWd4+wpTL7PhW4CXlWAcywl41y/3CUBL4B3i8jDBwkcC6bcAPbmjom8BKmkk2M92pJdzrJ3V6XJR3u6a/bNx/oFAUQJptBY1XNBYiASg+UaAWXBdGjalp3Zste/fc7Cne2xf1ZYc7B6B6uzbQ9rO+loiuGZffSkQKEfAIricxXUshUkAmn4UqOssVStW7exdwq4zeBU7szeBl4in7dRGQq8I0VNDaXs9VaSEoDN/lbSf2b8c4V8IlCAQSadCJQAtTiS4JYKpLRu3hH1IxE30028EJva "text/plain": [ "<PIL.Image.Image image mode=RGBA size=384x384>" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "The shield for shield_value = 0.9\n", "\n", "\n", "Computing new shield\n", "LOG: Starting with explicit model creation...\n", "Elapsed time is 0.05918574333190918 seconds.\n", "LOG: Starting with model checking...\n", "Elapsed time is 0.0002396106719970703 seconds.\n", "LOG: Starting to translate shield...\n", "Write to file shielding_files_20240924T133128_3pf0niht/shield.\n", "Elapsed time is 0.011339187622070312 seconds.\n" ] }, { "data": { "image/png": "iVBORw0KGgoAAAANSUhEUgAAAYAAAAGACAYAAACkx7W/AAAukklEQVR4Ae2dz64kyVWHq4fWIKRBIFtcPNJ4LC+84gEo8xB3h3mB4gFo7/oBWmyM2buewOzuCvEAcFl5xcoSlscWYwZhGTESYmTUxO/WPd1x41ZW/qnMjHMyvpCyszIy4pyIL079TlZW3uoXh8Ph7Y4CAQhAAALNEfiguRkzYQhAAAIQeCBAAiAQIAABCDRKgATQ6MIzbQhAAAIkAGIAAhCAQKMESACNLjzThgAEIEACIAYgAAEINEqABNDowjNtCEAAAiQAYgACEIBAowRIAI0uPNOGAAQgQAIgBiAAAQg0SoAE0OjCM20IQAACJABiAAIQgECjBEgAjS4804YABCBAAiAGIAABCDRKgATQ6MIzbQhAAAIkAGIAAhCAQKMESACNLjzThgAEIEACIAYgAAEINEqABNDowjNtCEAAAiQAYgACEIBAowRIAI0uPNOGAAQgQAIgBiAAAQg0SoAE0OjCM20IQAACJABiAAIQgECjBEgAjS4804YABCBAAiAGIAABCDRKgATQ6MIzbQhAAAIkAGIAAhCAQKMESACNLjzThgAEIEACIAYgAAEINEqABNDowjNtCEAAAi9rI3h9d1d1CF988e3dfnffM4a/S+f3aftmTzs7/Yv0Qjb/3Cqu3G/X/7/e/PGVbOgOgekEvvj2F9M7z9Dz5mc3uze3tzNYmmaiegLQsL/4ot4i7Hf/foHc36RzP0zbLx/b/FXaa+tKBBJ+tdem8kna1P6VDiaU7ftX8B+Oxwls5ulyPBzw3zD/3bfniaOoVpq+BaRr+vNFwiuR/37aJP7WUsL+adok6BJ7K3qtOp0z8Vcf9ZUN2ZLNoaUt/0Z3KJ252plf289ld6gd82v7of3mamd+bT+X3aF2zK/th/abq10tv3ONfw47zSaA84t/Tnj/MXH+p7R9ljZdzavkiaAUfrVRW/VRX3kamgja9X9+PRK6hUrprzxeyO07s6W/8vhdw4VelP7K44XcvjNb+iuP3zVc6MXa/haaxtVmm0wA5xf/ewlmfsVvwv/dR8h2FV8mArviN+E3EVc39T2XCOSrLK37f/85qyQz9/H59cd/F5dW+M89zwj2mksA3UGuL2y1lcJvt3ck5CplIjgn/Gr7Km3qq5InAvNzOvP+X6tv1f+JRPf6vCd1zas++33nr/Gtvn32+87j/zoCS/O9bnTr924qAVxefAnwj9NmV/wm/J+mOl3l/9njuTIR5Ff8Oqf+apvfJsoTgXzIV1la9/+ex+V1et9u7Kuhdoe2w/84AkO5Dm03znt/8h1rbwvtm0kAw4OqFH4ts8RZT/Tcp61MBKnq4TaPCb/aqK2J/LlEoD5dpXX/Jy7D16uL49P6sfbGtn/q7fnRWHtj2z/3+LRmrL2x7Z96e3401t7Y9s89Pq2Z295T63GPmkgAwxb/nPDa7R1dtev8D9JWJoJS+NVGbdXns7TJhkpfImjd/4lS/u+wdct7nH891c7UfuUoptqZ2g//TwnMxfGp1W0cbT4BDF/876cVlUirmPDnt3dU/yptZSK4T3VKCib8amOl/L5A9fIhX2Vp3X/J43Q8fP3of44A/M5Roc4IbDoBjAt+if454dd9fT2ho2RgJU8E54RfbdWn/L7gs1RnfsyW7a1ebfLE04p/4/B8P24d3/ef2u+9hdOrqXam9sP/UwJTOU7t99T7to82mwDGL75u5ZTCa7d39FMMukK3K3oLCiUCbVasv9qqT/l9gfWX3bK07r/k8fR47HqObf/U2/OjsfbGtn/u8WnNWHtj2z/19vxorL2x7Z97fFoz1t7Y9k+9tXO0yQRw3eLnT/Lcp0iQNd3P177rD7py4be/HLY+slEmglTVWVr33wmm9xFK66mVWqIMtTu03dgxDrU7tB3+xxLYXvvNJYDpwX9OeO2ZfD3Ro/M6loc8EeiqXlf8Jvxdfe5Tm0uJoHX/Cc+A0re+fecHuLjYpM9+3/mLxgec7LPfd36Ai4tN+uz3nb9ofMDJPvt95we4aKrJphLAdYuvL2fv0yYrJuLlrRodl4mgFP6+PvJhXzanl+9K6/7fgeh90bXOXfW9Bkc26PLTVT/SfG/zLj9d9b0GRzbo8tNVP9J8b/MuP131vQYbbrCZBHD94uvL3FL4f5HqXqXtxeNexyp5IpjSR77K0rr/ksfl43K9y+PLva8/W/orj6/3cNlC6a88vtz7+rOlv/L4eg+XLZT+yuPLvTlrBDaRAOZZfN3Ksat3E/5PU51drWuvYyWEPBFM6SNfZWndf8mj/9jW3fb9PeZtYX5tP6/1fmvm1/b9PeZtYX5tP6/1fmvm1/b9PWhREgifAOZd/HPCr8czdZWvvUqZCKb0OVl6/u8UW1P6PPd8qplia0qfLv/j6+ddf/yPJdA6/7G8vLUPnQDmDT49tplf8UvwP0ubnvDRVb72Oi4TwZQ+8lWW1v2XPDiGAASWJhA2Acwr/sJsopwLf3mrRsdlIlDfsX3Ml/pasbqxttR/bB/zZb61t7qxttR3bB/zpb4UCECgFoGQCWB+8Rd+Pbf/Nm0SeBN+ezTzRaqzL37Ty3d/EKb2U/rIV1la91/y4BgCEFiaQLgEsIz4l5hN+PXc/v3jSe11nCeCx1MPuyl98v756ym2pvTJfeavp9ia0if3yWsIQGBtAqESwPLiX4qY/cibrvL1RbBGUCaCso/aqK36/CBt5a+Hqn1XKW215r+LC/UQgMASBMIkgOXF/1Xia1f8Jrz2hIvQ25V/mQisjwm/ibj6yKZslIlA9WVp3X/Jg2MIQGBpAh8s7WAO+8uLv43ynPDrnL60lJCrlIngnPCrbf5FZ5kIHgyd+ad1/2eQUAUBCCxGwH0CWE/89eVvfsUv5vaF8PfS60/TZkKuc5YI8it+66+26mNPDam9ivWX3bKozvrbOdXJRgv+bc7sIQCBtQi4TgDriX+J24T3++mE/daP2vwwbZ+mzYRcdSom3DqnNioaff6jcbI5tLTufygn2kEAAtcQcJsA6oj/OeHVPX9d5X+WNj3vrpInAiWDXPjtmXj1Ud8xiaB1/wkXBQIQWI2AywRQR/x1myW/4jfh160eFbudUyYCu+I34TcRVx+7TVQmAvkqS+v+Sx4cQwACSxN4ubSDsfbriL9Gqd/8V5GQm+g/VBT/WCJQu1z8Vd9VLBHoU4H6mK+8vdW16j9nwWsIQGANAq4SQD3xF2oJsInwEPSWCIa0tTZKBF3JpXX/xog9BCCwFgE3t4Dqiv9auPEDAQhAwA+BF4fD4W3N4by+u9u9ub2tOQR8VyRwPP6oovfd7nD4y6r+cV6XgPSndqmpfy5uAR2Ox4dnZWosREqAu2PyX6u07n+3q5sAtO6sf7vxn64Aqq3/fYq9m5ubWtLz4NfNLSDBoLRMQH85XT4d9SrVacuL2uR/Za2/wVCdvmC3oteq0zkr5+zbOfYQWJeAF71zkwCE3wuUdUMBbycCEmhteozWio711FQu7ibkJu76YzvV5YlCx9Y3vXwoVpfbt3PsIbAeAU865yoBaAk8wVkvJPD09I/sjIceiVXJxd3q7BFcPVW1T5sixxJF3sYSRV6XmlIgUIGAN31zlwC0Jt4gVYiTBl2akOuK3q7SJfz6gbw+cc/bC50e0S0F/5x9taVAYB0CHnXNZQLQcniEtU6YtOzFhNyu7sXChNw+BVwS96GJIrffMm/mvhYBr3rmNgFoYbxCWyto2vNz7iqdTwHtxcG2ZuxZx1wnAIWBZ3jbClMvs+FTgJeVYBzXE/CuX+4TgJbAO8TrwwQL7wnknwL05I6KPgWo5JFgP9uR386xdlan20Vlu3P2H4zzDwRmJZBH66yGZzQWIgFovhFgzrguDZvSUzu22vtHDvZ0jx2r2pKDfUegOvv0kLezvpYIztlXXwoE5iNgETyfxWUshUkAmn4UqMssVStW7epdwq4reBW7sjeBl4jn7dRGQq8I0VNDeXs9VaSEoCt/lbyf2T+d4V8IzEEgkk6FSgBanEhw5wimtmxcEvY+ETfRzz8RmNhfShxtEWa "text/plain": [ "<PIL.Image.Image image mode=RGBA size=384x384>" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "The shield for shield_value = 0.99\n", "\n", "\n", "Computing new shield\n", "LOG: Starting with explicit model creation...\n", "Elapsed time is 0.05561947822570801 seconds.\n", "LOG: Starting with model checking...\n", "Elapsed time is 0.00025653839111328125 seconds.\n", "LOG: Starting to translate shield...\n", "Write to file shielding_files_20240924T133129_kc6xcewk/shield.\n", "Elapsed time is 0.012254714965820312 seconds.\n" ] }, { "data": { "image/png": "iVBORw0KGgoAAAANSUhEUgAAAYAAAAGACAYAAACkx7W/AAAubElEQVR4Ae2dz44ky1WHa8zoIqSLQFg0WLq+lhde8QA0PETv8BMUD8B4Nw8wO+ABXE9gdr1CPAA0K1askLB8sXTNRVhGXAlxZTTkr6vPTHR0ZeW/yIxzMr6QarIyMuKciC9O/U5WZnbNq+Px+P5AgQAEIACB5gh8q7kZM2EIQAACEHgkQAIgECAAAQg0SoAE0OjCM20IQAACJABiAAIQgECjBEgAjS4804YABCBAAiAGIAABCDRKgATQ6MIzbQhAAAIkAGIAAhCAQKMESACNLjzThgAEIEACIAYgAAEINEqABNDowjNtCEAAAiQAYgACEIBAowRIAI0uPNOGAAQgQAIgBiAAAQg0SoAE0OjCM20IQAACJABiAAIQgECjBEgAjS4804YABCBAAiAGIAABCDRKgATQ6MIzbQhAAAIkAGIAAhCAQKMESACNLjzThgAEIEACIAYgAAEINEqABNDowjNtCEAAAiQAYgACEIBAowRIAI0uPNOGAAQgQAIgBiAAAQg0SoAE0OjCM20IQAACJABiAAIQgECjBEgAjS4804YABCBAAiAGIAABCDRKgATQ6MIzbQhAAAKvayN4e39fdQhfffX9w+3hYWAMf9Mdv+1e3x1oZ4f/rXsjm39mFQu3+/X/rzd/sJAN3SEwn8BX3/9qfucCPW9+enN4d3dXwNI8E9UTgIb91Vf1FuH28O9XyP1Vd+yvu9fPn9r8RbfVqy8RSPjVXi+Vz7qX2r/Rzoyyf/8K/uPpNINNmS6n4xH/DfM/fL9MHEW10vQlIJ3TXy4SXon8j7qXxN9aStg/714SdIm9Fb1XnY6Z+KuP+sqGbMnm2NKWf6M7lk6pdubXtqXsjrVjfm07tl+pdubXtqXsjrVjfm07tl+pdrX8lhp/CTvNJoDLi39JeP++4/wP3euL7qWzeZU0EeTCrzZqqz7qK09jE0G7/i+vR4dupZL7y/dXcvvBbO4v3//QcKU3ub98fyW3H8zm/vL9Dw1XerO1v5Wmsdhskwng8uL/sIOZnvGb8P/JE2Q7i88TgZ3xm/CbiKub+l5KBPKVl9b9f/yelZMpvX95/fHfx6UV/qXnGcFecwmgP8h1w1avXPjt8o6EXCVPBJeEX23fdC/1VUkTgfk5H/n4r9W36v9Mon99PpJa8m7I/tDxJb7Vd8j+0HH8LyOwNt9lo9u+d1MJ4PriS4B/0r3sjN+E//OuTmf5f/p0LE8E6Rm/jqm/2qaXidJEIB/ylZfW/X/kcX2dPrab+m6s3bHt8D+NwFiuY9tN8z6cfKfa20P7ZhLA+KDKhV/LLHHWEz0P3StPBF3V42UeE361UVsT+UuJQH36Suv+z1zGr1cfx+f1U+1Nbf/c28u9qfamtn/p8XnNVHtT2z/39nJvqr2p7V96fF5T2t5z63H3mkgA4xb/kvDa5R2dtev4X3avPBHkwq82aqs+X3Qv2VAZSgSt+z9TSv8dt25pj8vv59qZ2y8fxVw7c/vh/zmBUhyfW93H3u4TwPjF/1G3ohJpFRP+9PKO6t90rzwRPHR1Sgom/GpjJb9foHr5kK+8tO4/53HeH79+9L9EAH6XqFBnBHadAKYFv0T/kvDrur6e0FEysJImgkvCr7bqk98v+KKrMz9my7ZWrzZp4mnFv3F4uZ22jh/7z+330cL53Vw7c/vh/zmBuRzn9nvufd97u00A0xdfl3Jy4bXLO/opBp2h2xm9BYUSgV5WrL/aqk9+v8D6y25eWvef83i+P3U9p7Z/7u3l3lR7U9u/9Pi8Zqq9qe2fe3u5N9Xe1PYvPT6vmWpvavvn3trZ22UCWLb46ZM8D10kyJqu52vb9wddqfDbXw5bH9nIE0FX1Vta998LZvARSuuplVqjjLU7tt3UMY61O7Yd/qcS2F/73SWA+cF/SXjtmXw90aPj2peHNBHorF5n/Cb8fX0eujbXEkHr/js8I8rQ+g4dH+HiapMh+0PHrxofcXDI/tDxES6uNhmyP3T8qvERB4fsDx0f4aKpJrtKAMsWXzdnH7qXrJiI55dqtJ8nglz4h/rIh91s7t5+KK37/wBi8E3fOvfVDxqc2KDPT1/9RPODzfv89NUPGpzYoM9PX/1E84PN+/z01Q8abLjBbhLA8sXXzdxc+P+tq3vTvV49bbWvkiaCOX3kKy+t+895XN/P1zvfv957+dHcX76/3MN1C7m/fP967+VHc3/5/nIP1y3k/vL96705agR2kQDKLL4u5djZuwn/512dna1rq30lhDQRzOkjX3lp3X/OY3jf1t22wz3KtjC/ti1rfdia+bXtcI+yLcyvbctaH7Zmfm073IMWOYHwCaDs4l8Sfj2eqbN8bVXyRDCnz9nSy3/n2JrT56Xnc80cW3P69PmfXl92/fE/lUDr/Kfy8tY+dAIoG3x6bDM945fgf9G99ISPzvK11X6eCOb0ka+8tO4/58E+BCCwNoGwCaCs+AuziXIq/PmlGu3niUB9p/YxX+prxeqm2lL/qX3Ml/nW1uqm2lLfqX3Ml/pSIACBWgRCJoDy4i/8em7/ffeSwJvw26OZr7o6u/Hbvf3wB2FqP6ePfOWldf85D/YhAIG1CYRLAOuIf47ZhF/P7T88HdRW+2kieDr0uJnTJ+2fvp9ja06f1Gf6fo6tOX1Sn7yHAAS2JhAqAawv/rmI2Y+86SxfN4I1gjwR5H3URm3V5y+7V/7roWrfV3Jbrfnv40I9BCCwBoEwCWB98X/T8bUzfhNee8JF6O3MP08E1seE30RcfWRTNvJEoPq8tO4/58E+BCCwNoFvre2ghP31xd9GeUn4dUw3LSXkKnkiuCT8apve6MwTwaOhC/+07v8CEqogAIHVCLhPANuJv27+pmf8Ym43hH/Yvf+8e5mQ65glgvSM3/qrrfrYU0Nqr2L9ZTcvqrP+dkx1stGCf5szWwhAYCsCrhPAduKf4zbh/VF3wH7rR23+unt93r1MyFWnYsKtY2qjotGnPxonm2NL6/7HcqIdBCCwhIDbBFBH/C8Jr6756yz/i+6l591V0kSgZJAKvz0Trz7qOyURtO6/w0WBAAQ2I+AyAdQRf11mSc/4Tfh1qUfFLufkicDO+E34TcTVxy4T5YlAvvLSuv+cB/sQgMDaBF6v7WCq/Trir1HqN/9VJOQm+o8V2T+WCNQuFX/V9xVLBPpWoD7mK21vda36T1nwHgIQ2IKAqwRQT/yFWgJsIjwGvSWCMW2tjRJBX3Jp3b8xYgsBCGxFwM0loLrivxVu/EAAAhDwQ+DV8Xh8X3M4b+/vD+/u7moOAd8VCZxOP67o/XA4Hv+8qn+c1yUg/aldauqfi0tAx9Pp8VmZGgvRJcDDqfNfq7Tu/3ComwC07qx/u/HfnQFUW/+HLvZubm5qSc+jXzeXgASD0jIB/eV0/nTUm65Or7SoTfpX1vobDNXpBrsVvVedjlm5ZN+OsYXAtgS86J2bBCD8XqBsGwp4OxOQQOulx2itaF9PTaXibkJu4q4/tlNdmii0b327t4/F6lL7dowtBLYj4EnnXCUALYEnONuFBJ6e/5Gd8dAjsSqpuFudPYKrp6puu5cixxJF2sYSRVrXNaVAoAIBb/rmLgFoTbxBqhAnDbo0IdcZvZ2lS/j1A3lD4p62Fzo9opsL/iX7akuBwDYEPOqaywSg5fAIa5swadmLCbmd3YuFCbl9C7gm7mMTRWq/Zd7MfSsCXvXMbQLQwniFtlXQtOfn0lk63wLai4N9zdizjrlOAAoDz/D2FaZeZsO3AC8rwTiWE/CuX+4TgJbAO8TlYYKFjwTSbwF6ckdF3wJU0kiwn+1IL+dYO6vT5aK83SX7j8b5BwJFCaTRWtRwQWMhEoDmGwFmwXVp2JSe2rHVvn3iYE/32L6qLTnYPQLV2beHtJ31tURwyb76UiBQjoBFcDmL61gKkwA0/ShQ11mqVqza2buEXWfwKnZmbwIvEU/bqY2EXhGip4bS9nqqSAlBZ/4qaT+zfz7CvxAoQSCSToVKAFqcSHBLBFNbNq4J+5CIm+in3whM7K8ljrY "text/plain": [ "<PIL.Image.Image image mode=RGBA size=384x384>" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "The shield for shield_value = 0.999\n", "\n", "\n", "Computing new shield\n", "LOG: Starting with explicit model creation...\n", "Elapsed time is 0.05743050575256348 seconds.\n", "LOG: Starting with model checking...\n", "Elapsed time is 0.0002510547637939453 seconds.\n", "LOG: Starting to translate shield...\n", "Write to file shielding_files_20240924T133129_xvlqgzvq/shield.\n", "Elapsed time is 0.011241436004638672 seconds.\n" ] }, { "data": { "image/png": "iVBORw0KGgoAAAANSUhEUgAAAYAAAAGACAYAAACkx7W/AAAufElEQVR4Ae2dz44ky1WHa8zoIqSLQFg0WLq+lhde8QA0PETv8BMUD8B4Nw8wO+ABXE9gdr1CPAA0K1askLB8sXTNRVhGXAlxZTTkr6vPTHR0ZeW/yIxzMr6QarIyMuKciC9O/U5WZnbNq+Px+P5AgQAEIACB5gh8q7kZM2EIQAACEHgkQAIgECAAAQg0SoAE0OjCM20IQAACJABiAAIQgECjBEgAjS4804YABCBAAiAGIAABCDRKgATQ6MIzbQhAAAIkAGIAAhCAQKMESACNLjzThgAEIEACIAYgAAEINEqABNDowjNtCEAAAiQAYgACEIBAowRIAI0uPNOGAAQgQAIgBiAAAQg0SoAE0OjCM20IQAACJABiAAIQgECjBEgAjS4804YABCBAAiAGIAABCDRKgATQ6MIzbQhAAAIkAGIAAhCAQKMESACNLjzThgAEIEACIAYgAAEINEqABNDowjNtCEAAAiQAYgACEIBAowRIAI0uPNOGAAQgQAIgBiAAAQg0SoAE0OjCM20IQAACJABiAAIQgECjBEgAjS4804YABCBAAiAGIAABCDRKgATQ6MIzbQhAAAKvayN4e39fdQhfffX9w+3hYWAMf9Mdv+1e3x1oZ4f/rXsjm39mFQu3+/X/rzd/sJAN3SEwn8BX3/9qfucCPW9+enN4d3dXwNI8E9UTgIb91Vf1FuH28O9XyP1Vd+yvu9fPn9r8RbfVqy8RSPjVXi+Vz7qX2r/Rzoyyf/8K/uPpNINNmS6n4xH/DfM/fL9MHEW10vQlIJ3TXy4SXon8j7qXxN9aStg/714SdIm9Fb1XnY6Z+KuP+sqGbMnm2NKWf6M7lk6pdubXtqXsjrVjfm07tl+pdubXtqXsjrVjfm07tl+pdrX8lhp/CTvNJoDLi39JeP++4/wP3euL7qWzeZU0EeTCrzZqqz7qK09jE0G7/i+vR4dupZL7y/dXcvvBbO4v3//QcKU3ub98fyW3H8zm/vL9Dw1XerO1v5Wmsdhskwng8uL/sIOZnvGb8P/JE2Q7i88TgZ3xm/CbiKub+l5KBPKVl9b9f/yelZMpvX95/fHfx6UV/qXnGcFecwmgP8h1w1avXPjt8o6EXCVPBJeEX23fdC/1VUkTgfk5H/n4r9W36v9Mon99PpJa8m7I/tDxJb7Vd8j+0HH8LyOwNt9lo9u+d1MJ4PriS4B/0r3sjN+E//OuTmf5f/p0LE8E6Rm/jqm/2qaXidJEIB/ylZfW/X/kcX2dPrab+m6s3bHt8D+NwFiuY9tN8z6cfKfa20P7ZhLA+KDKhV/LLHHWEz0P3StPBF3V42UeE361UVsT+UuJQH36Suv+z1zGr1cfx+f1U+1Nbf/c28u9qfamtn/p8XnNVHtT2z/39nJvqr2p7V96fF5T2t5z63H3mkgA4xb/kvDa5R2dtev4X3avPBHkwq82aqs+X3Qv2VAZSgSt+z9TSv8dt25pj8vv59qZ2y8fxVw7c/vh/zmBUhyfW93H3u4TwPjF/1G3ohJpFRP+9PKO6t90rzwRPHR1Sgom/GpjJb9foHr5kK+8tO4/53HeH79+9L9EAH6XqFBnBHadAKYFv0T/kvDrur6e0FEysJImgkvCr7bqk98v+KKrMz9my7ZWrzZp4mnFv3F4uZ22jh/7z+330cL53Vw7c/vh/zmBuRzn9nvufd97u00A0xdfl3Jy4bXLO/opBp2h2xm9BYUSgV5WrL/aqk9+v8D6y25eWvef83i+P3U9p7Z/7u3l3lR7U9u/9Pi8Zqq9qe2fe3u5N9Xe1PYvPT6vmWpvavvn3trZ22UCWLb46ZM8D10kyJqu52vb9wddqfDbXw5bH9nIE0FX1Vta998LZvARSuuplVqjjLU7tt3UMY61O7Yd/qcS2F/73SWA+cF/SXjtmXw90aPj2peHNBHorF5n/Cb8fX0eujbXEkHr/js8I8rQ+g4dH+HiapMh+0PHrxofcXDI/tDxES6uNhmyP3T8qvERB4fsDx0f4aKpJrtKAMsWXzdnH7qXrJiI55dqtJ8nglz4h/rIh91s7t5+KK37/wBi8E3fOvfVDxqc2KDPT1/9RPODzfv89NUPGpzYoM9PX/1E84PN+/z01Q8abLjBbhLA8sXXzdxc+P+tq3vTvV49bbWvkiaCOX3kKy+t+895XN/P1zvfv957+dHcX76/3MN1C7m/fP967+VHc3/5/nIP1y3k/vL96705agR2kQDKLL4u5djZuwn/512dna1rq30lhDQRzOkjX3lp3X/OY3jf1t22wz3KtjC/ti1rfdia+bXtcI+yLcyvbctaH7Zmfm073IMWOYHwCaDs4l8Sfj2eqbN8bVXyRDCnz9nSy3/n2JrT56Xnc80cW3P69PmfXl92/fE/lUDr/Kfy8tY+dAIoG3x6bDM945fgf9G99ISPzvK11X6eCOb0ka+8tO4/58E+BCCwNoGwCaCs+AuziXIq/PmlGu3niUB9p/YxX+prxeqm2lL/qX3Ml/nW1uqm2lLfqX3Ml/pSIACBWgRCJoDy4i/8em7/ffeSwJvw26OZr7o6u/Hbvf3wB2FqP6ePfOWldf85D/YhAIG1CYRLAOuIf47ZhF/P7T88HdRW+2kieDr0uJnTJ+2fvp9ja06f1Gf6fo6tOX1Sn7yHAAS2JhAqAawv/rmI2Y+86SxfN4I1gjwR5H3URm3V5y+7V/7roWrfV3Jbrfnv40I9BCCwBoEwCWB98X/T8bUzfhNee8JF6O3MP08E1seE30RcfWRTNvJEoPq8tO4/58E+BCCwNoFvre2ghP31xd9GeUn4dUw3LSXkKnkiuCT8apve6MwTwaOhC/+07v8CEqogAIHVCLhPANuJv27+pmf8Ym43hH/Yvf+8e5mQ65glgvSM3/qrrfrYU0Nqr2L9ZTcvqrP+dkx1stGCf5szWwhAYCsCrhPAduKf4zbh/VF3wH7rR23+unt93r1MyFWnYsKtY2qjotGnPxonm2NL6/7HcqIdBCCwhIDbBFBH/C8Jr6756yz/i+6l591V0kSgZJAKvz0Trz7qOyURtO6/w0WBAAQ2I+AyAdQRf11mSc/4Tfh1qUfFLufkicDO+E34TcTVxy4T5YlAvvLSuv+cB/sQgMDaBF6v7WCq/Trir1HqN/9VJOQm+o8V2T+WCNQuFX/V9xVLBPpWoD7mK21vda36T1nwHgIQ2IKAqwRQT/yFWgJsIjwGvSWCMW2tjRJBX3Jp3b8xYgsBCGxFwM0loLrivxVu/EAAAhDwQ+DV8Xh8X3M4b+/vD+/u7moOAd8VCZxOP67o/XA4Hv+8qn+c1yUg/aldauqfi0tAx9Pp8VmZGgvRJcDDqfNfq7Tu/3ComwC07qx/u/HfnQFUW/+HLvZubm5qSc+jXzeXgASD0jIB/eV0/nTUm65Or7SoTfpX1vobDNXpBrsVvVedjlm5ZN+OsYXAtgS86J2bBCD8XqBsGwp4OxOQQOulx2itaF9PTaXibkJu4q4/tlNdmii0b327t4/F6lL7dowtBLYj4EnnXCUALYEnONuFBJ6e/5Gd8dAjsSqpuFudPYKrp6puu5cixxJF2sYSRVrXNaVAoAIBb/rmLgFoTbxBqhAnDbo0IdcZvZ2lS/j1A3lD4p62Fzo9opsL/iX7akuBwDYEPOqaywSg5fAIa5swadmLCbmd3YuFCbl9C7gm7mMTRWq/Zd7MfSsCXvXMbQLQwniFtlXQtOfn0lk63wLai4N9zdizjrlOAAoDz/D2FaZeZsO3AC8rwTiWE/CuX+4TgJbAO8TlYYKFjwTSbwF6ckdF3wJU0kiwn+1IL+dYO6vT5aK83SX7j8b5BwJFCaTRWtRwQWMhEoDmGwFmwXVp2JSe2rHVvn3iYE/32L6qLTnYPQLV2beHtJ31tURwyb76UiBQjoBFcDmL61gKkwA0/ShQ11mqVqza2buEXWfwKnZmbwIvEU/bqY2EXhGip4bS9nqqSAlBZ/4qaT+zfz7CvxAoQSCSToVKAFqcSHBLBFNbNq4J+5CIm+in3whM7K8ljrY "text/plain": [ "<PIL.Image.Image image mode=RGBA size=384x384>" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "The shield for shield_value = 0.9999\n", "\n", "\n", "Computing new shield\n", "LOG: Starting with explicit model creation...\n", "Elapsed time is 0.057801008224487305 seconds.\n", "LOG: Starting with model checking...\n", "Elapsed time is 0.0002875328063964844 seconds.\n", "LOG: Starting to translate shield...\n", "Elapsed time is 0.011219024658203125 seconds.\n", "Write to file shielding_files_20240924T133129_9qlpdi5z/shield.\n" ] }, { "data": { "image/png": "iVBORw0KGgoAAAANSUhEUgAAAYAAAAGACAYAAACkx7W/AAAugUlEQVR4Ae2dT44kyXWno6hCCwJakCBiUiJANcEFVzrA5MwhcieeIHSAKe7qALXT6ACME3B2uRJ0AClnpZVWAoZgi0BTLYigoAYENSjU+C8jX6WlZXj4P3O399w+A6I83NzsPbPPXvyeh7tn1Jvj8fjxQIEABCAAgeYIfKe5GTNhCEAAAhB4JEACIBAgAAEINEqABNDowjNtCEAAAiQAYgACEIBAowRIAI0uPNOGAAQgQAIgBiAAAQg0SoAE0OjCM20IQAACJABiAAIQgECjBEgAjS4804YABCBAAiAGIAABCDRKgATQ6MIzbQhAAAIkAGIAAhCAQKMESACNLjzThgAEIEACIAYgAAEINEqABNDowjNtCEAAAiQAYgACEIBAowRIAI0uPNOGAAQgQAIgBiAAAQg0SoAE0OjCM20IQAACJABiAAIQgECjBEgAjS4804YABCBAAiAGIAABCDRKgATQ6MIzbQhAAAIkAGIAAhCAQKMESACNLjzThgAEIEACIAYgAAEINEqABNDowjNtCEAAAiQAYgACEIBAowRIAI0uPNOGAAQgQAIgBiAAAQg0SoAE0OjCM20IQAACb2sjeH9/X3UIX3/9w8Pt4WFgDP+nO37bvf50oJ0d/qfujWz+uVUs3O7X//+7+eOFbOgOgfkEvv7h1/M7F+h58/Obw4e7uwKW5pmongA07K+/rrcIt4d/vkLuf3fH/qp7/fKpzf/qtnr1JQIJv9rrpfL97qX277Qzo+zfv4L/eDrNYFOmy+l4xH/D/A8/LBNHUa00fQlI5/SXi4RXIv+T7iXxt5YS9i+6lwRdYm9F71WnYyb+6qO+siFbsjm2tOXf6I6lU6qd+bVtKbtj7Zhf247tV6qd+bVtKbtj7Zhf247tV6pdLb+lxl/CTrMJ4PLiXxLev+04/133+rJ76WxeJU0EufCrjdqqj/rK09hE0K7/y+vRoVup5P7y/ZXcfjKb+8v3PzVc6U3uL99fye0ns7m/fP9Tw5XebO1vpWksNttkAri8+D/uYKZn/Cb8/+MJsp3F54nAzvhN+E3E1U19LyUC+cpL6/6fv2flZErvX15//PdxaYV/6XlGsNdcAugPct2w1SsXfru8IyFXyRPBJeFX23fdS31V0kRgfs5Hnv+1+lb9n0n0r88zqSXvhuwPHV/iW32H7A8dx/8yAmvzXTa67Xs3lQCuL74E+Gfdy874Tfi/6Op0lv8/n47liSA949cx9Vfb9DJRmgjkQ77y0rr/Zx7X1+m53dR3Y+2ObYf/aQTGch3bbpr34eQ71d4e2jeTAMYHVS78WmaJs57oeeheeSLoqh4v85jwq43amshfSgTq01da93/mMn69+ji+rJ9qb2r7l95e7021N7X9a48va6bam9r+pbfXe1PtTW3/2uPLmtL2XlqPu9dEAhi3+JeE1y7v6Kxdx/+ye+WJIBd+tVFb9fmye8mGylAiaN3/mVL677h1S3tcfj/Xztx++Sjm2pnbD/8vCZTi+NLqPvZ2nwDGL/5PuhWVSKuY8KeXd1T/rnvlieChq1NSMOFXGyv5/QLVy4d85aV1/zmP8/749aP/JQLwu0SFOiOw6wQwLfgl+peEX9f19YSOkoGVNBFcEn61VZ/8fsGXXZ35MVu2tXq1SRNPK/6Nw+vttHV87j+337OF87u5dub2w/9LAnM5zu330vu+93abAKYvvi7l5MJrl3f0Uww6Q7czegsKJQK9rFh/tVWf/H6B9ZfdvLTuP+fxcn/qek5t/9Lb672p9qa2f+3xZc1Ue1Pbv/T2em+qvantX3t8WTPV3tT2L721s7fLBLBs8dMneR66SJA1Xc/Xtu8PulLht78ctj6ykSeCrqq3tO6/F8zgI5TWUyu1Rhlrd2y7qWMca3dsO/xPJbC/9rtLAPOD/5Lw2jP5eqJHx7UvD2ki0Fm9zvhN+Pv6PHRtriWC1v13eEaUofUdOj7CxdUmQ/aHjl81PuLgkP2h4yNcXG0yZH/o+FXjIw4O2R86PsJFU012lQCWLb5uzj50L1kxEc8v1Wg/TwS58A/1kQ+72dy9/VRa9/8JxOCbvnXuqx80OLFBn5+++onmB5v3+emrHzQ4sUGfn776ieYHm/f56asfNNhwg90kgOWLr5u5ufD/U1f3rnu9edpqXyVNBHP6yFdeWvef87i+n693vn+99/Kjub98f7mH6xZyf/n+9d7Lj+b+8v3lHq5byP3l+9d7c9QI7CIBlFl8Xcqxs3cT/i+6Ojtb11b7SghpIpjTR77y0rr/nMfwvq27bYd7lG1hfm1b1vqwNfNr2+EeZVuYX9uWtT5szfzadrgHLXIC4RNA2cW/JPx6PFNn+dqq5IlgTp+zpdf/zrE1p89rz+eaObbm9OnzP72+7PrjfyqB1vlP5eWtfegEUDb49NhmesYvwf+ye+kJH53la6v9PBHM6SNfeWndf86DfQhAYG0CYRNAWfEXZhPlVPjzSzXazxOB+k7tY77U14rVTbWl/lP7mC/zra3VTbWlvlP7mC/1pUAAArUIhEwA5cVf+PXc/sfuJYE34bdHM990dXbjt3v76Q/C1H5OH/nKS+v+cx7sQwACaxMIlwDWEf8cswm/ntt/eDqorfbTRPB06HEzp0/aP30/x9acPqnP9P0cW3P6pD55DwEIbE0gVAJYX/xzEbMfedNZvm4EawR5Isj7qI3aqs9fdq/810PVvq/ktlrz38eFeghAYA0CYRLA+uL/ruNrZ/wmvPaEi9DbmX+eCKyPCb+JuPrIpmzkiUD1eWndf86DfQhAYG0C31nbQQn764u/jfKS8OuYblpKyFXyRHBJ+NU2vdGZJ4JHQxf+ad3/BSRUQQACqxFwnwC2E3/d/E3P+MXcbgj/uHv/RfcyIdcxSwTpGb/1V1v1saeG1F7F+stuXlRn/e2Y6mSjBf82Z7YQgMBWBFwngO3EP8dtwvuT7oD91o/a/FX3+qJ7mZCrTsWEW8fURkWjT380TjbHltb9j+VEOwhAYAkBtwmgjvhfEl5d89dZ/pfdS8+7q6SJQMkgFX57Jl591HdKImjdf4eLAgEIbEbAZQKoI/66zJKe8Zvw61KPil3OyROBnfGb8JuIq49dJsoTgXzlpXX/OQ/2IQCBtQm8XdvBVPt1xF+j1G/+q0jITfQfK7J/LBGoXSr+qu8rlgj0rUB9zFfa3upa9Z+y4D0EILAFAVcJoJ74C7UE2ER4DHpLBGPaWhslgr7k0rp/Y8QWAhDYioCbS0B1xX8r3PiBAAQg4IfAm+Px+LHmcN7f3x8+3N3VHAK+KxI4nX5a0fvhcDz+RVX/OK9LQPpTu9TUPxeXgI6n0+OzMjUWokuAh1Pnv1Zp3f/hUDcBaN1Z/3bjvzsDqLb+D13s3dzc1JKeR79uLgEJBqVlAvrL6fzpqHddnV5pUZv0r6z1Nxiq0w12K3qvOh2zcsm+HWMLgW0JeNE7NwlA+L1A2TYU8HYmIIHWS4/RWtG+nppKxd2E3MRdf2ynujRRaN/6dm8fi9Wl9u0YWwhsR8CTzrlKAFoCT3C2Cwk8vfwjO+OhR2JVUnG3OnsEV09V3XYvRY4lirSNJYq0rmtKgUAFAt70zV0C0Jp4g1QhThp0aUKuM3o7S5fw6wfyhsQ9bS90ekQ3F/xL9tWWAoFtCHjUNZcJQMvhEdY2YdKyFxNyO7sXCxNy+xZwTdzHJorUfsu8mftWBLzqmdsEoIXxCm2roGnPz6WzdL4FtBcH+5qxZx1znQAUBp7h7StMvcyGbwFeVoJxLCfgXb/cJwAtgXeIy8MEC88E0m8BenJHRd8CVNJIsJ/tSC/nWDur0+WivN0l+4/G+QcCRQmk0VrUcEFjIRKA5hsBZsF1adiUntqx1b594mBP99i+qi052D0C1dm3h7Sd9bVEcMm++lIgUI6ARXA5i+tYCpMANP0oUNdZqlas2tm7hF1n8Cp2Zm8CLxFP26mNhF4RoqeG0vZ6qkgJQWf+Kmk/s38+wr8QKEEgkk6FSgBanEhwSwRTWzauCfuQiJvop98ITOy "text/plain": [ "<PIL.Image.Image image mode=RGBA size=384x384>" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "The shield for shield_value = 1.0\n", "Training with shield:\n" ] }, { "data": { "image/png": "iVBORw0KGgoAAAANSUhEUgAAAYAAAAGACAYAAACkx7W/AAAufElEQVR4Ae2dT44kyXWno6hCCwJakCBicthAsxtccMXVrCalQ+ROnAuEDqDirg5QO0oHYJyA2uVK0AGk1Ga44orAECwS6FYLIiioAUENCjX2i8hXZWkZHv4nzN3ec/8M8PJwc7P3zD578XseHp5RL/b7/bsdBQIQgAAENkfgW5ubMROGAAQgAIEjARIAgQABCEBgowRIABtdeKYNAQhAgARADEAAAhDYKAESwEYXnmlDAAIQIAEQAxCAAAQ2SoAEsNGFZ9oQgAAESADEAAQgAIGNEiABbHThmTYEIAABEgAxAAEIQGCjBEgAG114pg0BCECABEAMQAACENgoARLARheeaUMAAhAgARADEIAABDZKgASw0YVn2hCAAARIAMQABCAAgY0SIAFsdOGZNgQgAAESADEAAQhAYKMESAAbXXimDQEIQIAEQAxAAAIQ2CgBEsBGF55pQwACECABEAMQgAAENkqABLDRhWfaEIAABEgAxAAEIACBjRIgAWx04Zk2BCAAARIAMQABCEBgowRIABtdeKYNAQhAgARADEAAAhDYKAESwEYXnmlDAAIQIAEQAxCAAAQ2SoAEsNGFZ9oQgAAEXrZG8Pr+vukQvvrqe7vb3UPPGP4unb9N23d72tnpX6cXsvmXVnHlfr3+/9/N/7ySDd0hMJ3AV9/7anrnCj1vfnmze3N3V8HSNBPNE4CG/dVX7RbhdvcvF8j9TTr3t2n7zWObv057bV2JQMKv9tpUPk2b2r/SwYSyfv8K/v3hMIFNnS6H/R7/G+a/+16dOIpqZdO3gHRNf75IeCXyP0qbxN9aStg/S5sEXWJvRa9Vp3Mm/uqjvrIhW7I5tGzLv9EdSqdWO/Nr+1p2h9oxv7Yf2q9WO/Nr+1p2h9oxv7Yf2q9Wu1Z+a42/hp3NJoDzi39OeP8xcf6ntL1Nm67mVfJEUAq/2qit+qivPA1NBNv1f349ErqZSumvPJ7J7Xuzpb/y+H3DmV6U/srjmdy+N1v6K4/fN5zpxdL+ZprG1WY3mQDOL/4PE8z8it+E/88fIdtVfJkI7IrfhN9EXN3U91wikK+ybN3/h89ZJZnax+fXH/9dXLbCv/Y8I9jbXALoDnJ9YautFH67vSMhVykTwTnhV9tXaVNflTwRmJ/TmQ//Wv1W/Z9IdK/PB1LXvOqz33f+Gt/q22e/7zz+ryMwN9/rRrd8700lgMuLLwH+adrsit+E/7NUp6v8v3g8VyaC/Ipf59RfbfPbRHkikA/5KsvW/X/gcXmdPrQb+2qo3aHt8D+OwFCuQ9uN896ffMfaW0P7zSSA4UFVCr+WWeKsJ3oe0lYmglR1vM1jwq82amsify4RqE9X2br/E5fh69XF8Wn9WHtj2z/19vxorL2x7Z97fFoz1t7Y9k+9PT8aa29s++cen9bUtvfUetyjTSSAYYt/Tnjt9o6u2nX+x2krE0Ep/GqjturzNm2yodKXCLbu/0Qp/3fYuuU9zr+eamdqv3IUU+1M7Yf/pwRqcXxqdR1Hq08Awxf/R2lFJdIqJvz57R3Vv0pbmQgeUp2Sggm/2lgpvy9QvXzIV1m27r/kcToevn70P0cAfueoUGcEVp0AxgW/RP+c8Ou+vp7QUTKwkieCc8KvtupTfl/wNtWZH7Nle6tXmzzxbMW/cXi+H7eOH/pP7ffBwunVVDtT++H/KYGpHKf2e+p93UerTQDjF1+3ckrhtds7+ikGXaHbFb0FhRKBNivWX23Vp/y+wPrLblm27r/k8fR47HqObf/U2/OjsfbGtn/u8WnNWHtj2z/19vxorL2x7Z97fFoz1t7Y9k+9bedolQngusXPn+R5SJEga7qfr33XH3Tlwm9/OWx9ZKNMBKmqs2zdfyeY3kcoradWao4y1O7QdmPHONTu0Hb4H0tgfe1XlwCmB/854bVn8vVEj87rWB7yRKCrel3xm/B39XlIbS4lgq37T3gGlL717Ts/wMXFJn32+85fND7gZJ/9vvMDXFxs0me/7/xF4wNO9tnvOz/AxaaarCoBXLf4+nL2IW2yYiJe3qrRcZkISuHv6yMf9mVzevm+bN3/exC9L7rWuau+1+DIBl1+uupHmu9t3uWnq77X4MgGXX666kea723e5aervtfghhusJgFcv/j6MrcU/l+nuldpe/G417FKngim9JGvsmzdf8nj8nG53uXx5d7Xny39lcfXe7hsofRXHl/uff3Z0l95fL2HyxZKf+Xx5d6cNQKrSAB1Fl+3cuzq3YT/s1RnV+va61gJIU8EU/rIV1m27r/k0X9s6277/h51W5hf29e13m/N/Nq+v0fdFubX9nWt91szv7bv70GLkkD4BFB38c8Jvx7P1FW+9iplIpjS52Tp+b9TbE3p89zzqWaKrSl9uvyPr6+7/vgfS2Dr/Mfy8tY+dAKoG3x6bDO/4pfgv02bnvDRVb72Oi4TwZQ+8lWWrfsveXAMAQjMTSBsAqgr/sJsopwLf3mrRsdlIlDfsX3Ml/pasbqxttR/bB/zZb61t7qxttR3bB/zpb4UCECgFYGQCaC++Au/ntt/lzYJvAm/PZr5ItXZF7/p5fs/CFP7KX3kqyxb91/y4BgCEJibQLgEMI/4l5hN+PXc/sPjSe11nCeCx1PH3ZQ+ef/89RRbU/rkPvPXU2xN6ZP75DUEILA0gVAJYH7xL0XMfuRNV/n6IlgjKBNB2Udt1FZ9fpy28tdD1b6rlLa25r+LC/UQgMAcBMIkgPnF/1Xia1f8Jrz2hIvQ25V/mQisjwm/ibj6yKZslIlA9WXZuv+SB8cQgMDcBL41t4Ma9ucXfxvlOeHXOX1pKSFXKRPBOeFX2/yLzjIRHA2d+Wfr/s8goQoCEJiNgPsEsJz468vf/IpfzO0L4R+m15+lzYRc5ywR5Ff81l9t1ceeGlJ7Fesvu2VRnfW3c6qTjS34tzmzhwAEliLgOgEsJ/4lbhPeH6UT9ls/avO3afssbSbkqlMx4dY5tVHR6PMfjZPNoWXr/odyoh0EIHANAbcJoI34nxNe3fPXVf7btOl5d5U8ESgZ5MJvz8Srj/qOSQRb959wUSAAgcUIuEwAbcRft1nyK34Tft3qUbHbOWUisCt+E34TcfWx20RlIpCvsmzdf8mDYwhAYG4CL+d2MNZ+G/HXKPWb/yoSchP9Y0XxjyUCtcvFX/VdxRKBPhWoj/nK21vdVv3nLHgNAQgsQcBVAmgn/kItATYRHoLeEsGQttZGiaAruWzdvzFiDwEILEXAzS2gtuK/FG78QAACEPBD4MV+v3/Xcjiv7+93b+7uWg4B3w0JHA4/aeh9t9vv/6qpf5y3JSD9aV1a6p+LW0D7w+H4rEyLhUgJcHdI/luVrfvf7domAK0767/d+E9XAM3W/yHF3s3NTSvpOfp1cwtIMChbJqC/nC6fjnqV6rTlRW3yv7LW32CoTl+wW9Fr1emclXP27Rx7CCxLwIveuUkAwu8FyrKhgLcTAQm0Nj1Ga0XHemoqF3cTchN3/bGd6vJEoWPrm14ei9Xl9u0cewgsR8CTzrlKAFoCT3CWCwk8Pf0jO+OhR2JVcnG3OnsEV09V3aZNkWOJIm9jiSKvS00pEGhAwJu+uUsAWhNvkBrEyQZdmpDrit6u0iX8+oG8PnHP2wudHtEtBf+cfbWlQGAZAh51zWUC0HJ4hLVMmGzZiwm5Xd2LhQm5fQq4JO5DE0Vuf8u8mftSBLzqmdsEoIXxCm2poNmen3NX6XwK2F4crGvGnnXMdQJQGHiGt64w9TIbPgV4WQnGcT0B7/rlPgFoCbxDvD5MsPCBQP4pQE/uqOhTgEoeCfazHfntHGtndbpdVLY7Z/9onH8gUJVAHq1VDVc0FiIBaL4RYFZclw2b0lM7ttq3jxzs6R47VrUlB/uOQHX26SFvZ30tEZyzr74UCNQjYBFcz+I8lsIkAE0/CtR5lmorVu3qXcKuK3gVu7I3gZeI5+3URkKvCNFTQ3l7PVWkhKArf5W8n9k/neFfCNQgEEmnQiUALU4kuDWCaVs2Lgl7n4ib6Oe "text/plain": [ "<PIL.Image.Image image mode=RGBA size=384x384>" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "Using cpu device\n", "Wrapping the env with a `Monitor` wrapper\n", "Wrapping the env in a DummyVecEnv.\n", "Wrapping the env in a VecTransposeImage.\n", "-----------------------------------\n", "| info/ | |\n", "| no_shield_action | 0 |\n", "| sum_opened_door | 0 |\n", "| sum_picked_up | 0 |\n", "| sum_ran_into_lava | 0 |\n", "| sum_reached_goal | 2 |\n", "| rollout/ | |\n", "| ep_len_mean | 186 |\n", "| ep_rew_mean | 0.2 |\n", "| time/ | |\n", "| fps | 194 |\n", "| iterations | 1 |\n", "| time_elapsed | 10 |\n", "| total_timesteps | 2048 |\n", "-----------------------------------\n" ] } ], "source": [ "GRID_TO_PRISM_BINARY=os.getenv(\"M2P_BINARY\")\n", "import gymnasium as gym\n", "\n", "\n", "def mask_fn(env: gym.Env):\n", " return env.create_action_mask()\n", "\n", "def nomask_fn(env: gym.Env):\n", " return [1.0] * 7\n", "\n", "def main():\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", " value_for_training = 1.0\n", " shield_comparison = \"absolute\"\n", " shielding = ShieldingConfig.Training\n", " \n", " logger = Logger(\"/tmp\", output_formats=[HumanOutputFormat(sys.stdout)])\n", " \n", "\n", " env = gym.make(env, render_mode=\"rgb_array\")\n", " image_env = RGBImgObsWrapper(env, TILE_PIXELS)\n", " env = RGBImgObsWrapper(env, 8)\n", " env = ImgObsWrapper(env)\n", " env = MiniWrapper(env)\n", "\n", " \n", " env.reset()\n", " Image.fromarray(env.render()).show()\n", " \n", " shield_handlers = dict()\n", " if shield_needed(shielding):\n", " for value in [0.9, 0.99, 0.999, 0.9999, 1.0]:\n", " shield_handler = MiniGridShieldHandler(GRID_TO_PRISM_BINARY, \"grid.txt\", \"grid.prism\", formula, shield_value=value, shield_comparison=shield_comparison, nocleanup=True, prism_file=None)\n", " env = MiniGridSbShieldingWrapper(env, shield_handler=shield_handler, create_shield_at_reset=False)\n", " create_shield_overlay_image(image_env, shield_handler.create_shield())\n", " print(f\"The shield for shield_value = {value}\")\n", "\n", " shield_handlers[value] = shield_handler\n", "\n", "\n", " if shielding == ShieldingConfig.Training:\n", " env = MiniGridSbShieldingWrapper(env, shield_handler=shield_handler, create_shield_at_reset=False)\n", " env = ActionMasker(env, mask_fn)\n", " print(\"Training with shield:\")\n", " create_shield_overlay_image(image_env, shield_handlers[value_for_training].create_shield())\n", " elif shielding == ShieldingConfig.Disabled:\n", " env = ActionMasker(env, nomask_fn)\n", " else:\n", " assert(False) \n", " model = MaskablePPO(\"CnnPolicy\", env, verbose=1, device=\"auto\")\n", " model.set_logger(logger)\n", " steps = 20_000\n", "\n", " \n", " model.learn(steps,callback=[InfoCallback()])\n", "\n", "\n", "\n", "if __name__ == '__main__':\n", " print(\"Starting the training\")\n", " main()" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [] } ], "metadata": { "kernelspec": { "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" }, "language_info": { "codemirror_mode": { "name": "ipython", "version": 3 }, "file_extension": ".py", "mimetype": "text/x-python", "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", "version": "3.10.12" } }, "nbformat": 4, "nbformat_minor": 4}
|
