Beyond Response: A Catalog of Response Pattern Refinements

README file for artifact of submission: "Beyond Response: A Catalog of Response Pattern Refinements" Artifact Contents----------------- The folder contains the following files and directories: 1. ResponsePatternIdentifier - source code for the detection and validation of response pattern instances. The source as-is will not compile standalone, since it depends on the Xtext-based Spectra language project. To run detection and validation, use the pre-built jar files described in items 8 and 9 instead. 2. xmv; promela; tlsf; spectra - one folder per specification language, in the order they are discussed in the paper. Each folder contains a `dataset` subfolder holding the collected specifications, plus three result files: - [Language]_manual.csv - manually detected response pattern instances (specification file + request expression + grant expression). - [Language]_automatic.csv - automatically detected response pattern instances, according to the custom detection algorithm for that language (specification file + request expression + grant expression). - [Language]_results.xlsx - assembled results of the manual and automatic detection, followed by semantic validation. The table of entries is divided into two parts, separated by a single empty row: the first part contains instances classified as non-trivial (either the refinement or its restore-direction counterpart is not `NONE`); the second part contains either trivial classifications (both `NONE`) or instances that could not be classified (empty cells, e.g. due to a timeout or error). Manual detections are shown in bold. Where the original specifications were gathered in separate batches, they are kept in subfolders of `dataset` rather than mixed together; detection commands recurse through the entire `dataset` folder, including these subfolders. Specifics for each language: a. xmv - the `dataset` folder additionally contains an `invalid` subfolder: specifications collected during dataset gathering that could not be parsed/compiled standalone by the toolchain (for example, because they reference other files via `#include` that are not part of the dataset). They are excluded from `XMV_manual.csv`/`XMV_automatic.csv` and from the reported results, but are kept for transparency. Because detection recurses into every subfolder of `dataset`, re-running DETECT over `xmv/dataset` from scratch will also attempt these files and is expected to skip or fail on them. b. promela - the `dataset` folder has no further subfolders. c. tlsf - the `dataset` folder additionally contains a `sweap` subfolder, holding TLSF benchmarks collected from the sweap infinite-state synthesis tool's benchmark suite. d. spectra - the `dataset` folder additionally contains `team-1` .. `team-10` and `syntech23` subfolders, holding specifications collected from separate sources. Every Spectra specification imports a shared pattern library, `DwyerPatterns.spectra`, using a path relative to its own location rather than a fixed search path; consequently `dataset` and each of these subfolders keeps its own local copy of `DwyerPatterns.spectra` alongside the specifications that import it. Do not remove these copies when tidying the dataset - doing so breaks validation for every specification in that folder. 3. temp - working folder used during execution. It must contain a copy of `DwyerPatterns.spectra`, since Spectra pattern validation copies the specification under validation into this folder before parsing it. This is a separate requirement from the `DwyerPatterns.spectra` copies described in item 2d above. 4. Full_Response_Pattern_Refinements_Catalog.pdf - catalog of response pattern refinements, including LTL and CTL formulas, along with Büchi automata graphs. 5. ResponsePatterns.spectra - an auto-generated pattern library containing all combinations of request and restoring phases together with their independent refinements, generated by `pattern_generator.py` (see below). 6. pattern_generator.py - a Python script that uses the Spot API to identify response pattern combinations that are semantically equivalent to one another, then generates `ResponsePatterns.spectra` containing every valid combination, annotating each pattern with a comment listing the combinations it is equivalent to. 7. libcudd.so - CUDD library file required during execution of Spectra pattern validation. 8. single_validator.jar - executes validation and classification of a single instance (file + request + grant). Requires Java 21 or higher. Depending on the specification language: - XMV: requires a Linux environment and NuSMV (https://nusmv.fbk.eu/downloads.html) installed at `~/NuSMV-2.7.0-linux64/`. - Promela: requires Spin (https://spinroot.com) and a C compiler (e.g. gcc) on the PATH, since Spin compiles and runs a verifier for each check. - TLSF: requires `ltlsynt` and `autfilt`, both part of Spot (https://spot.lre.epita.fr), on the PATH. - Spectra: requires `libcudd.so` to be on the library path (see IMPORTANT note below). Usage: java -jar single_validator.jar [XMV|Promela|TLSF|Spectra] [Specification file path] '[Request Expression]' '[Grant Expression]' For example: java -jar single_validator.jar Spectra spectra/dataset/AirportControlTower.spectra 'passengersWaiting_takeoff_secondary' 'busLocation' checks the AirportControlTower specification for the refinement of the response pattern "G (passengersWaiting_takeoff_secondary -> F busLocation)" that appears in the specification. IMPORTANT: to check Spectra files, run "export LD_LIBRARY_PATH=[path to libcudd.so]" beforehand. If executing from the artifact's root directory, simply run "export LD_LIBRARY_PATH=." beforehand. 9. detector_validator.jar - executes detection of patterns in a folder, or validation and classification of instances from a csv file. Requires Java 21 or higher, and `single_validator.jar` (with its own dependencies described in item 8 above) in the same directory. Results are saved to a csv file named "[file or folder name]_[XMV|Promela|TLSF|Spectra]_results.csv". a. Detection mode: Examines all specifications in a folder (recursively) to detect instances of response patterns. Usage: java -jar detector_validator.jar DETECT [XMV|Promela|TLSF|Spectra] [folder] For example: java -jar detector_validator.jar DETECT XMV xmv/dataset detects instances in all specifications under `xmv/dataset` and saves the results to `dataset_XMV_results.csv`, in a three-column file+request+grant format. b. Validation mode: Validates every entry in a csv file (file+request+grant format), calling `single_validator.jar` in a separate process per entry with a 30-minute timeout. Usage: java -jar detector_validator.jar VALIDATE [XMV|Promela|TLSF|Spectra] [csv file] For example: java -jar detector_validator.jar VALIDATE XMV xmv/XMV_manual.csv validates every entry in `XMV_manual.csv` and saves the results to `XMV_manual.csv_XMV_results.csv`, in an extended format that includes the instance classification. 10. pattern_frequency_report.py - a Python script that reports Refinement/Refinement Restore frequency statistics from one or more `[XMV|Promela|TLSF|Spectra]_results.xlsx` files, with a combined summary when given more than one. Usage: python3 pattern_frequency_report.py [Results excel spreadsheet path] [additional paths...] 11. User Study - materials from a two-semester user study in which student developers wrote Spectra specifications for a series of mini-projects, with an accompanying Slack channel per participant for questions and weekly reports. - Spectra mini-project 1 - Patrolling.pdf; Spectra mini-project 2 - Deliveries.pdf; Spectra mini-project 3 - Escaping a Guard.pdf; Spectra mini-project 4 - Catching an Intruder.pdf - the four mini-project assignments given to participants, in order. - Consent.pdf - The consent form presented to students via Moodle at the beginning of each semester. - Analysis.xlsx - analysis of the collected specifications and the accompanying Slack correspondence, per mini-project and per semester (26a = first semester, 26b = second), across three sheets: - `26ab Excerpts` - for each of the four mini-projects, the assignment's requirement text alongside anonymized excerpts of participants' questions from the Slack channels, grouped by semester. - `26a Classification` / `26b Classification` - for each mini-project, the response pattern instance found in every participant's submitted specification, together with its refinement classification and whether the participant reused the built-in pattern library rather than writing the pattern directly. 12. Dockerfile - builds a self-contained image with every dependency listed in item 8 pre-installed (NuSMV 2.7.0, Spin + a C compiler, and Spot with Python bindings and its `ltlsynt`/`autfilt` command-line tools, on top of Java 21), so none of it needs to be installed manually. Build and run it from the artifact's root directory with: docker build -t response-patterns-artifact . docker run -it --rm response-patterns-artifact This drops into a shell at `/artifact` (the container's copy of this folder), with `LD_LIBRARY_PATH` already set as required by item 8. Every command shown above (single_validator.jar, detector_validator.jar, pattern_generator.py) can then be run exactly as documented, with no further setup. All four language pipelines and `pattern_generator.py` have been tested inside this image.