Artifact

This page explains the SCP2024 artifact for our paper: “SMT-Based Robust Model Checking for Signal Temporal Logic” by J. Lee, G. Yu, and K. Bae.

The artifact includes the followings:

Remark: Our artifact can only be run on Ubuntu because underlying reachability solvers (e.g., SpaceEx, Flow*) do not provide MacOS executables.

To install our artifact, follow the below instruction steps:

Follow the instructions in https://stlmc.github.io/download/ to install prerequisites for STLmc.
Install the STLmc tool using the following command:
```
user@ubuntu:~$ pip install stlmc==1.0.0.dev3
```
Download and unzip the artifact archive file (artifact.zip).

Running the Experiments

Our artifact contains the scripts to reproduce the experiments of our paper. You can run the experiments of the paper as follows:

To run the first experiment of the paper. Go to the ‘scripts/exp1’ directory and use the following command:
```
user@ubuntu:~/artifact/scripts/exp1$ ./run-exp ../../benchmarks/exp1 -t 3600
```
This command reproduces the first experiment with a time out 3600s using the benchmarks in the directory ‘../../benchmarks/exp1’.
To run the second experiment of the paper. Go to the ‘scripts/exp2’ directory and use the following command:
```
user@ubuntu:~/artifact/scripts/exp2$ ./run-exp ../../benchmarks/exp2 -t 3600
```
This command reproduces the experiment using models in ‘../../benchmarks/exp2’.

Remark: Each reproduction script creates a ‘log’ directory and put log files in it.

Generating Reports

You can create a spreadsheet report for each experiment from the log files using the ‘gen-report’ script in each experiment directory.

For example, you can generate a report file for the first experiment as follows:

user@ubuntu:~/artifact/scripts/exp1$ ./gen-report # generates a report 'exp1-report.csv'

Note: Each script generates a report file using the log files in the ‘log’ directory.

Generating HTML Tables

You can also create an html table from a report file using the ‘gen-table’ script.

For example, the following command generates an html table ‘exp1-table.html’ using the ‘exp1-report.csv’.

user@ubuntu:~/artifact/scripts/exp1$ ./gen-table # generates a table 'exp1-table.html'

You can find log files for our paper, including spreadsheet reports and html tables from logs.zip.

We also provide online links to our tables: exp1-table and exp2-table.