Implementation

We provide the software via a docker image and recommend using this container. TEMPEST builds on top of Storm, which itself has many dependencies on. Therefore using the docker image makes the installation easier.

In case you want to build TEMPEST from source, the code is available as a github repository, which features this description as README as well.

Using TEMPEST via a Docker Image

Install Docker

Please install docker on your system, following these installation instructions:

Note: We have not tested TEMPEST on Windows or MacOS machines when using docker. We continue with the description on how to use TEMPEST assuming a Linux environment.

To use docker first start the service as following:

sudo systemctl start docker
# Verify with
sudo docker info
# and add yourself to the docker usergroup
# if you don't want to do this you need to prepend sudo to all docker commands
sudo usermod -aG docker $USER

We provide a docker image which comes with a pre-built version of TEMPEST. The image can be downloaded as follows:

docker pull tempestshields/tempest:atva21_final
docker images
# REPOSITORY                  TAG                 IMAGE ID            CREATED             SIZE
# tempestshields/tempest      atva21_final              d19ed0c41b52        14 hours ago        2.06GB

Performing Experiments

Use the following command to start the docker container with the run script:

docker run -it -v "$(pwd)":/data tempestshields/tempest:atva21_final /bin/bash /tempest-shields/run.sh

To redo the experiments from the paper choose one of the examples from the list:

Select one of the following examples [enter <option> and <value>]:
        1 <w>            Warehouse Optimal Controller
        2 <w>            Warehouse Safety Shield
        3 <lengthA>      Warehouse Optimal Shield
        4 <lmax>         Optimal Shield for Traffic Control
        e|xit            Exit this script.

For example to synthesize a safety shield for the warehouse example issue the following:

2 16

will run Warehouse Safety with a grid width of 16.

Adding New Examples

You can also perform your own experiments by mounting a directory containing your examples into the container.

In order to be correctly parsed into tempest please adhere to the following directory structure:

my_examples
├── another_example
│   ├── model.prism
│   └── properties.prop
└── my_example
    ├── model.prism
    └── properties.prop

Each example has its own directory containing two files model.prism and properties.prop containing the model description and properties respectively.

From the directory containing the directory my_examples run the following command:

docker run -it -v "$(pwd)"/my_examples:/tempest-shields/examples/my_examples tempestshields/tempest:atva21_final /bin/bash

Your examples will then be mounted in the same directory as the provided examples:

29e5007af431# ls /tempest-shields/examples
my_examples  optimal_traffic_light_shielding  warehouse

Note that the copied and created files within the container are not persistent, apart from those that are copied into the my_examples directory.

Running the examples can be done using the provided runtempest script which provides an easy interface to the command line interface:

cd /tempest-shields/
runtempest -i -e -c "<undefined_constant>=,..." examples/my_examples/<example_to_run>

The optional flags -i and -e enable full state and action descriptions in the created shield files and. Not using these flags results in smaller shield files.

If your model features undefined constants (e.g. the width of the grid in warehouse examples) you have to define them using
-c "<constant_name>=), multiple constants need to be defined likewise, seperated by commas (,).

In order to examine the created shields on your system, copy the created shield file to the mounted directory.

In the docker container execute the following commands:

cd /tempest-shields
cp <shieldFilename>.shield /tempest-shields/examples/my_examples
exit

The file <shieldFilename>.shield will be contained in ./my_examples on your local filesystem.

Building TEMPEST from Source

If you do not want to install docker on your machine you can also build TEMPEST from source. The installation process follows the same procedure as the installation process of Storm:

Install the recommended dependencies as detailed on stormchecker.org, they will contain all needed dependencies.

Download the source:

git clone https://github.com/tempest-shields/tempest-shields
cd tempest-shields

The installation process then follow the same as described on the storm website:

mkdir build
cd build
cmake ..
# building the command line interface for tempest suffices:
make storm-main
# if you have at least 8GB of RAM and multiple cores available you can speed up the build step via
make storm-main -j${NUMBER_OF_CORES_TO_BE_USED}

The binary will then be contained in <cloned_directory>/build/bin/ called storm. In order to run TEMPEST as discussed above please change the path in runtempest appropriately and append a '\' at the end of the line.