VMCAI 2025 - Submission Artifact for paper "Reasoning about Rare-Event Reachability in Vector Addition Systems via Affine Vector Spaces"

This is a tar.gz compressed Docker image which contains the tools associated with our VMCAI 2025 submission: Reasoning about Rare-Event Reachability inVector Addition Systems via Affine Vector Spaces. The purpose of this upload is to provide a docker image which supports the results presented in our paper so that reviewers may replicate the results. Please load the docker image using docker load --input, and then docker run -it ifndefjosh/vmcai2025:latest. The tool presented in the paper is called Wayfarer, and lives in /opt/wayfarer. To produce the results, simply run /opt/wayfarer/all_test.sh. These will put the results in the results/ directory. The file 8react.csv corresponds to the MYP model, Table 1, and the remaining results correspond to Table 2. The results in Table 2 refer to the lowest K or Qty needed to get the highest Pmin found during the tests. Note: Running all_test.sh will produce many many lines of output. If you don't wish to see this output, you may pipe it to /dev/null, i.e., /opt/wayfarer/all_test.sh >> /dev/null. This will not affect the production of results files. It is recommended to create mountpoints for /opt/wayfarer/results and /opt/ragtimer/results to folders on the host machine, though this is not strictly necessary. If you wish not to, you will simply have to observe the results from within the container. We also provide a means to test against RAGTIMER, the primary tool we compare against in the paper. RAGTIMER lives in /opt/ragtimer. It may be run via the /opt/ragtimer/benchmark.py script, which will put results in /opt/ragtimer/results. Note: "SOP" refers to "Single Distance Priority" in the paper. "SOP/Single Order Priority" was an older version of the name we ditched to avoid confusion or conflation with other methods using the word "order". Interpreting the Results The 2react, 6react, and 12react models refer to the SSPD, EFC and SMR models in Table 2 of the paper. For these models on both Ragtimer and Wayfarer, choose the lowest K/Qty/runtime corresponding to when the tool gets the highest Pmin. All results are placed in filenames according to the models that they are for. The results files ending in *_piped.csv correspond to the Space Scaling method mentioned in Appendix A.1. All results are stored in CSV format. Terminal-based tools can be used to easily view CSV files, notably sc-im (spreadsheet editor with vim-like keybindings). We do not include this tool in the image due to licensing reasons, but reviewers may install it within the image after they have obtained it. For reviewers which do not wish to install this tool, and only wish to view the results using existing terminal-based tools, you may chain the following commands to get the CSV file into a pager: cat <results_file>.csv | sed s/,/"\\t"/g | less (to use the "less" pager) cat <results_file>.csv | sed s/,/"\\t"/g | more (to use the "more" pager) The above commands are not strictly necessary, but replace commas with tab characters for readability. Architecture This image was built on x86_64, and the ARM image was cross-compiled. With any luck the ARM version should work equally well, but may run into performance issues. Licensing Wayfarer (our tool) is licensed under the GPLv3+. This license is also the license which Storm/Stormpy uses, which are included in this container as Wayfarer utilizes Storm for its probabilistic model checking functionality. Ragtimer (the tool we are comparing against) is licensed under the MIT license.