Spec Narrowing Eval

spec-narrowing-eval

Synthesizing Test Cases for Narrowing Specification Candidates — Cunha et al. (2025) (arXiv:2511.19177, 2025)

What this evaluates

Evaluates two solver-based algorithms for synthesizing minimal test suites to distinguish between candidate formal specifications (Alloy models). It measures how execution time and test suite size scale with the number of candidate specifications and the domain scope.

Datasets

• Alloy4Fun — total ?; splits: test (28); repo https://github.com/haslab/Specification-Narrowing

Metrics

• execution_time (primary) — range: other
  • Wall-clock time in seconds to synthesize a test suite for a given problem instance. Measured per run with a 60-second timeout.
• test_suite_size — range: other
  • Number of generated test cases (|T|) required to narrow the candidate specifications to at most one. Reported as average or median across completed runs.

Input / output format

Input: Alloy model containing declarations, optional facts, and a sequence of predicates representing candidate specifications, along with a specified scope for bounded analysis.

Output: A set of Alloy run commands constituting the narrowing test suite, or a timeout/failure signal if the solver exceeds 60 seconds.

Scoring recipe

results = []
for problem in benchmark_problems: # 28 reqs * 7 sizes
    start = time()
    try:
        suite = run_algorithm(problem.specs, problem.scope, timeout=60)
        elapsed = time() - start
        results.append({"time": elapsed, "size": len(suite), "status": "success"})
    except TimeoutError:
        results.append({"time": 60, "size": 0, "status": "timeout"})
# Aggregate: avg time, avg/median size, growth rate analysis

Common pitfalls

• Execution time averages only include runs completed within the 60s timeout, masking solver failures for larger candidate sets.
• Increasing the domain scope does not reduce test suite size and may cause timeouts, contradicting the intuition that larger scopes yield better specifications.
• The prototype only supports Alloy v5; models using temporal logic or mutable elements will fail silently or require filtering.

Evidence (verbatim from paper)

To answer RQ1 and RQ2 we executed our prototype implementation of both algorithms on all 28×7 problems of our benchmark using a scope of 3 and collected all the execution times and generated test suite sizes |T|. ... A timeout of 60s was set for each execution of the prototype tool and the chosen SAT solver was SAT4J, which supports PM-SAT problems.

Citation

@misc{cunha2025synthesizingtestcases,
  title={Synthesizing Test Cases for Narrowing Specification Candidates},
  author={Cunha et al. (2025)},
  year={2025},
  note={arXiv:2511.19177}
}

• arXiv: 2511.19177