evaluation.py

"""Run the batch comparison, scope study, and always-online comparison.

Each synthesis request runs in a separate, persistent worker process.  The
driver can therefore enforce a safety timeout on every request and kill the
worker without leaving a Python/JVM process behind. Each request constructs one
complete batch, so the timeout bounds total batch synthesis. Main-scope results
are reused by the scope and online studies, and results are written
incrementally so a long evaluation can be resumed safely.
"""

from __future__ import annotations

import argparse
from copy import deepcopy
from contextlib import redirect_stdout
from datetime import datetime, timezone
import io
import json
import math
import os
from pathlib import Path
import selectors
import statistics
import subprocess
import sys
from timeit import default_timer as timer
from typing import Optional

from evaluation_report import batch_preparation_seconds


ALGORITHMS = ("balanced-split", "arbitrary-split", "joint-cover", "enumerated-cover")
SCOPE_STUDY_ALGORITHMS = ALGORITHMS
TEMPORAL_STUDY_ALGORITHMS = ALGORITHMS
TRACE_STUDY_ALGORITHMS = TEMPORAL_STUDY_ALGORITHMS
METHOD_METADATA = {
    "balanced-split": {
        "display_name": "Balanced Split",
        "family": "tree-guided",
    },
    "arbitrary-split": {
        "display_name": "Arbitrary Split",
        "family": "tree-guided",
    },
    "joint-cover": {
        "display_name": "Joint Cover",
        "family": "cover-based",
    },
    "enumerated-cover": {
        "display_name": "Enumerated Cover",
        "family": "cover-based",
    },
}
CURRENT_FORMAT_VERSION = 8
ALLOYMAX_VERSION = "1.0.2"
DEFAULT_ONLINE_TIMEOUT_SECONDS = 180.0
RESULT_PREFIX = "__SPEC_NARROWING_RESULT__"
ONLINE_RESULT_PREFIX = "__SPEC_NARROWING_ONLINE_RESULT__"


def _trace_length_argument(trace_length: Optional[int]) -> str:
    return "none" if trace_length is None else str(trace_length)


def _parse_trace_length_argument(value: str) -> Optional[int]:
    return None if value == "none" else int(value)


def method_metadata(algorithms):
    """Return JSON-friendly display metadata for the selected method IDs."""

    return {
        algorithm: dict(METHOD_METADATA[algorithm])
        for algorithm in algorithms
    }


def _percentile(values: list[float], fraction: float) -> float:
    ordered = sorted(values)
    if len(ordered) == 1:
        return ordered[0]
    position = fraction * (len(ordered) - 1)
    lower = math.floor(position)
    upper = math.ceil(position)
    if lower == upper:
        return ordered[lower]
    weight = position - lower
    return ordered[lower] * (1 - weight) + ordered[upper] * weight


def number_stats(values) -> Optional[dict[str, float]]:
    """Return descriptive statistics in a JSON-friendly dictionary."""

    numbers = [float(value) for value in values if value is not None]
    if not numbers:
        return None
    return {
        "count": len(numbers),
        "mean": round(statistics.mean(numbers), 2),
        "median": round(statistics.median(numbers), 2),
        "stdev": round(statistics.pstdev(numbers), 2),
        "min": round(min(numbers), 2),
        "p25": round(_percentile(numbers, 0.25), 2),
        "p75": round(_percentile(numbers, 0.75), 2),
        "p95": round(_percentile(numbers, 0.95), 2),
        "max": round(max(numbers), 2),
    }


def _worker_server(
    algorithm: str,
    filename: str,
    scope: int,
    trace_length: Optional[int],
) -> int:
    """Serve newline-delimited synthesis requests on stdin/stdout."""

    from arbitrary_split import arbitrary_split_batch
    from balanced_split import balanced_split_batch
    from enumerated_cover import enumerated_cover_batch
    from joint_cover import joint_cover_batch

    content = Path(filename).read_text()
    strategy = {
        "balanced-split": balanced_split_batch,
        "joint-cover": joint_cover_batch,
        "arbitrary-split": arbitrary_split_batch,
        "enumerated-cover": enumerated_cover_batch,
    }[algorithm]

    for line in sys.stdin:
        request = json.loads(line)
        if request.get("stop"):
            return 0
        messages = io.StringIO()
        algorithm_statistics = None
        try:
            start = timer()
            with redirect_stdout(messages):
                if algorithm in {"balanced-split", "enumerated-cover"}:
                    algorithm_statistics = {}
                    strategy_arguments = (
                        content,
                        scope,
                        trace_length,
                        algorithm_statistics,
                    )
                else:
                    strategy_arguments = (content, scope, trace_length)
                batch = strategy(*strategy_arguments)
                instances = [instance.alloy5 for instance in batch]
                truth_table = [instance.truth_vector for instance in batch]
            response = {
                "status": "completed",
                "synthesis_seconds": timer() - start,
                "instances": instances,
                "truth_table": truth_table,
            }
            if messages.getvalue().strip():
                response["messages"] = messages.getvalue().strip()
            if algorithm_statistics is not None:
                response[algorithm] = algorithm_statistics
        except BaseException as error:
            response = {
                "status": "error",
                "error": f"{type(error).__name__}: {error}",
            }
        print(RESULT_PREFIX + json.dumps(response), flush=True)
    return 0


def _online_worker(
    filename: str,
    scope: int,
    trace_length: Optional[int],
) -> int:
    """Measure all oracle paths of adaptive iterative classification."""

    from balanced_split import iterative_classification_path_costs

    try:
        result = iterative_classification_path_costs(
            Path(filename).read_text(), scope, trace_length
        )
        result["status"] = "completed"
    except BaseException as error:
        result = {
            "status": "error",
            "error": f"{type(error).__name__}: {error}",
        }
    print(ONLINE_RESULT_PREFIX + json.dumps(result), flush=True)
    return 0


def _run_online_problem(
    filename: Path,
    scope: int,
    timeout_seconds: float,
    trace_length: Optional[int] = None,
):
    """Run one online comparison in an isolated, time-bounded process."""

    try:
        completed = subprocess.run(
            [
                sys.executable,
                str(Path(__file__).resolve()),
                "_online_worker",
                str(filename),
                str(scope),
                _trace_length_argument(trace_length),
            ],
            capture_output=True,
            text=True,
            timeout=timeout_seconds,
            check=False,
        )
    except subprocess.TimeoutExpired:
        return {
            "status": "timeout",
            "synthesis_timeout_seconds": timeout_seconds,
        }
    for line in completed.stdout.splitlines():
        if line.startswith(ONLINE_RESULT_PREFIX):
            return json.loads(line[len(ONLINE_RESULT_PREFIX) :])
    return {
        "status": "error",
        "error": completed.stderr.strip() or "online worker returned no result",
    }


class SynthesisServer:
    """A restartable synthesis worker with a timeout for each request."""

    def __init__(
        self,
        algorithm,
        filename,
        scope,
        timeout_seconds,
        trace_length=None,
    ):
        self.algorithm = algorithm
        self.filename = str(filename)
        self.scope = scope
        self.timeout_seconds = timeout_seconds
        self.trace_length = trace_length
        self.process = None

    def start(self):
        if self.process is not None and self.process.poll() is None:
            return
        self.process = subprocess.Popen(
            [
                sys.executable,
                str(Path(__file__).resolve()),
                "_worker",
                self.algorithm,
                self.filename,
                str(self.scope),
                _trace_length_argument(self.trace_length),
            ],
            stdin=subprocess.PIPE,
            stdout=subprocess.PIPE,
            stderr=subprocess.DEVNULL,
            text=True,
            bufsize=1,
        )

    def request(self, candidates=None):
        self.start()
        request = {} if candidates is None else {"candidates": candidates}
        try:
            self.process.stdin.write(json.dumps(request) + "\n")
            self.process.stdin.flush()
        except (BrokenPipeError, OSError) as error:
            self.stop()
            return {"status": "error", "error": str(error)}

        deadline = timer() + self.timeout_seconds
        selector = selectors.DefaultSelector()
        selector.register(self.process.stdout, selectors.EVENT_READ)
        try:
            while True:
                remaining = deadline - timer()
                if remaining <= 0 or not selector.select(remaining):
                    self.stop()
                    return {
                        "status": "timeout",
                        "timeout_seconds": self.timeout_seconds,
                    }
                line = self.process.stdout.readline()
                if not line:
                    result = {
                        "status": "error",
                        "error": f"synthesis worker exited with {self.process.poll()}",
                    }
                    self.stop()
                    return result
                if line.startswith(RESULT_PREFIX):
                    return json.loads(line[len(RESULT_PREFIX) :])
        finally:
            selector.close()

    def stop(self):
        process = self.process
        self.process = None
        if process is None:
            return
        if process.poll() is None:
            try:
                process.stdin.write(json.dumps({"stop": True}) + "\n")
                process.stdin.flush()
                process.wait(timeout=1)
            except (BrokenPipeError, OSError, subprocess.TimeoutExpired):
                process.terminate()
                try:
                    process.wait(timeout=2)
                except subprocess.TimeoutExpired:
                    process.kill()
                    process.wait()
        if process.stdin is not None:
            process.stdin.close()
        if process.stdout is not None:
            process.stdout.close()

    def __enter__(self):
        self.start()
        return self

    def __exit__(self, _type, _value, _traceback):
        self.stop()


def fixed_classification_counts(predicates, truth_table):
    """Adaptively order a fixed suite for every possible ground truth."""

    counts = {}
    errors = {}
    for oracle in predicates:
        remaining = list(predicates)
        answered = set()
        classifications = 0
        while len(remaining) > 1:
            ranked = []
            for index, truths in enumerate(truth_table):
                if index in answered:
                    continue
                desirable = [p for p in remaining if truths[p]]
                undesirable = [p for p in remaining if not truths[p]]
                if not desirable or not undesirable:
                    continue
                ranked.append(
                    (
                        max(len(desirable), len(undesirable)),
                        -len(desirable) * len(undesirable),
                        index,
                    )
                )
            if not ranked:
                errors[oracle] = "fixed suite does not distinguish remaining candidates"
                break
            index = min(ranked)[2]
            answered.add(index)
            answer = truth_table[index][oracle]
            remaining = [p for p in remaining if truth_table[index][p] == answer]
            classifications += 1
        counts[oracle] = classifications if remaining == [oracle] else None
    return counts, errors


def evaluate_batch(
    collector,
    filename,
    algorithm,
    scope,
    timeout_seconds,
    trace_length=None,
):
    predicates = list(collector.predicates)
    with SynthesisServer(
        algorithm,
        filename,
        scope,
        timeout_seconds,
        trace_length,
    ) as server:
        synthesis = server.request()
    result = {
        "algorithm": algorithm,
        "status": synthesis["status"],
        "synthesis_status": synthesis["status"],
        "evaluation_status": "not_run",
        "synthesis_timeout_seconds": timeout_seconds,
        "classifications": {predicate: None for predicate in predicates},
        "classification_stats": None,
        "completed_oracles": 0,
        "total_oracles": len(predicates),
    }
    if collector.temporal:
        result["trace_length"] = collector.trace_length
    if synthesis["status"] != "completed":
        result.update(
            {
                key: value
                for key, value in synthesis.items()
                if key not in {"status", "timeout_seconds"}
            }
        )
        result["failure_stage"] = "synthesis"
        return result

    instances = synthesis["instances"]
    # Retain successful synthesis even if later table handling or review fails.
    result.update({
        "test_suite_size": len(instances),
        "synthesis_seconds": round(synthesis["synthesis_seconds"], 2),
    })
    if synthesis.get("messages"):
        result["messages"] = synthesis["messages"]
    for method in ("enumerated-cover", "balanced-split"):
        if synthesis.get(method) is not None:
            details = dict(synthesis[method])
            for key in ("enumeration_seconds", "cover_seconds"):
                if details.get(key) is not None:
                    details[key] = round(details[key], 2)
            result[method] = details
    try:
        truth_table = synthesis.get("truth_table")
        if not isinstance(truth_table, list) or len(truth_table) != len(instances) or any(
            not isinstance(row, dict)
            or any(type(row.get(predicate)) is not bool for predicate in predicates)
            for row in truth_table
        ):
            raise ValueError("synthesis returned incomplete candidate predictions")
        result["truth_vector_source"] = "synthesis"
    except Exception as error:
        result.update({
            "status": "error",
            "evaluation_status": "error",
            "failure_stage": "truth_vector_validation",
            "error": f"{type(error).__name__}: {error}",
        })
        return result
    result["evaluation_status"] = "completed"
    counts, errors = fixed_classification_counts(predicates, truth_table)
    result.update(
        {
            "classifications": counts,
            "classification_stats": number_stats(counts.values()),
            "completed_oracles": sum(value is not None for value in counts.values()),
            "total_oracles": len(predicates),
        }
    )
    if errors:
        result["oracle_errors"] = errors
        result["status"] = "partial"
        result["failure_stage"] = "classification"
    return result


def _problem_key(path: Path):
    parts = path.stem.rsplit("_", 2)
    try:
        size = int(parts[-1])
    except (ValueError, IndexError):
        size = 0
    return size, path.name


def _problem_metadata(path: Path, predicates, collector=None):
    parts = path.stem.rsplit("_", 2)
    metadata = {
        "file": path.name,
        "model": parts[0] if len(parts) == 3 else None,
        "requirement": parts[1] if len(parts) == 3 else None,
        "declared_size": int(parts[2]) if len(parts) == 3 else len(predicates),
        "candidate_count": len(predicates),
        "candidates": list(predicates),
    }
    if collector is not None:
        metadata["temporal"] = collector.temporal
        if collector.temporal:
            metadata["trace_length"] = collector.trace_length
    return metadata


def _format_stats(stats):
    if stats is None:
        return "no completed oracles"
    return (
        f"mean {stats['mean']:.2f}, median {stats['median']:.2f}, "
        f"min {stats['min']:.2f}, p95 {stats['p95']:.2f}, "
        f"max {stats['max']:.2f}"
    )


def print_algorithm_result(key, result):
    suffix = _format_stats(result.get("classification_stats"))
    extra = ""
    if result.get("failure_stage"):
        extra = f"; failure during {result['failure_stage']}"
    if "test_suite_size" in result:
        extra += (
            f"; suite {result['test_suite_size']}; "
            f"synthesis {result['synthesis_seconds']:.2f} seconds"
        )
        if result.get("enumerated-cover"):
            enumeration = result["enumerated-cover"]
            extra += (
                f"; enumerated {enumeration['separation_patterns']} "
                "separation patterns in "
                f"{enumeration.get('enumeration_solver_calls', 'unknown')} "
                "SAT calls; "
                "enumeration/cover "
                f"{enumeration['enumeration_seconds']:.2f}/"
                f"{enumeration['cover_seconds']:.2f} seconds"
            )
        if result.get("balanced-split"):
            balanced = result["balanced-split"]
            extra += (
                f"; MaxSAT calls {balanced['maxsat_calls']}; "
                f"reuses {balanced['ideal_reuses'] + balanced['matched_reuses']}"
            )
    print(
        f"  {key:24} {result['status']:9} "
        f"{result.get('completed_oracles', 0)}/{result.get('total_oracles', 0)} "
        f"oracles; classifications {suffix}{extra}",
        flush=True,
    )


def synthesis_completed(result):
    """Separate batch synthesis from later validation and review simulation."""

    return result.get("synthesis_status", result.get("status")) == "completed"


def grouped_summary(problems):
    summary = {}
    for key in ALGORITHMS:
        by_size = {}
        for problem in problems:
            size = str(problem["candidate_count"])
            result = problem["algorithms"].get(key)
            if result is None:
                continue
            bucket = by_size.setdefault(
                size,
                {
                    "problems": 0,
                    "completed_problems": 0,
                    "synthesis_completed_problems": 0,
                    "post_synthesis_errors": 0,
                    "completed_oracles": 0,
                    "total_oracles": 0,
                    "classifications": [],
                    "test_suite_sizes": [],
                    "synthesis_seconds": [],
                    "enumerated_instances": [],
                    "separation_patterns": [],
                    "enumeration_solver_calls": [],
                    "enumeration_seconds": [],
                    "cover_seconds": [],
                },
            )
            bucket["problems"] += 1
            bucket["completed_problems"] += result["status"] == "completed"
            bucket["synthesis_completed_problems"] += synthesis_completed(result)
            bucket["post_synthesis_errors"] += synthesis_completed(result) and result["status"] != "completed"
            bucket["completed_oracles"] += result.get("completed_oracles", 0)
            bucket["total_oracles"] += result.get("total_oracles", 0)
            bucket["classifications"].extend(
                value
                for value in result.get("classifications", {}).values()
                if value is not None
            )
            if result.get("test_suite_size") is not None:
                bucket["test_suite_sizes"].append(result["test_suite_size"])
            if result.get("enumerated-cover"):
                enumeration = result["enumerated-cover"]
                bucket["enumerated_instances"].append(
                    enumeration["enumerated_instances"]
                )
                bucket["separation_patterns"].append(
                    enumeration["separation_patterns"]
                )
                if enumeration.get("enumeration_solver_calls") is not None:
                    bucket["enumeration_solver_calls"].append(
                        enumeration["enumeration_solver_calls"]
                    )
                bucket["enumeration_seconds"].append(
                    enumeration["enumeration_seconds"]
                )
                bucket["cover_seconds"].append(enumeration["cover_seconds"])
            if result.get("synthesis_seconds") is not None:
                bucket["synthesis_seconds"].append(result["synthesis_seconds"])
        summary[key] = {}
        for size, bucket in by_size.items():
            summary[key][size] = {
                key: value
                for key, value in bucket.items()
                if key
                not in {
                    "classifications",
                    "test_suite_sizes",
                    "synthesis_seconds",
                    "enumerated_instances",
                    "separation_patterns",
                    "enumeration_solver_calls",
                    "enumeration_seconds",
                    "cover_seconds",
                }
            }
            summary[key][size]["classification_stats"] = number_stats(
                bucket["classifications"]
            )
            if bucket["test_suite_sizes"]:
                summary[key][size]["test_suite_size_stats"] = number_stats(
                    bucket["test_suite_sizes"]
                )
            for values_key, stats_key in (
                ("synthesis_seconds", "synthesis_seconds_stats"),
                ("enumerated_instances", "enumerated_instances_stats"),
                ("separation_patterns", "separation_patterns_stats"),
                (
                    "enumeration_solver_calls",
                    "enumeration_solver_calls_stats",
                ),
                ("enumeration_seconds", "enumeration_seconds_stats"),
                ("cover_seconds", "cover_seconds_stats"),
            ):
                if bucket[values_key]:
                    summary[key][size][stats_key] = number_stats(bucket[values_key])
    return summary


def _scope_study_problem(main_problem):
    """Copy stable problem metadata without duplicating main-study results."""

    return {
        key: deepcopy(main_problem[key])
        for key in (
            "file",
            "model",
            "requirement",
            "declared_size",
            "candidate_count",
            "candidates",
            "temporal",
            "trace_length",
        )
        if key in main_problem
    } | {"scopes": {}}


def _trace_study_problem(main_problem):
    """Copy stable problem metadata for the temporal-depth study."""

    return {
        key: deepcopy(main_problem[key])
        for key in (
            "file",
            "model",
            "requirement",
            "declared_size",
            "candidate_count",
            "candidates",
            "temporal",
            "trace_length",
        )
        if key in main_problem
    } | {"trace_lengths": {}}


def scope_study_summary(study):
    """Summarize completed scope runs and the Joint Cover completion subset."""

    scopes = [str(scope) for scope in study["configuration"]["scopes"]]
    algorithm_keys = list(
        dict.fromkeys(
            study["configuration"]["algorithms"]
            + study["configuration"].get("temporal_algorithms", [])
        )
    )
    by_scope = {key: {} for key in algorithm_keys}
    for key in algorithm_keys:
        for scope in scopes:
            results = [
                problem.get("scopes", {}).get(scope, {}).get(key)
                for problem in study.get("problems", [])
            ]
            results = [result for result in results if result is not None]
            completed = [
                result for result in results if result.get("status") == "completed"
            ]
            synthesized = [result for result in results if synthesis_completed(result)]
            by_scope[key][scope] = {
                "problems": len(results),
                "completed_problems": len(completed),
                "synthesis_completed_problems": len(synthesized),
                "post_synthesis_errors": sum(result.get("status") != "completed" for result in synthesized),
                "completed_oracles": sum(
                    result.get("completed_oracles", 0) for result in results
                ),
                "total_oracles": sum(
                    result.get("total_oracles", 0) for result in results
                ),
                "test_suite_size_stats": number_stats(
                    result.get("test_suite_size") for result in completed
                ),
                "classification_stats": number_stats(
                    classification
                    for result in completed
                    for classification in result.get("classifications", {}).values()
                    if classification is not None
                ),
                "synthesis_seconds_stats": number_stats(
                    result.get("synthesis_seconds") for result in synthesized
                ),
            }

    joint_cover_key = "joint-cover"
    paired_problems = [
        problem
        for problem in study.get("problems", [])
        if all(
            problem.get("scopes", {})
            .get(scope, {})
            .get(joint_cover_key, {})
            .get("status")
            == "completed"
            for scope in scopes
        )
    ]
    paired_algorithms = {key: {} for key in algorithm_keys}
    for key in algorithm_keys:
        for scope in scopes:
            results = [
                problem["scopes"][scope].get(key) for problem in paired_problems
            ]
            results = [
                result
                for result in results
                if result is not None and result.get("status") == "completed"
            ]
            paired_algorithms[key][scope] = {
                "completed_problems": len(results),
                "test_suite_size_stats": number_stats(
                    result.get("test_suite_size") for result in results
                ),
                "classification_stats": number_stats(
                    classification
                    for result in results
                    for classification in result.get("classifications", {}).values()
                    if classification is not None
                ),
            }
    return {
        "by_scope": by_scope,
        "paired_joint_cover_completed_all_scopes": {
            "problem_count": len(paired_problems),
            "files": [problem["file"] for problem in paired_problems],
            "algorithms": paired_algorithms,
        },
    }


def trace_study_summary(study):
    """Summarize the independent temporal trace-length experiment."""

    trace_lengths = [
        str(trace_length)
        for trace_length in study["configuration"]["trace_lengths"]
    ]
    algorithm_keys = study["configuration"]["algorithms"]
    by_trace_length = {key: {} for key in algorithm_keys}
    for key in algorithm_keys:
        for trace_length in trace_lengths:
            results = [
                problem.get("trace_lengths", {}).get(trace_length, {}).get(key)
                for problem in study.get("problems", [])
            ]
            results = [result for result in results if result is not None]
            completed = [
                result for result in results if result.get("status") == "completed"
            ]
            synthesized = [result for result in results if synthesis_completed(result)]
            by_trace_length[key][trace_length] = {
                "problems": len(results),
                "completed_problems": len(completed),
                "synthesis_completed_problems": len(synthesized),
                "post_synthesis_errors": sum(result.get("status") != "completed" for result in synthesized),
                "completed_oracles": sum(
                    result.get("completed_oracles", 0) for result in results
                ),
                "total_oracles": sum(
                    result.get("total_oracles", 0) for result in results
                ),
                "test_suite_size_stats": number_stats(
                    result.get("test_suite_size") for result in completed
                ),
                "classification_stats": number_stats(
                    classification
                    for result in completed
                    for classification in result.get("classifications", {}).values()
                    if classification is not None
                ),
                "synthesis_seconds_stats": number_stats(
                    result.get("synthesis_seconds") for result in synthesized
                ),
            }

    paired_problems = [
        problem
        for problem in study.get("problems", [])
        if all(
            problem.get("trace_lengths", {})
            .get(trace_length, {})
            .get("joint-cover", {})
            .get("status")
            == "completed"
            for trace_length in trace_lengths
        )
    ]
    return {
        "by_trace_length": by_trace_length,
        "paired_joint_cover_completed_all_trace_lengths": {
            "problem_count": len(paired_problems),
            "files": [problem["file"] for problem in paired_problems],
        },
    }


def online_comparison_summary(document):
    """Compare upfront batch synthesis with cumulative iterative oracle paths."""

    study = document.get("online_comparison", {})
    batch_by_file = {
        problem["file"]: problem["algorithms"]["balanced-split"]
        for problem in document.get("problems", [])
        if problem.get("algorithms", {}).get("balanced-split", {}).get("status")
        == "completed"
    }
    completed = [
        result
        for result in study.get("problems", [])
        if result.get("status") == "completed" and result["file"] in batch_by_file
    ]
    if not completed:
        return {"completed_configurations": 0}

    timed = [
        result for result in completed
        if batch_preparation_seconds(batch_by_file[result["file"]]) is not None
    ]
    counts = {
        "completed_configurations": len(completed),
        "timed_configurations": len(timed),
        "completed_oracle_paths": sum(len(result["path_synthesis_seconds"]) for result in completed),
    }
    if not timed:
        return counts
    batch_seconds = [
        batch_preparation_seconds(batch_by_file[result["file"]]) for result in timed
    ]
    online_configuration_means = [
        statistics.mean(result["path_synthesis_seconds"].values())
        for result in timed
    ]
    online_paths = [
        seconds
        for result in timed
        for seconds in result["path_synthesis_seconds"].values()
    ]
    ratios = [
        online / batch
        for online, batch in zip(online_configuration_means, batch_seconds)
        if batch > 0
    ]
    paired_differences = [
        batch - online
        for batch, online in zip(batch_seconds, online_configuration_means)
    ]
    return {
        **counts,
        "batch_preparation_seconds": {
            "mean": statistics.mean(batch_seconds),
            "median": statistics.median(batch_seconds),
        },
        "online_mean_path_synthesis_seconds": {
            "mean_across_configurations": statistics.mean(
                online_configuration_means
            ),
            "median_across_configurations": statistics.median(
                online_configuration_means
            ),
            "path_weighted_mean": statistics.mean(online_paths),
            "path_weighted_median": statistics.median(online_paths),
        },
        "online_to_batch_ratio": {
            "mean": statistics.mean(ratios),
            "median": statistics.median(ratios),
        },
        "paired_batch_minus_online_seconds": {
            "mean": statistics.mean(paired_differences),
            "median": statistics.median(paired_differences),
            "min": min(paired_differences),
            "max": max(paired_differences),
            "batch_slower_configurations": sum(
                difference > 0 for difference in paired_differences
            ),
        },
    }


def _normalize_study_trace_length(configuration, trace_length, label):
    """Add a trace bound to legacy study metadata or verify an existing one."""

    if "temporal_trace_length" not in configuration:
        configuration["temporal_trace_length"] = trace_length
        return True
    existing = configuration["temporal_trace_length"]
    if existing is not None and existing != trace_length:
        raise ValueError(
            f"cannot resume: existing {label} temporal trace length "
            "does not match --trace-length"
        )
    if existing is None and trace_length is not None:
        configuration["temporal_trace_length"] = trace_length
        return True
    return False


def ensure_online_comparison(document, timeout_seconds, trace_length=None):
    """Initialize and normalize metadata for the paired iterative baseline."""

    expected = {
        "baseline_method": "iterative",
        "paired_batch_method": "balanced-split",
        "scope": document["configuration"]["scope"],
        "temporal_trace_length": trace_length,
        "synthesis_timeout_seconds": timeout_seconds,
        "eligible_batch_status": "completed",
        "aggregation": "mean oracle-path cost per configuration",
        "batch_runtime_components": ["synthesis_seconds"],
    }
    changed = False
    study = document.get("online_comparison")
    if study is None:
        study = {
            "configuration": expected,
            "problems": [],
        }
        document["online_comparison"] = study
        changed = True
    else:
        configuration = study.setdefault("configuration", {})
        changed |= _normalize_study_trace_length(
            configuration, trace_length, "online-comparison"
        )
        old_timeout = configuration.pop("timeout_seconds", None)
        if old_timeout is not None:
            changed = True
        if old_timeout is not None and "synthesis_timeout_seconds" not in configuration:
            configuration["synthesis_timeout_seconds"] = old_timeout
        # The legacy field conflated the baseline with its paired batch method.
        if "method" in configuration:
            del configuration["method"]
            changed = True
        for key, value in expected.items():
            if configuration.get(key) != value:
                if (
                    key in {"scope", "synthesis_timeout_seconds"}
                    and configuration.get(key) is not None
                ):
                    raise ValueError(
                        "cannot resume: existing online-comparison scope or "
                        "timeout does not match the requested configuration"
                    )
                configuration[key] = value
                changed = True
        if configuration.pop("batch_results", None) is not None:
            changed = True
        if configuration.pop("problems_directory", None) is not None:
            changed = True

    summary = online_comparison_summary(document)
    if study.get("summary") != summary:
        study["summary"] = summary
        changed = True
    return changed


def ensure_scope_study(
    document,
    candidate_count,
    scopes,
    timeout_seconds,
    trace_length=None,
    temporal_candidate_count=None,
):
    """Initialize scope sensitivity studies and reuse matching main-study results."""

    scopes = sorted(set(scopes))
    if temporal_candidate_count is None:
        temporal_candidate_count = candidate_count
    algorithms = list(SCOPE_STUDY_ALGORITHMS)
    temporal_algorithms = list(TEMPORAL_STUDY_ALGORITHMS)
    main_scope = document.get("configuration", {}).get("scope")
    expected = {
        "candidate_count": candidate_count,
        "temporal_candidate_count": temporal_candidate_count,
        "scopes": scopes,
        "algorithms": algorithms,
        "method_metadata": method_metadata(algorithms),
        "temporal_algorithms": temporal_algorithms,
        "temporal_method_metadata": method_metadata(temporal_algorithms),
        "synthesis_timeout_seconds": timeout_seconds,
        "temporal_trace_length": trace_length,
        "alloymax_version": ALLOYMAX_VERSION,
    }
    changed = False
    study = document.get("scope_study")
    if study is None:
        study = {
            "configuration": expected,
            "problems": [],
        }
        document["scope_study"] = study
        changed = True
    else:
        study_configuration = study.setdefault("configuration", {})
        # Extend the original static study without invalidating its measurements.
        if study_configuration.get("algorithms") == [
            "balanced-split", "arbitrary-split", "joint-cover"
        ]:
            study_configuration["algorithms"] = algorithms
            study_configuration["method_metadata"] = method_metadata(algorithms)
            changed = True
        changed |= _normalize_study_trace_length(
            study_configuration, trace_length, "scope-study"
        )
        old_trace_lengths = study_configuration.pop(
            "temporal_trace_lengths_by_scope", None
        )
        if old_trace_lengths is not None:
            has_diagonal_temporal_results = any(
                problem.get("temporal")
                and any(
                    int(scope) != main_scope
                    and results
                    and any(
                        result.get("trace_length", trace_length) != trace_length
                        for result in results.values()
                    )
                    for scope, results in problem.get("scopes", {}).items()
                )
                for problem in study.get("problems", [])
            )
            if has_diagonal_temporal_results:
                raise ValueError(
                    "cannot resume: existing scope-study results used an "
                    "increasing trace length; remove scope_study from the "
                    "output or start a new output file"
                )
            changed = True
        if "temporal_candidate_count" not in study_configuration:
            has_temporal_results = any(
                problem.get("temporal")
                and any(problem.get("scopes", {}).values())
                for problem in study.get("problems", [])
            )
            if has_temporal_results and temporal_candidate_count != candidate_count:
                raise ValueError(
                    "cannot resume: existing temporal scope-study results use "
                    "the old shared candidate count"
                )
            study_configuration["temporal_candidate_count"] = (
                temporal_candidate_count
            )
            changed = True
        if "alloymax_version" not in study_configuration:
            study_configuration["alloymax_version"] = ALLOYMAX_VERSION
            changed = True
        if "method_metadata" not in study_configuration:
            study_configuration["method_metadata"] = method_metadata(algorithms)
            changed = True
        if "temporal_algorithms" not in study_configuration:
            study_configuration["temporal_algorithms"] = temporal_algorithms
            changed = True
        if "temporal_method_metadata" not in study_configuration:
            study_configuration["temporal_method_metadata"] = method_metadata(
                temporal_algorithms
            )
            changed = True
        if study_configuration != expected:
            raise ValueError(
                "cannot resume: existing scope-study configuration does not "
                "match the requested static/temporal candidate counts, scopes, algorithms, "
                "timeout, temporal trace length, or AlloyMax version"
            )

    study_by_file = {
        problem["file"]: problem for problem in study.get("problems", [])
    }
    for main_problem in document.get("problems", []):
        expected_candidate_count = (
            temporal_candidate_count
            if main_problem.get("temporal")
            else candidate_count
        )
        if main_problem.get("candidate_count") != expected_candidate_count:
            continue
        problem = study_by_file.get(main_problem["file"])
        if problem is None:
            problem = _scope_study_problem(main_problem)
            study["problems"].append(problem)
            study_by_file[main_problem["file"]] = problem
            changed = True
        if main_scope not in scopes:
            continue
        scope_results = problem["scopes"].setdefault(str(main_scope), {})
        problem_algorithms = (
            temporal_algorithms if main_problem.get("temporal") else algorithms
        )
        for key in problem_algorithms:
            main_result = main_problem.get("algorithms", {}).get(key)
            if main_result is not None and key not in scope_results:
                scope_results[key] = deepcopy(main_result)
                changed = True

    summary = scope_study_summary(study)
    if study.get("summary") != summary:
        study["summary"] = summary
        changed = True
    if document.get("format_version") != CURRENT_FORMAT_VERSION:
        document["format_version"] = CURRENT_FORMAT_VERSION
        changed = True
    return changed


def ensure_trace_study(
    document,
    candidate_count,
    trace_lengths,
    timeout_seconds,
    base_trace_length,
):
    """Initialize the fixed-scope temporal-depth study and reuse base results."""

    trace_lengths = sorted(set(trace_lengths))
    algorithms = list(TRACE_STUDY_ALGORITHMS)
    fixed_scope = document["configuration"]["scope"]
    expected = {
        "candidate_count": candidate_count,
        "fixed_scope": fixed_scope,
        "trace_lengths": trace_lengths,
        "algorithms": algorithms,
        "method_metadata": method_metadata(algorithms),
        "synthesis_timeout_seconds": timeout_seconds,
        "alloymax_version": ALLOYMAX_VERSION,
    }
    changed = False
    study = document.get("trace_study")
    if study is None:
        study = {"configuration": expected, "problems": []}
        document["trace_study"] = study
        changed = True
    else:
        configuration = study.setdefault("configuration", {})
        existing_algorithms = configuration.get("algorithms", [])
        comparable_existing = {
            key: value
            for key, value in configuration.items()
            if key not in {"algorithms", "method_metadata"}
        }
        comparable_expected = {
            key: value
            for key, value in expected.items()
            if key not in {"algorithms", "method_metadata"}
        }
        if (
            comparable_existing != comparable_expected
            or not set(existing_algorithms).issubset(algorithms)
        ):
            raise ValueError(
                "cannot resume: existing trace-study configuration does not "
                "match the requested candidate count, fixed scope, trace "
                "range, timeout, or AlloyMax version"
            )
        if existing_algorithms != algorithms:
            configuration["algorithms"] = algorithms
            changed = True
        expected_metadata = method_metadata(algorithms)
        if configuration.get("method_metadata") != expected_metadata:
            configuration["method_metadata"] = expected_metadata
            changed = True

    study_by_file = {
        problem["file"]: problem for problem in study.get("problems", [])
    }
    for main_problem in document.get("problems", []):
        if (
            not main_problem.get("temporal")
            or main_problem.get("candidate_count") != candidate_count
        ):
            continue
        problem = study_by_file.get(main_problem["file"])
        if problem is None:
            problem = _trace_study_problem(main_problem)
            study["problems"].append(problem)
            study_by_file[main_problem["file"]] = problem
            changed = True
        if base_trace_length not in trace_lengths:
            continue
        base_results = problem["trace_lengths"].setdefault(
            str(base_trace_length), {}
        )
        for key in algorithms:
            main_result = main_problem.get("algorithms", {}).get(key)
            if main_result is not None and key not in base_results:
                base_results[key] = deepcopy(main_result)
                changed = True

    summary = trace_study_summary(study)
    if study.get("summary") != summary:
        study["summary"] = summary
        changed = True
    return changed


def save_results(output: Path, document):
    document["updated_at"] = datetime.now(timezone.utc).isoformat()
    output.parent.mkdir(parents=True, exist_ok=True)
    temporary = output.with_suffix(output.suffix + ".tmp")
    temporary.write_text(json.dumps(document, indent=2, sort_keys=True) + "\n")
    os.replace(temporary, output)


def _positive_int(value):
    parsed = int(value)
    if parsed < 1:
        raise argparse.ArgumentTypeError("must be at least 1")
    return parsed


def argument_parser():
    parser = argparse.ArgumentParser(
        description=(
            "Evaluate Arbitrary Split, Balanced Split, Joint Cover, and "
            "Enumerated Cover batch synthesis, the scope study, and adaptive "
            "iterative classification."
        )
    )
    parser.add_argument("--problems", type=Path, default=Path("problems"))
    parser.add_argument("--output", type=Path, default=Path("evaluation-results.json"))
    report_mode = parser.add_mutually_exclusive_group()
    report_mode.add_argument(
        "--paper-report",
        action="store_true",
        help=(
            "read --output and print the paper tables and compact supporting "
            "summaries without running or modifying an evaluation"
        ),
    )
    report_mode.add_argument(
        "--full-report",
        action="store_true",
        help=(
            "read --output and print all RQ tables, diagnostics, and pairwise "
            "comparisons without running or modifying an evaluation"
        ),
    )
    parser.add_argument("--scope", type=int, default=3)
    parser.add_argument(
        "--trace-length",
        type=_positive_int,
        help=(
            "maximum number of states for temporal Alloy models; required "
            "when selected problems use temporal syntax"
        ),
    )
    parser.add_argument(
        "--timeout",
        type=float,
        default=60.0,
        help=(
            "total synthesis budget for constructing one complete batch "
            "(default: 60 seconds)"
        ),
    )
    parser.add_argument("--min-size", type=int)
    parser.add_argument("--max-size", type=int)
    parser.add_argument("--limit", type=int, help="process only the first N problems")
    parser.add_argument(
        "--study",
        choices=("all", "main", "scope", "online"),
        default="main",
        help=(
            "run every study, or only the main, scope, or online comparison "
            "(default: main)"
        ),
    )
    parser.add_argument(
        "--online-timeout",
        type=float,
        default=DEFAULT_ONLINE_TIMEOUT_SECONDS,
        help=(
            "safety timeout for traversing one online balanced tree "
            f"(default: {DEFAULT_ONLINE_TIMEOUT_SECONDS:g} seconds)"
        ),
    )
    parser.add_argument(
        "--scope-study-size",
        type=int,
        help="candidate count for static scope studies (default: 16)",
    )
    parser.add_argument(
        "--temporal-study-size",
        type=int,
        help=(
            "candidate count for temporal scope and trace-length studies "
            "(default: --scope-study-size)"
        ),
    )
    parser.add_argument("--scope-study-min", type=int, default=3)
    parser.add_argument("--scope-study-max", type=int, default=7)
    parser.add_argument(
        "--trace-study-min",
        type=_positive_int,
        help="minimum trace length in the temporal-depth study",
    )
    parser.add_argument(
        "--trace-study-max",
        type=_positive_int,
        help="maximum trace length in the temporal-depth study",
    )
    output_mode = parser.add_mutually_exclusive_group()
    output_mode.add_argument(
        "--resume",
        action="store_true",
        help="resume an existing output file (the default when it exists)",
    )
    output_mode.add_argument(
        "--overwrite",
        action="store_true",
        help="discard an existing output file and start a new evaluation",
    )
    return parser


def _main_paths(args):
    paths = sorted(args.problems.glob("*.als"), key=_problem_key)
    if args.min_size is not None:
        paths = [path for path in paths if _problem_key(path)[0] >= args.min_size]
    if args.max_size is not None:
        paths = [path for path in paths if _problem_key(path)[0] <= args.max_size]
    if args.limit is not None:
        paths = paths[: args.limit]
    return paths


def _scope_study_paths(args):
    from alloy import requires_trace_length

    paths = sorted(args.problems.glob("*.als"), key=_problem_key)
    paths = [
        path
        for path in paths
        if _problem_key(path)[0]
        == (
            args.temporal_study_size
            if requires_trace_length(path.read_text())
            else args.scope_study_size
        )
    ]
    if args.limit is not None:
        paths = paths[: args.limit]
    return paths


def _trace_study_paths(args):
    from alloy import requires_trace_length

    return [
        path
        for path in _scope_study_paths(args)
        if requires_trace_length(path.read_text())
    ]


def _configure_study_arguments(args):
    if args.scope_study_size is None:
        args.scope_study_size = 16
    if args.scope_study_size < 1:
        raise SystemExit("--scope-study-size must be at least 1")
    if args.temporal_study_size is None:
        args.temporal_study_size = args.scope_study_size
    if args.temporal_study_size < 1:
        raise SystemExit("--temporal-study-size must be at least 1")
    if args.trace_length is None:
        if args.trace_study_min is not None or args.trace_study_max is not None:
            raise SystemExit("--trace-study-min/max require --trace-length")
        args.trace_study_min = None
        args.trace_study_max = None
        return
    if args.trace_study_min is None:
        args.trace_study_min = args.trace_length
    if args.trace_study_max is None:
        args.trace_study_max = args.trace_length + (
            args.scope_study_max - args.scope_study_min
        )
    if args.trace_study_min > args.trace_study_max:
        raise SystemExit("--trace-study-min cannot exceed --trace-study-max")


def _trace_study_values(args):
    if args.trace_study_min is None:
        return []
    return range(args.trace_study_min, args.trace_study_max + 1)


def _selected_paths(args):
    paths = []
    if args.study in {"all", "main", "online"}:
        paths.extend(_main_paths(args))
    if args.study in {"all", "scope"}:
        paths.extend(_scope_study_paths(args))
    return list(dict.fromkeys(paths))


def _validate_temporal_trace_length(args, requires_trace_length):
    if args.trace_length is not None:
        return
    temporal_paths = [
        path
        for path in _selected_paths(args)
        if requires_trace_length(path.read_text())
    ]
    if temporal_paths:
        example = temporal_paths[0]
        raise SystemExit(
            "--trace-length is required because the selected problems include "
            f"temporal Alloy syntax (for example, {example})"
        )


def _new_document(args):
    return {
        "format_version": CURRENT_FORMAT_VERSION,
        "created_at": datetime.now(timezone.utc).isoformat(),
        "configuration": {
            "scope": args.scope,
            "synthesis_timeout_seconds": args.timeout,
            "problems_directory": str(args.problems),
            "algorithms": list(ALGORITHMS),
            "method_metadata": method_metadata(ALGORITHMS),
            "alloymax_version": ALLOYMAX_VERSION,
            "temporal_trace_length": args.trace_length,
        },
        "problems": [],
    }


def _load_document(args):
    changed = False
    if args.output.exists() and not args.overwrite:
        document = json.loads(args.output.read_text())
        if document.get("format_version") != CURRENT_FORMAT_VERSION:
            raise SystemExit(
                "cannot resume: unsupported result format; use a format-"
                f"{CURRENT_FORMAT_VERSION} file or --overwrite"
            )
        configuration = document.get("configuration", {})
        if configuration.get("scope") != args.scope:
            raise SystemExit("cannot resume: output scope does not match --scope")
        if configuration.get("synthesis_timeout_seconds") != args.timeout:
            raise SystemExit("cannot resume: output timeout does not match --timeout")
        configured_trace_length = configuration.get("temporal_trace_length")
        if configured_trace_length is not None:
            if (
                args.trace_length is not None
                and args.trace_length != configured_trace_length
            ):
                raise SystemExit(
                    "cannot resume: output temporal trace length does not "
                    "match --trace-length"
                )
            args.trace_length = configured_trace_length
        elif args.trace_length is not None:
            configuration["temporal_trace_length"] = args.trace_length
            changed = True
        elif "temporal_trace_length" not in configuration:
            configuration["temporal_trace_length"] = None
            changed = True
        scope_configuration = document.get("scope_study", {}).get(
            "configuration", {}
        )
        if args.scope_study_size is None:
            args.scope_study_size = scope_configuration.get("candidate_count")
        if args.temporal_study_size is None:
            args.temporal_study_size = scope_configuration.get(
                "temporal_candidate_count"
            )
        trace_configuration = document.get("trace_study", {}).get(
            "configuration", {}
        )
        configured_trace_lengths = trace_configuration.get("trace_lengths", [])
        if configured_trace_lengths:
            if args.trace_study_min is None:
                args.trace_study_min = min(configured_trace_lengths)
            if args.trace_study_max is None:
                args.trace_study_max = max(configured_trace_lengths)
        if not args.resume:
            print(f"Resuming existing results in {args.output}.", flush=True)
    else:
        document = _new_document(args)
        changed = True

    # A resumed output may have supplied the trace length omitted on the CLI.
    _configure_study_arguments(args)
    from alloy import requires_trace_length

    _validate_temporal_trace_length(args, requires_trace_length)

    if args.study in {"all", "scope"}:
        scopes = range(args.scope_study_min, args.scope_study_max + 1)
        try:
            changed |= ensure_scope_study(
                document,
                args.scope_study_size,
                scopes,
                args.timeout,
                args.trace_length,
                args.temporal_study_size,
            )
        except ValueError as error:
            raise SystemExit(str(error)) from error
        trace_study_values = list(_trace_study_values(args))
        if trace_study_values:
            try:
                changed |= ensure_trace_study(
                    document,
                    args.temporal_study_size,
                    trace_study_values,
                    args.timeout,
                    args.trace_length,
                )
            except ValueError as error:
                raise SystemExit(str(error)) from error
    if args.study in {"all", "online"}:
        try:
            changed |= ensure_online_comparison(
                document, args.online_timeout, args.trace_length
            )
        except ValueError as error:
            raise SystemExit(str(error)) from error

    if changed:
        document["format_version"] = CURRENT_FORMAT_VERSION
        save_results(args.output, document)
    return document


def _failed_result(algorithm, predicates, error, synthesis_timeout_seconds):
    return {
        "algorithm": algorithm,
        "status": "error",
        "error": f"{type(error).__name__}: {error}",
        "synthesis_timeout_seconds": synthesis_timeout_seconds,
        "classifications": {predicate: None for predicate in predicates},
        "classification_stats": None,
        "completed_oracles": 0,
        "total_oracles": len(predicates),
    }


def run_main_study(args, document, parse):
    paths = _main_paths(args)
    existing_by_file = {
        problem["file"]: problem for problem in document["problems"]
    }
    required_keys = set(ALGORITHMS)
    pending = [
        path
        for path in paths
        if path.name not in existing_by_file
        or not required_keys.issubset(
            existing_by_file[path.name].get("algorithms", {})
        )
    ]
    print(
        f"Main comparison at scope {args.scope}: {len(pending)} problems "
        f"pending; {args.timeout:g}s synthesis timeout.",
        flush=True,
    )
    for index, path in enumerate(pending, 1):
        problem_start = timer()
        collector = parse(path.read_text(), trace_length=args.trace_length)
        predicates = list(collector.predicates)
        problem = existing_by_file.get(path.name)
        if problem is None:
            problem = _problem_metadata(path, predicates, collector)
            problem["algorithms"] = {}
            document["problems"].append(problem)
            existing_by_file[path.name] = problem
        missing_count = sum(
            algorithm not in problem["algorithms"] for algorithm in ALGORITHMS
        )
        print(
            f"[main {index}/{len(pending)}] {path.name} "
            f"({len(predicates)} candidates; {missing_count} methods pending)",
            flush=True,
        )
        for algorithm in ALGORITHMS:
            if algorithm in problem["algorithms"]:
                continue
            try:
                result = evaluate_batch(
                    collector,
                    path,
                    algorithm,
                    args.scope,
                    args.timeout,
                    args.trace_length,
                )
            except Exception as error:
                result = _failed_result(
                    algorithm, predicates, error, args.timeout
                )
            problem["algorithms"][algorithm] = result
            print_algorithm_result(algorithm, result)
        document["summary_by_candidate_count"] = grouped_summary(
            document["problems"]
        )
        save_results(args.output, document)
        print(
            f"  finished in {timer() - problem_start:.2f} seconds; "
            f"saved {args.output}",
            flush=True,
        )


def run_scope_study(args, document, parse):
    from alloy import requires_trace_length

    ensure_scope_study(
        document,
        args.scope_study_size,
        range(args.scope_study_min, args.scope_study_max + 1),
        args.timeout,
        args.trace_length,
        args.temporal_study_size,
    )
    study = document["scope_study"]
    study_by_file = {
        problem["file"]: problem for problem in study.get("problems", [])
    }
    paths = _scope_study_paths(args)
    scopes = study["configuration"]["scopes"]
    static_algorithms = study["configuration"]["algorithms"]
    temporal_algorithms = study["configuration"]["temporal_algorithms"]

    def required_algorithms(path):
        return (
            temporal_algorithms
            if requires_trace_length(path.read_text())
            else static_algorithms
        )

    pending_tasks = [
        (path, scope)
        for path in paths
        for scope in scopes
        if path.name not in study_by_file
        or not set(required_algorithms(path)).issubset(
            study_by_file[path.name]
            .get("scopes", {})
            .get(str(scope), {})
        )
    ]
    print(
        f"Scope sensitivity study for static n={args.scope_study_size}, temporal "
        f"n={args.temporal_study_size}, scopes "
        f"{scopes[0]}--{scopes[-1]}: {len(pending_tasks)} problem/scope "
        f"combinations pending; scope-{args.scope} main results are reused. "
        f"Temporal trace length is fixed at {args.trace_length}.",
        flush=True,
    )
    for index, (path, scope) in enumerate(pending_tasks, 1):
        task_start = timer()
        collector = parse(path.read_text(), trace_length=args.trace_length)
        predicates = list(collector.predicates)
        problem = study_by_file.get(path.name)
        if problem is None:
            metadata = _problem_metadata(path, predicates, collector)
            problem = _scope_study_problem(metadata)
            study["problems"].append(problem)
            study_by_file[path.name] = problem
        scope_results = problem["scopes"].setdefault(str(scope), {})
        required_keys = (
            temporal_algorithms if collector.temporal else static_algorithms
        )
        missing = [key for key in required_keys if key not in scope_results]
        print(
            f"[scope {index}/{len(pending_tasks)}] {path.name}, scope {scope} "
            f"({len(missing)} methods pending)",
            flush=True,
        )
        for algorithm in required_keys:
            if algorithm in scope_results:
                continue
            try:
                result = evaluate_batch(
                    collector,
                    path,
                    algorithm,
                    scope,
                    args.timeout,
                    args.trace_length,
                )
            except Exception as error:
                result = _failed_result(
                    algorithm, predicates, error, args.timeout
                )
                if collector.temporal:
                    result["trace_length"] = collector.trace_length
            scope_results[algorithm] = result
            print_algorithm_result(algorithm, result)
        study["summary"] = scope_study_summary(study)
        save_results(args.output, document)
        print(
            f"  finished in {timer() - task_start:.2f} seconds; "
            f"saved {args.output}",
            flush=True,
        )


def run_trace_study(args, document, parse):
    """Vary temporal trace length while holding structural scope fixed."""

    trace_lengths = list(_trace_study_values(args))
    ensure_trace_study(
        document,
        args.temporal_study_size,
        trace_lengths,
        args.timeout,
        args.trace_length,
    )
    study = document["trace_study"]
    study_by_file = {
        problem["file"]: problem for problem in study.get("problems", [])
    }
    reused_base_result = False

    # If the main study was not run, reuse the base point just computed by the
    # structural scope sweep instead of synthesizing (scope, trace) twice.
    if args.trace_length in trace_lengths:
        for scope_problem in document.get("scope_study", {}).get("problems", []):
            if (
                not scope_problem.get("temporal")
                or scope_problem.get("candidate_count")
                != args.temporal_study_size
            ):
                continue
            source = scope_problem.get("scopes", {}).get(str(args.scope), {})
            if not source:
                continue
            problem = study_by_file.get(scope_problem["file"])
            if problem is None:
                problem = _trace_study_problem(scope_problem)
                study["problems"].append(problem)
                study_by_file[scope_problem["file"]] = problem
                reused_base_result = True
            target = problem["trace_lengths"].setdefault(
                str(args.trace_length), {}
            )
            for algorithm in TRACE_STUDY_ALGORITHMS:
                if algorithm in source and algorithm not in target:
                    target[algorithm] = deepcopy(source[algorithm])
                    reused_base_result = True

    if reused_base_result:
        study["summary"] = trace_study_summary(study)
        save_results(args.output, document)

    paths = _trace_study_paths(args)
    required_keys = set(study["configuration"]["algorithms"])
    pending_tasks = [
        (path, trace_length)
        for path in paths
        for trace_length in trace_lengths
        if path.name not in study_by_file
        or not required_keys.issubset(
            study_by_file[path.name]
            .get("trace_lengths", {})
            .get(str(trace_length), {})
        )
    ]
    print(
        f"Temporal-depth study for n={args.temporal_study_size}, trace lengths "
        f"{trace_lengths[0]}--{trace_lengths[-1]}: {len(pending_tasks)} "
        f"problem/trace combinations pending; structural scope is fixed at "
        f"{args.scope}.",
        flush=True,
    )
    for index, (path, trace_length) in enumerate(pending_tasks, 1):
        task_start = timer()
        collector = parse(path.read_text(), trace_length=trace_length)
        predicates = list(collector.predicates)
        problem = study_by_file.get(path.name)
        if problem is None:
            metadata = _problem_metadata(path, predicates, collector)
            problem = _trace_study_problem(metadata)
            study["problems"].append(problem)
            study_by_file[path.name] = problem
        trace_results = problem["trace_lengths"].setdefault(
            str(trace_length), {}
        )
        missing = [key for key in required_keys if key not in trace_results]
        print(
            f"[trace {index}/{len(pending_tasks)}] {path.name}, trace length "
            f"{trace_length} ({len(missing)} methods pending)",
            flush=True,
        )
        for algorithm in TRACE_STUDY_ALGORITHMS:
            if algorithm in trace_results:
                continue
            try:
                result = evaluate_batch(
                    collector,
                    path,
                    algorithm,
                    args.scope,
                    args.timeout,
                    trace_length,
                )
            except Exception as error:
                result = _failed_result(
                    algorithm, predicates, error, args.timeout
                )
                result["trace_length"] = trace_length
            trace_results[algorithm] = result
            print_algorithm_result(algorithm, result)
        study["summary"] = trace_study_summary(study)
        save_results(args.output, document)
        print(
            f"  finished in {timer() - task_start:.2f} seconds; "
            f"saved {args.output}",
            flush=True,
        )


def run_online_study(args, document):
    """Evaluate online balanced path costs for batch-completed configurations."""

    ensure_online_comparison(
        document, args.online_timeout, args.trace_length
    )
    study = document["online_comparison"]
    selected_paths = {path.name: path for path in _main_paths(args)}
    eligible = [
        problem
        for problem in document.get("problems", [])
        if problem["file"] in selected_paths
        and problem.get("algorithms", {}).get("balanced-split", {}).get("status")
        == "completed"
    ]
    existing = {
        result["file"]: result for result in study.get("problems", [])
    }
    pending = [
        problem for problem in eligible if problem["file"] not in existing
    ]
    print(
        "Adaptive iterative classification comparison: "
        f"{len(pending)} pending of {len(eligible)} eligible; "
        f"{args.online_timeout:g}s safety timeout.",
        flush=True,
    )
    for index, problem in enumerate(pending, 1):
        result = _run_online_problem(
            selected_paths[problem["file"]],
            document["configuration"]["scope"],
            args.online_timeout,
            args.trace_length,
        )
        result["file"] = problem["file"]
        result["candidate_count"] = problem["candidate_count"]
        study["problems"].append(result)
        study["summary"] = online_comparison_summary(document)
        save_results(args.output, document)
        detail = ""
        if result["status"] == "completed":
            detail = (
                "; mean path "
                f"{statistics.mean(result['path_synthesis_seconds'].values()):.2f}s"
            )
        print(
            f"[online {index}/{len(pending)}] {problem['file']}: "
            f"{result['status']}{detail}",
            flush=True,
        )
    summary = online_comparison_summary(document)
    if study.get("summary") != summary:
        study["summary"] = summary
        save_results(args.output, document)


def print_main_summary(document):
    print("\nMain summary by candidate count", flush=True)
    for key, sizes in document.get("summary_by_candidate_count", {}).items():
        print(key, flush=True)
        for size in sorted(sizes, key=int):
            row = sizes[size]
            suite = ""
            if row.get("test_suite_size_stats"):
                suite = f"; suite mean {row['test_suite_size_stats']['mean']:.2f}"
            timing = ""
            if row.get("synthesis_path_seconds_stats"):
                timing = (
                    "; mean oracle-path synthesis "
                    f"{row['synthesis_path_seconds_stats']['mean']:.2f} seconds"
                )
            elif row.get("synthesis_seconds_stats"):
                timing = (
                    "; mean synthesis "
                    f"{row['synthesis_seconds_stats']['mean']:.2f} seconds"
                )
            if row.get("separation_patterns_stats"):
                timing += (
                    "; separation patterns/SAT calls mean "
                    f"{row['separation_patterns_stats']['mean']:.2f}/"
                    f"{row.get('enumeration_solver_calls_stats', {}).get('mean', float('nan')):.2f}; "
                    "enumeration/cover mean "
                    f"{row['enumeration_seconds_stats']['mean']:.2f}/"
                    f"{row['cover_seconds_stats']['mean']:.2f} seconds"
                )
            print(
                f"  n={size}: {row['completed_oracles']}/{row['total_oracles']} "
                f"oracles; classifications {_format_stats(row['classification_stats'])}"
                f"{suite}{timing}",
                flush=True,
            )


def print_scope_summary(document):
    study = document.get("scope_study")
    if not study:
        return
    print("\nRQ2 scope-study summary", flush=True)
    for key, scopes in study.get("summary", {}).get("by_scope", {}).items():
        print(key, flush=True)
        for scope in sorted(scopes, key=int):
            row = scopes[scope]
            suite_stats = row.get("test_suite_size_stats")
            suite = "NA" if suite_stats is None else f"{suite_stats['mean']:.2f}"
            print(
                f"  scope={scope}: {row.get('synthesis_completed_problems', row['completed_problems'])}/{row['problems']} "
                f"synthesized batches; {row.get('post_synthesis_errors', 0)} post-synthesis errors; "
                f"validated suite mean {suite}; classifications "
                f"{_format_stats(row.get('classification_stats'))}",
                flush=True,
            )
    paired = study.get("summary", {}).get(
        "paired_joint_cover_completed_all_scopes", {}
    )
    print(
        "  Joint Cover paired subset completed at every scope: "
        f"{paired.get('problem_count', 0)} problems",
        flush=True,
    )


def print_trace_summary(document):
    study = document.get("trace_study")
    if not study:
        return
    print("\nTemporal trace-length-study summary", flush=True)
    for key, trace_lengths in study.get("summary", {}).get(
        "by_trace_length", {}
    ).items():
        print(key, flush=True)
        for trace_length in sorted(trace_lengths, key=int):
            row = trace_lengths[trace_length]
            suite_stats = row.get("test_suite_size_stats")
            suite = "NA" if suite_stats is None else f"{suite_stats['mean']:.2f}"
            print(
                f"  trace={trace_length}: "
                f"{row.get('synthesis_completed_problems', row['completed_problems'])}/{row['problems']} synthesized batches; "
                f"{row.get('post_synthesis_errors', 0)} post-synthesis errors; "
                f"validated suite mean {suite}; classifications "
                f"{_format_stats(row.get('classification_stats'))}",
                flush=True,
            )


def print_online_summary(document):
    study = document.get("online_comparison")
    if not study:
        return
    summary = study.get("summary", {})
    completed = summary.get("completed_configurations", 0)
    print("\nAdaptive iterative classification comparison", flush=True)
    if not completed:
        print("  no completed configurations", flush=True)
        return
    if not summary.get("timed_configurations"):
        print("  no configurations with recorded batch synthesis time", flush=True)
        return
    batch = summary["batch_preparation_seconds"]["median"]
    online = summary["online_mean_path_synthesis_seconds"][
        "median_across_configurations"
    ]
    print(
        f"  {summary['timed_configurations']} configurations; median batch/iterative path "
        f"{batch:.2f}/{online:.2f} seconds",
        flush=True,
    )


def main(argv=None):
    args = argument_parser().parse_args(argv)
    if args.paper_report or args.full_report:
        report_label = "full" if args.full_report else "paper"
        if not args.output.exists():
            raise SystemExit(f"cannot generate {report_label} report: {args.output} not found")
        try:
            document = json.loads(args.output.read_text())
        except (OSError, json.JSONDecodeError) as error:
            raise SystemExit(
                f"cannot generate {report_label} report from {args.output}: {error}"
            ) from error
        from evaluation_report import print_full_report, print_paper_report

        printer = print_full_report if args.full_report else print_paper_report
        printer(document, source=args.output)
        return 0
    if args.scope_study_min > args.scope_study_max:
        raise SystemExit("--scope-study-min cannot exceed --scope-study-max")
    document = _load_document(args)

    from alloy import parse

    try:
        if args.study in {"all", "main"}:
            run_main_study(args, document, parse)
        if args.study in {"all", "scope"}:
            # Main scope results may have been added immediately above. Seed
            # them into the scope study before looking for missing work.
            if ensure_scope_study(
                document,
                args.scope_study_size,
                range(args.scope_study_min, args.scope_study_max + 1),
                args.timeout,
                args.trace_length,
                args.temporal_study_size,
            ):
                save_results(args.output, document)
            run_scope_study(args, document, parse)
            if args.trace_length is not None:
                if ensure_trace_study(
                    document,
                    args.temporal_study_size,
                    _trace_study_values(args),
                    args.timeout,
                    args.trace_length,
                ):
                    save_results(args.output, document)
            run_trace_study(args, document, parse)
        if args.study in {"all", "online"}:
            run_online_study(args, document)
    except KeyboardInterrupt:
        print("\nInterrupted; completed work has already been saved.", flush=True)
        return 130

    if args.study in {"all", "main"}:
        print_main_summary(document)
    if args.study in {"all", "scope"}:
        print_scope_summary(document)
        print_trace_summary(document)
    if args.study in {"all", "online"}:
        print_online_summary(document)
    return 0


if __name__ == "__main__":
    if len(sys.argv) >= 2 and sys.argv[1] == "_worker":
        raise SystemExit(
            _worker_server(
                sys.argv[2],
                sys.argv[3],
                int(sys.argv[4]),
                _parse_trace_length_argument(sys.argv[5]),
            )
        )
    if len(sys.argv) == 5 and sys.argv[1] == "_online_worker":
        raise SystemExit(
            _online_worker(
                sys.argv[2],
                int(sys.argv[3]),
                _parse_trace_length_argument(sys.argv[4]),
            )
        )
    raise SystemExit(main())