Here we explain how to reproduce the results of the QEST 2020 submission Compact and explainable strategy representations using dtControl. More concretely, we show how to
In the end, you will obtain Figure 1 and all the numbers reported in Table 1.
Here is a demonstration video from which you may copy-paste the commands.
More detailed instructions follow.
Recent advances have shown how decision trees are apt data structures for concisely representing strategies arising out of both model checking as well as controller synthesis for cyber-physical systems. Moreover, they make the strategy explainable and help boost understanding and trust. This tool demonstration paper presents dtControl – a tool that can represent strategies arising from strategy synthesis using tools like PRISM, Storm, UPPAAL STRATEGO, and SCOTS. We demonstrate the ease-of-use both when employing dtControl as a black box as well as when controlling all hyper-parameters. We compare the decision tree representation to BDDs and also demonstrate the possibility of obtaining even smaller decision trees using the specialized algorithms available in the tool.
To run dtControl, you need an up-to-date version of Python 3 (>=3.6.8) and the Python package installer pip. Additionally, for downloading the case studies, we also require that you have Git installed. Remaining dependencies of dtControl will be automatically installed by pip. All of these are installed together with our tool, since it is distributed using the pip package management system.
The experiments reported in the paper have been conducted on an Ubuntu Linux machine with 192GB of RAM and a Intel Xeon CPU E5-2630 v4 @ 2.20GHz. The full set of experiments require 6GB of RAM and takes about 1-2 hours to complete, however we also provide a reduced set of experiments which require only 1GB of RAM and finishes in less than 15 minutes. The commands in this tutorial assume you are using command line, but an advanced user should be able to transfer the commands given here and make it work on Windows.
You will clone a git repository to obtain the case studies. If you do not have it, install git by following their advice on their official downloads website.
Make sure you have Python 3.6.8 (or newer),
python3-venv for creating virtual environments.
On Ubuntu 16.10 or newer:
$ sudo apt-get install python3 python3-pip python3-venv
On MacOS, you can install with the help of the package manager Homebrew.
$ brew install python3
or refer to this tutorial if you don’t have Homebrew installed.
We use a virtual environment to make sure that the installation is clean and easy, and does not interfere with the python packages installed in your system.
For the purpose of this artifact evaluation, let us create a folder
dtcontrol in your home directory and place our virtual environment in the folder
~/dtcontrol/venv. This can be accomplished by running:
$ python3 -m venv ~/dtcontrol/venv
After evaluating our artifact, you can delete this folder and thereby all traces of the python packages you installed for reproducing our results.
To activate the virtual environment, run
$ source ~/dtcontrol/venv/bin/activate
After activating the virtual environment, execute
$ pip3 install dtcontrol
You can check if dtControl was sucessfully installed by running
dtcontrol --help. This should display the help message.
On some machines, one may see
error: invalid command 'bdist_wheel' during the installation, but dtControl still installs successfully.
To obtain all case studies, first go to the dtcontrol directory
$ cd ~/dtcontrol
and then download the examples by executing
$ git clone https://gitlab.lrz.de/i7/dtcontrol-examples.git
Most of the input files are zipped. You can unpack them by executing
$ cd dtcontrol-examples && ./unzip_qest.sh
Since we want to execute several algorithms of dtControl on multiple case studies, it is quicker to use the built-in benchmarking functionality.
Download the file qest20-artifact.py into the
~/dtcontrol directory by running
$ cd ~/dtcontrol $ wget https://dtcontrol.model.in.tum.de/files/qest20-artifact.py
We estimate that running the full set of experiments will take 1-2 hours depending on your machine specifications and will use around 6GB of RAM. We also provide a script containing a smaller subset of experiments, which takes only 15 mins and requires only 1GB of RAM. You can download qest20-artifact-subset.py by running
$ cd ~/dtcontrol $ wget https://dtcontrol.model.in.tum.de/files/qest20-artifact-subset.py
In case you don’t have
wget on your machine, you can also manually perform the download or install
wget by running
sudo apt install wget (on Ubuntu).
However, this file must be placed inside the
~/dtcontrol folder as it uses relative paths to access the case studies.
Next, to start the full set of experiments, execute (assuming you have activated the virtual environment where dtControl is installed)
$ python qest20-artifact.py
or to run the subset
$ python qest20-artifact-subset.py
Note that you might see many warnings and messages during execution, however, as long as all experiments run, it should be safe to ignore them.
To run dtControl on a single case study, execute the following (assuming you have activated the virtual environment, installed dtControl and unzipped the case studies) from the
$ dtcontrol --input ~/dtcontrol/dtcontrol-examples/<case_study> --use-preset <preset>
<case_study> is the file name of the case study, e.g. cartpole.scs
<preset> is one of the available presets. For the paper, we used the
avg preset for the MDP case studies and
mlentropy preset for the CPS case studies.
Running dtControl creates several files. One of them is
~/dtcontrol/benchmark.html. Open this file in a browser, and you will see a table containing the results of all the case study - algorithm combinations which were executed.
The contents of the table are the following.
#(s,a), the number of state-action pairs, and
#doc, the domain of controller. We report
#docunder the “Lookup table” column of Table 1 in the paper. This is size of the domain when the strategy is seen as a map from states to set of allowed actions (f: S ➔ 2ᴬ).
Extra details for the curious: All the CPS case studies use the Multi-label Entropy approach which exploits the non-determinism in the controller. For the MDP case studies, we use the Attribute-value Grouping approach which works with categorical variables. This approach takes in a
tolerance parameter, which we set to
1e-5 for some case studies, and to
MAX_INT for some other case studies. The choice, as described in the paper, was made purely on an empirical basis.
To reproduce Figure 1, you may open
~/dtcontrol/benchmark.html in a browser and click on the “DOT” link in the DT column for
dtControl also stores the source of this image in Graphviz/DOT format in the file
Figure 2 shows an overview of the modular structure of dtControl. To verify this structure, you can download the source code as zip or view it on gitlab. The source code is in the dtcontrol folder. There you can see:
print_cmethods in the