This file explains the artifact for our paper "STLmc: Robust STL Model Checking of Hybrid Systems using SMT". The STLmc tool is available on our tool webpage: https://stlmc.github.io/ ====================================================== 1. Artifact Overview ====================================================== In this section, we explain the overview of our STLmc tool artifact. The artifact includes the following things: (1) a short demo of the STLmc tool, (2) a script to run the experiments in the paper, and (3) additional examples providing more detailed usages not included in the paper. Part (1) explains how to execute the input model and visualize counterexamples in Section 3 of the paper. Part (2) shows how to reproduce the experimental results in Table 2 in Section 5 of the paper. Part (3) describes an additional demo and additional benchmark models not included in the paper for the 'reusable' badge. The STLmc artifact includes the following files and directories: - AUTHORS.md : authors information, - LICENSE.md : the STLmc tool license, - Makefile : a makefile for generating Antlr4 parser and setting permissions for executables, - benchmarks : benchmark models for our paper and additional experiments, - scripts: experiment reproduction scripts, - stlmc : the source codes and executables of STLmc, - logs : the experimental results and raw log files of the experiments that run on provided VM. The rest of 'README' is organized as follows. Section 2 provides how to set up the artifact using a virtual box image. Section 3 explains rudimentary testing. Section 4 describes a short demo of the STLmc tool in Section 3 of the paper. Section 5 explains how to reproduce the experiments in Section 5 of the paper. Section 6 explains the structure of the log files for the experiments. Section 7 explains the most relevant parts of the source code. Section 8 explains the structure of the benchmark model directories. Section 9 provides additional examples of various options not used in the paper. Section 10 explains how to run additional experiments and more details on our scripts. Section 11 explains supplemental materials. Finally, Section 12 provides guidance on how to run the artifact without VM. For the 'functional' badge, we provide rudimentary testing, scripts to reproduce the results of the paper, log files, and explanations of the interesting parts of the source code. These are explained in Sections 2 through 7. For the 'reusable' badge, we explain more usages of the STLmc tool, additional experiments, and instructions for installing the artifact without a VM image. These are explained in Sections 8 through 12. ====================================================== 2. Running the VirtualBox Image ====================================================== We provide a URL for the VM image 'STLmc.ova' via our tool webpage: https://stlmc.github.io/cav2022-artifact This VM image contains our tool and experiments (with Ubuntu 18.04.6 installed). The size of the image is about 4GB. A minimum system requirement is a quad-core machine with 4GB memory. You can run the image using VirtualBox (https://www.virtualbox.org) as follows: - Download 'STLmc.ova' from our webpage (https://stlmc.github.io/cav2022-artifact) - Click 'File/Import Appliance' in the top menu. - Choose 'STLmc.ova', and click 'Continue'. - Set the number of CPU cores (>= 4) and the size of memory (>= 4GB). - Click 'Import' (which will take a few minutes). - Click the green right arrow to run the imported image. Remark: Some experiments may not run properly on the following architectures: - Apple MacBook Pro 2015 or earlier: Yices 2.6 with QF-NRA is not working ====================================================== 3. Rudimentary Testing ====================================================== We provide rudimentary testing to check there are no problems running the STLmc tool. The tests check whether the prerequisites, such as Python 3, Yices, dReal, etc., are installed well and run the STLmc tool using simple models. The following command runs the tests: user@VB:~/CAV2022-AeC$ make test If the tests succeed, you will see the following messages: start smoke test ... [exec] Python: pass [exec] Yices: pass [exec] dReal: pass [exec] Z3: pass [exec] Java: pass [exec] Gnuplot: pass [file] Config: pass [smt] dReal ./tests/smt2/dreal/01.smt2: pass ./tests/smt2/dreal/02.smt2: pass [smt] Z3 ./tests/smt2/z3/01.smt2: pass ./tests/smt2/z3/02.smt2: pass [smt] Yices ./tests/smt2/yices2/01.smt2: pass ./tests/smt2/yices2/02.smt2: pass [tool] STLmc ./tests/stlmc/01.model: pass ./tests/stlmc/02.model: pass ====================================================== 4. Short Demo of the STLmc Tool ====================================================== In this section, we shortly demonstrate the usage of the STLmc tool on our VM (i.e., STLmc.ova) using the two networked thermostat controller model, explained in Sec. 3 of our paper. To start the STLmc tool, go to the 'stlmc/src' directory of the artifact: user@VB:~$ cd '/home/user/CAV2022-AeC/stlmc/src' We can use the script 'stlmc' in the 'stlmc/src' directory to start the STLmc tool. The following command finds a counterexample of the formula 'f2' of the thermostat model at bound 2 with respect to robustness threshold 2 using parallelized 2-step algorithm and dReal: user@VB:~/CAV2022-AeC/stlmc/src$./stlmc ../../benchmarks/paper/thm-ode/therm.model -bound 5 -time-bound 25 -threshold 2 -goal f2 -solver dreal -two-step -parallel -visualize The analysis in VM took 91 seconds on AMD Ryzen 9 3.3GHz with quad-core and 4GB of memory. When the '-visualize' option is set and there is a counterexample, the STLmc tool creates a counterexample file and a visualization configuration file to draw graphs for the counterexample. The configuration file contains information about variables to draw, the storage format of the graph, and grouping information to draw into one graph. The above command generates a counterexample file, named 'therm_b5_f2_dreal.counterexample', and a visualization configuration file, named 'therm_b5_f2_dreal.cfg', in the current directory. The contents of 'therm_b5_f2_dreal.cfg' are as follows: { # state variables: x0 , x1 # f2_0 ---> ([][2.0,4.0] (((x0 - x1) >= 4) -> (<>[3.0,10.0] ((x0 - x1) <= -3)))) # f2_1 ---> (((x0 - x1) >= 4) -> (<>[3.0,10.0] ((x0 - x1) <= -3))) # f2_2 ---> (not ((x0 - x1) >= 4)) # f2_3 ---> (<>[3.0,10.0] ((x0 - x1) <= -3)) # f2_4 ---> ((x0 - x1) >= 4) # f2_5 ---> ((x0 - x1) <= -3) output = html # pdf group { } } The STLmc tool provides the script 'stlmc-vis' to draw counterexample signals and robustness degrees. For example, the counterexample graphs for the property 'f2' of the thermostat can be generated using the following command: user@VB:~/CAV2022-AeC/stlmc/src$./stlmc-vis therm_b5_f2_dreal.counterexample The default visualization configuration creates two graphs: (1) a graph for continuous state variables and (2) a graph for robustness degrees of STL subformulas. The grouping information to draw into one graph can be changed by modifying the visualization configuration file. Variables in the same group are displayed on the same graph. For example, we can generate four graphs corresponding to Figure 3 of our paper by modifying the group attributes in 'therm_b5_f2_dreal.cfg' as follows: { # state variables: x0 , x1 # f2_1 ---> (((x0 - x1) >= 4) -> (<>[3.0,10.0] ((x0 - x1) <= -3))) # f2_0 ---> ([][2.0,4.0] (((x0 - x1) >= 4) -> (<>[3.0,10.0] ((x0 - x1) <= -3)))) # f2_4 ---> ((x0 - x1) >= 4) # f2_2 ---> (not ((x0 - x1) >= 4)) # f2_3 ---> (<>[3.0,10.0] ((x0 - x1) <= -3)) # f2_5 ---> ((x0 - x1) <= -3) output = html # pdf group { (x0, x1), (f2_0, f2_1), (f2_2, f2_3), (f2_4, f2_5) } } These four graphs can be viewed in 'therm_b5_f2_dreal.counterexample.html' created by rerunning the following command: user@VB:~/CAV2022-AeC/stlmc/src$./stlmc-vis therm_b5_f2_dreal.counterexample ====================================================== 5. Running the Experiments ====================================================== In this section, we explain how to reproduce the experiment of the paper in Section 5 In Section 5 of our paper, we evaluate the effectiveness of the STLmc tool using a number of hybrid system benchmarks and nontrivial STL properties. We consider a total of 30 cases as indicated in Table 2 of our paper, taking into account ten benchmark models and three STL formulas for each model. We provide the script 'run_exp' in the 'scripts' subdirectory to automate the experiments. The models of the experiments are located in the 'benchmarks/paper' subdirectory. The following command run all these models (10 models, 3 formulas): user@VB:~/CAV2022-AeC/scripts$ ./run-exp ../benchmarks/paper/ -t 3600 The command-line argument '-t 3600' denotes a 3600-second timeout. This command creates a 'log' subdirectory in the current directory. The log files for each case are in the 'log' subdirectory. We provide the script 'gen-table' to generate a table summarizing results in the format of Table 2 in our paper. The script 'gen-table' uses the log files located in the 'log' subdirectory to generate the table. For example, the following command generates the file 'log-table.html' corresponding to Table 2 of the paper in the same directory: user@VB:~/CAV2022-AeC/scripts$ ./gen-table ====================================================== 6. Log Files for the Experiments ====================================================== The subdirectory 'logs' of the top artifact directory 'CAV2022-AeC' contains the log files, CSV reports, and html tables for the experiments. There are two subdirectories in the 'logs': (1) non-vm, and (2) vm. In the 'logs/non-vm' subdirectory, there are experimental results that were run in the same environment as the paper (Intel Xeon 2.8GHz with 256GB memory). In the 'logs/vm' subdirectory, there are experimental results that were run in VM on AMD Ryzen 9 3.3GHz with quad-core and 4GB of memory. The results of the experiment of the paper are placed in the 'paper' subdirectory and the results of the additional experiment are placed in the 'additional' subdirectory. These results are placed in the following directory, where is one of {'non-vm', 'vm'}: - logs//paper/raw.zip: a zip file of the log files of the experimenst of the paper in Section 5 - logs//paper/raw-report.csv: a CSV report of the log files - logs//paper/raw-table.html: an html table corresponding to Table 2 of our paper - logs//additional/raw.zip: a zip file of the log files of the extended experiments of the technical report in Section 5 - logs//additional/raw-report.csv: a CSV report of raw.zip - logs//additional/raw-table.html: the html table corresponding to Table 2 and Table 3 of the technical report ====================================================== 7. Interesting Parts of STLmc Source Code ====================================================== The full source code of our tool is located in the 'stlmc/src' subdirectory of the top directory 'CAV2022-AeC'. Our tool is implemented in around 9,500 lines of Python code. Some interesting parts of the source codes are as follows: - stlmc/src/stlmcPy/encoding/ This directory contains the implementation of direct (i.e., 1-step) and 2-step solving algorithms, explained in Sec. 4.2 and 4.3 of the paper, respectively. The 1-step solving algorithm is implemented in 'monolithc.py' and 2-step solving algorithm is implemented in 'enumerate.py', where each file contains the implementation of the epsilon strengthening and encoding of Boolean STL model checking. - stlmc/src/stlmcPy/objects/algorithm.py: This directory contains the implementation of SMT parallelization algorithm. The STLmc tool uses the implementation of the solving algorithms in 'src/stlmcPy/encoding' and the implementation of the parallelization of this directory together to perform the 2-step parallel algorithm, explained in Sec. 4.3. - stlmc/src/stlmcPy/solver: This directory contains the implementation of the STLmc SMT solving interface, described as 'SMT solving interface' in Fig. 4 of our paper. We connect three SMT solvers (i.e., Z3, Yices2, and dReal) using the interface. Each connection is implemented in a file .py under this directory, where is one of {'z3', 'yices', 'dreal'}. ====================================================== 8. The Structure of the Benchmark Model Directories ====================================================== In this section, we explain the structure of the benchmarks model directories of our artifact. We provide benchmark models and their configurations in the subdirectory 'benchmarks/', placed at the top directory 'CAV2022-AeC'. There are two subdirectories in the 'benchmarks': one for the benchmarks of the paper (i.e., 'benchmarks/paper') and the other for the additional benchmarks (i.e., 'benchmarks/additional). Each model is placed in the directory of the same name, with four configuration files. For the benchmarks of our paper, the benchmark models and corresponding configuration files are placed in the directory, named '-' where it is one of {car-liner, wat-linear, bat-linear, thm-poly, car-poly, rail-poly, thm-ode, space-ode, oscil-ode, nav-ode} and