An artifact for Scopelines: A Visualizable Semantic LTL Representation

Artifact of the paper "Scopelines: A Visualizable Semantic LTL Representation" A scopeline is a representation of an LTL property that sits between LTL and first-order logic: like first-order logic, it states every quantifier explicitly (forall, exists, and their strong/weak variants), and like LTL, it needs no index variables. Nested before and after scopes form a chain, which is rendered as stacked bands on a timeline. For example, a U b is the scopeline "exists b strictly before always a". The archive scopelines_artifact.zip contains the folder scopelines_artifact with:- the translation of scopelines into LTL (Algorithm 1) and the search for scopelines equivalent to an LTL formula (Algorithm 2, with the decomposition heuristic of Section V);- the renderer of scopelines as SVG/PNG (Section VI);- the five datasets and the scripts that reproduce every result of the evaluation (Section VII): Table I, the statistics in the text, Figure 7, the decomposition ablation, and the oracle-based validation;- the scripts that render the example figures (Figures 1 and 3-6);- a README with detailed instructions, a Dockerfile, and a ready-made Docker image (scopelines-docker.tar.gz). REQUIREMENTS - Docker (recommended): the image contains Python 3.12, Spot 2.15.1 (built from source), the Python packages, and the code, so nothing else needs installing. It is built for linux/amd64; on an ARM64 host, build it locally from the Dockerfile.- Without Docker: Python 3.10 or later with Spot (https://spot.lre.epita.fr, tested with 2.15.1) and the packages in requirements.txt (cairosvg, matplotlib, scipy). Spot is not on PyPI; install its Python bindings from your distribution's packages, conda (conda install -c conda-forge spot), or a source build, and then run: pip install -r requirements.txt- Linux (or macOS); the time budgets rely on fork.- Any x86-64 or ARM64 machine with 4 cores and 8 GB of RAM. The paper's numbers come from an Intel Core i5-10210U laptop (4 cores/8 threads at 1.60 GHz, 16 GB of RAM). RUNNING WITH DOCKER unzip scopelines_artifact.zip && cd scopelines_artifact docker load -i scopelines-docker.tar.gz mkdir -p results docker run --rm -it -v "`pwd`/results:/scopelines/results" scopelines This opens a shell in /scopelines, where every command below runs as is; the mounted results directory keeps the outputs on the host. Commands run as the owner of the results directory (see docker-entrypoint.sh), so its files belong to you if you created it, as above. If an earlier run left files owned by root in it, remove them first (e.g. sudo rm -r results/*). The image can also be rebuilt with "docker build -t scopelines ." (about 15-20 minutes, mostly compiling Spot). VIEWING THE RENDERED SCOPELINES The container has no display, so open the rendered SVG/PNG files on the host, where they appear in the results directory (the figures of step 7 in results/figures). From a terminal on the host (a second one, or after leaving the container): xdg-open results/example.svg (Linux) open results/example.svg (macOS) start results\example.svg (Windows) Double-clicking the file in a file manager works too, and SVG files open in any web browser. Without Docker, the same commands open the files directly. QUICK CHECK (ABOUT 1 MINUTE) python3 find_scopeline.py 'G(a -> F b)' --svg results/example.svg python3 run_benchmark.py --limit 4 --timeout 10 python3 analyze_results.py python3 render_figures.py python3 verify_oracle.py random --count 200 python3 verify_oracle.py reported find_scopeline.py prints the scopeline (forall (a) after (sometimes (b))), its LTL translation G(a -> Fb), and "equivalent: True", and draws the scopeline in results/example.svg (see Viewing the rendered scopelines above). The benchmark runs the first 4 formulas of each dataset (20 in all, 19 distinct) and prints a table like Table I; the oracle reports no mismatch. REPRODUCING THE PAPER All outputs go to results/. Steps 2, 3, and 5 read the results of step 1; the others are independent. The runtimes are on the laptop above, about 1.5 hours in all. 1. Search all formulas: python3 run_benchmark.py (about 50 minutes; Section VII) Options: --timeout seconds per formula (default 60); --limit N, only the first N formulas of each dataset (default all); --out directory (default results/). Searches every formula of datasets/ for a scopeline, renders each result as PNG (timed, then discarded), and deduplicates the formulas semantically, within each dataset and across datasets (208 and 186 formulas). Writes results/detail.csv (one row per formula: the scopeline found, the search time, node count, depth, and whether it is an AND/OR combination of the formula's components), results/summary.csv, and results/dedup.json. 2. Derive the results: python3 analyze_results.py (about 5 seconds; Table I, Section VII-B, Figure 7) Options: the results directory (default results/). Prints the dataset statistics of Section VII-A (formula counts, 1 to 15 atomic propositions, 3.28 on average); the rows of Table I (also written to results/table1.tex); the statistics of Section VII-B (detection of 156 of 186 formulas, node counts and depths, event sizes, AND/OR combinations, the largest and the slowest result, the share found in under one second, PNG rendering times, the use of X in events, the undetected formulas, and the mapping of Dwyer's patterns onto the survey of real-world instances); and the Spearman correlations of the scalability analysis, with Figure 7 (results/figure7.png). 3. Decomposition ablation: python3 ablation_no_decomposition.py (about 15 minutes; Section VII-B) Options: the results directory (default results/); --timeout seconds per formula (default 60); --procs, formulas searched in parallel (default half the cores). Reruns, without decomposition, every formula found as an AND/OR combination and every undetected one (8 of the 47 combinations are then found, as single chains). 4. Oracle, random scopelines: python3 verify_oracle.py random (about 17 minutes on 8 threads; Section VII-A) Options: --count scopelines (default 10000); --max-nodes (default 5); --seed (default 1); --procs (default all cores). Compares the independent semantic oracle, which interprets the window semantics of Section III directly on lasso words, with Spot's verdicts for LTL(S) on 10,000 random supported scopelines, each on all 1,216 lasso words over {a, b} with a prefix of at most 2 and a loop of at most 3 letters (12,160,000 checks). Also checks negation duality, the cases of the proof of Theorem 1, and empty windows. 5. Oracle, reported scopelines: python3 verify_oracle.py reported (about 15 seconds; Section VII-A) Options: a detail.csv (default results/detail.csv); --lassos per scopeline (default 1000); --seed (default 1); --procs (default all cores). Compares every scopeline found in step 1 with its original formula on 1,000 random lasso words plus an accepting word of the formula and of its negation, and checks it equivalent with Spot. 6. Fault injection: python3 oracle_mutations.py (about 6 minutes; Section VII-A) Options: the number of random scopelines (default 300); a filter on the fault names (default none). Injects the nine faults listed in the paper into the translation and the supported conditions, one at a time, and shows that the oracle catches each of them. 7. Example figures: python3 render_figures.py (about 10 seconds; Figures 1 and 3-6) Options: the output directory (default results/figures). Steps 4 and 5 should report no mismatch, and step 6 a mismatch for every fault (and none for the unmutated code). WHAT MAY DIFFER FROM THE PAPER - Search times depend on the machine and its load, so they differ from Table I, and so do the statistics computed from them (average and median times, the slowest formula, and the Spearman correlations with search time). Detection does not, except for a formula whose search time is close to the 60-second budget: the slowest one in the paper took 55.83 seconds (50.16 seconds in our rerun), so on a slower machine it may time out. run_benchmark.py --timeout changes the budget. For the same reason, the decomposition ablation (step 3) reports 8 or 9 of the 47 combinations, depending on the run.- The scopelines found are the same up to equivalent alternatives: a rerun on our machine reproduces the paper's detection, node counts, and depths exactly, but for 11 of the 208 formulas it prints a different equivalent scopeline -- the same chains in another order within an AND/OR, or an equivalent event (e.g. a & !b & Xa instead of a & Xa). The search is deterministic for a given run, but Spot orders the operands of a conjunction or disjunction by internal identifiers, which depend on the formulas the process has created before. Two per-dataset event sizes in Table I may therefore differ by 0.01.- PNG rendering times likewise depend on the machine. USING SCOPELINES BEYOND THE PAPER From the command line, for any LTL formula in Spot's syntax, find_scopeline.py prints the scopeline found, its translation into LTL, whether Spot confirms the two equivalent, and the search time. Parameters:- formula: the LTL formula, in Spot's syntax- --timeout SECONDS: the search's time budget (default 60)- --svg FILE: write the rendering as SVG- --png FILE: write the rendering as PNG- --negate: render the negation of the scopeline instead- --no-decompose: search without the decomposition heuristic Examples: python3 find_scopeline.py '(G a) -> (F b)' --png results/out.png --timeout 30 python3 find_scopeline.py 'G(req -> X X ack)' --svg results/out.svg python3 find_scopeline.py 'G(a -> F b)' --png results/negation.png --negate In Docker, write the renderings under results/ to open them on the host (see Viewing the rendered scopelines above). Atomic propositions that start with F, G, or X followed by more letters must be double-quoted (e.g. "FCT_sent"), as Spot would otherwise read them as operators. From Python: import spot from scopelines import find_scopeline, result_ltl, Scopeline, Quantifier from scopelines.render.png import save_png result = find_scopeline("G(a -> F b)", timeout=60) # a runner.Result print(result.status, result) # found (forall (a) after (sometimes (b))) print(result_ltl(result.scopelines, result.operator)) # G(a -> Fb) save_png(result.scopelines, "results/out.png", operator=result.operator) # building a scopeline by hand and translating it into LTL s = Scopeline(spot.formula("b"), Quantifier.EXISTS) s.before = Scopeline(spot.formula("a"), Quantifier.FORALL) s.before.strictly = True print(s, s.is_supported(), s.to_ltl()) # ... True a U b Other datasets can be evaluated by adding CSV files (one formula per line) to datasets/, and the search can be run without the decomposition heuristic with decompose=False (--no-decompose on the command line). CODE OVERVIEW - scopelines/scopeline.py: the scopeline data structure, the supported conditions, negation, and the translation into LTL (Algorithm 1)- scopelines/search.py: the search (Algorithm 2): events, Check, Refine, and the decomposition heuristic- scopelines/runner.py: find_scopeline, the search under a time budget, in a child process- scopelines/render/: rendering: rows per node (layout.py), SVG drawing (svg.py), and standalone SVG/PNG export (png.py)- scopelines/oracle.py: the independent semantic oracle on lasso words- scopelines/parse.py: parsing printed scopelines back into objects- scopelines/dedup.py: semantic deduplication of formulas, up to renaming of atomic propositions- scopelines/utils.py: LTL construction helpers and helpers for search results- datasets/: the five datasets of Section VII-A LICENSE The software (the code in the archive) is licensed under the MIT License; see the LICENSE file. The other content of this record, such as the documentation, is licensed under CC BY 4.0. The datasets are drawn from the sources cited in the paper (a human LTL comprehension study, the ltl2timeline and nl2spec datasets, requirements from the SpaceWire standard, and Dwyer's specification patterns); please cite those sources when reusing them.