Artifact for the TACAS 2026 paper "Deconstructing Subset Construction: Reducing While Determinizing"

This artifact contains the supplementary material for the TACAS26 submission "Deconstructing Subset Construction: Reducing While Determinizing". Contents of this archive The archive contains the following parts. LICENSE.txt contains the license of this artifact. To get a list of the installed software in the Docker container and their respective licenses, simply run docker run --rm otf-tacas26-benchmark:latest apk list after importing the container (see below). otf-tacas26-benchmark.tar.gz is a pre-built Docker image which contains the necessary binaries for executing our benchmarks. README.md contains this text. results contains our recorded benchmark results that we have used in the paper. source contains the source code of our benchmarks in form of Gradle projects, including a Dockerfile for building the previous Docker image and a Python script for plotting the results. systems contains the systems that we benchmarked in the paper. How to run the benchmark (in the following, we use $ARTIFACT to denote the absolute path to the extracted version of this archive) We highly suggest to import the provided Docker image via docker load --input $ARTIFACT/otf-tacas26-benchmark.tar.gz Alternatively, you can build the Docker image yourself via docker build -t otf-tacas26-benchmark $ARTIFACT/source The docker image is configured to use two volumes (one for reading the input systems and one for writing the output results) and can be parameterized with three environment variables (one for the number of parallel threads, one for the timeout duration in seconds, and one for the JVM options). Replicating results For running the Walnut benchmark, we called Docker as follows: docker run \ -v $ARTIFACT/results/:/workdir/OTF_benchmark/data \ -v $ARTIFACT/systems/walnut/:/workdir/OTF_benchmark/benchmarks/ \ -e TIMEOUT=3600 \ -e NUM_JOBS=12 \ otf-tacas26-benchmark:latest For running the random modular benchmark, we called Docker as follows: docker run \ -v $ARTIFACT/results/:/workdir/OTF_benchmark/data \ -v $ARTIFACT/systems/randomModular/:/workdir/OTF_benchmark/benchmarks/ \ -e TIMEOUT=1000 \ -e NUM_JOBS=20 \ otf-tacas26-benchmark:latest The results of the benchmarks are written to a timestamped folder in the provided result directory (typically $ARTIFACT/results). Hardware requirements / Smoke testing Note that the benchmark execution may require a significant amount of system resources. On a server with two AMD EPYC 7763 CPUs and 2TB of RAM the Walnut benchmark took thirteen hours whereas the random modular benchmark took eight hours. To account for local hardware limitations or smoke-testing the benchmark, you may reduce the number of parallel jobs, decrease the timeout, or select a smaller set of systems. For example, docker run \ -v $ARTIFACT/results/:/workdir/OTF_benchmark/data \ -v $ARTIFACT/systems/walnut/:/workdir/OTF_benchmark/benchmarks/ \ -e TIMEOUT=10 \ -e NUM_JOBS=4 \ -e JAVA_OPTS="-Xmx8G -XX:ParallelGCThreads=2" \ otf-tacas26-benchmark:latest should create some exemplary data within ~15 minutes. You may further consult Docker's options on resource constraints to adjust to your local hardware conditions. Displaying the results After the benchmarks have finished, the output folder contains the respective benchmark data as .csv files and an error log (err.log) for reporting any issues that occurred during execution. For visualizing the results, you can use the provided plot.py script as follows python $ARTIFACT/source/plot.py $ARTIFACT/results/ The script produces a plot.pdf file in your current directory, which contains the cactus plots for the respective data. Note that the script requires you to have the Python packages pandas and matplotlib installed.