Create tlaplus.py

scripts/tlaplus.py

@@ -0,0 +1,286 @@
+#!/usr/bin/env python3
+"""
+Unified TLC helper: replaces bootstrap.{sh,ps1} and run-tlc.{sh,ps1}.
+
+Subcommands:
+  - bootstrap : download tla2tools.jar into tools/ (or custom dir)
+  - run       : ensure jar exists, then run TLC and tee output to log
+"""
+
+from __future__ import annotations
+
+import argparse
+import shutil
+import subprocess
+import sys
+from pathlib import Path
+from typing import Iterable, List
+from urllib.request import urlopen
+
+
+DEFAULT_VERSION = "1.8.0"
+DEFAULT_TOOLS_DIR = "tools"
+DEFAULT_RESULTS_DIR = "ci-results"
+DEFAULT_MODULE = "STLRepairAlgo"
+DEFAULT_CONFIG = "models/STLRepairAlgo.cfg"
+DEFAULT_SPEC_DIR = "spec"
+DEFAULT_JAVA = "java"
+
+
+def parse_args() -> argparse.Namespace:
+    parser = argparse.ArgumentParser(
+        description="TLA+ TLC helper (bootstrap + run) in one script."
+    )
+
+    parser.add_argument(
+        "--tools-dir",
+        default=DEFAULT_TOOLS_DIR,
+        help=f"Directory for tla2tools.jar (default: {DEFAULT_TOOLS_DIR!r}).",
+    )
+
+    parser.add_argument(
+        "--version",
+        default=DEFAULT_VERSION,
+        help=f"TLA+ tools version tag (default: {DEFAULT_VERSION!r}).",
+    )
+
+    parser.add_argument(
+        "--url-template",
+        default=(
+            "https://github.com/tlaplus/tlaplus/releases/"
+            "download/v{version}/tla2tools.jar"
+        ),
+        help="Template URL for tla2tools.jar; {version} will be substituted.",
+    )
+
+    subparsers = parser.add_subparsers(
+        dest="command",
+        required=True,
+        help="Subcommands.",
+    )
+
+    bootstrap = subparsers.add_parser(
+        "bootstrap",
+        help="Download tla2tools.jar into tools-dir if missing.",
+    )
+
+    bootstrap.add_argument(
+        "--force",
+        action="store_true",
+        help="Re-download even if tla2tools.jar already exists.",
+    )
+
+    run_p = subparsers.add_parser(
+        "run",
+        help="Run TLC on a TLA+ module, teeing output to a log file.",
+    )
+
+    run_p.add_argument(
+        "module",
+        nargs="?",
+        default=DEFAULT_MODULE,
+        help=f"TLA+ module name without .tla (default: {DEFAULT_MODULE!r}).",
+    )
+
+    run_p.add_argument(
+        "-c",
+        "--config",
+        default=DEFAULT_CONFIG,
+        help=f"Path to TLC config file (default: {DEFAULT_CONFIG!r}).",
+    )
+
+    run_p.add_argument(
+        "--spec-dir",
+        default=DEFAULT_SPEC_DIR,
+        help=f"Directory containing .tla specs (default: {DEFAULT_SPEC_DIR!r}).",
+    )
+
+    run_p.add_argument(
+        "--results-dir",
+        default=DEFAULT_RESULTS_DIR,
+        help=f"Directory for TLC log files (default: {DEFAULT_RESULTS_DIR!r}).",
+    )
+
+    run_p.add_argument(
+        "--java",
+        default=DEFAULT_JAVA,
+        help=f"Java executable (default: {DEFAULT_JAVA!r}).",
+    )
+
+    run_p.add_argument(
+        "--extra-java-arg",
+        action="append",
+        default=[],
+        metavar="ARG",
+        help="Extra argument to pass to Java (can be repeated).",
+    )
+
+    run_p.add_argument(
+        "--no-bootstrap",
+        action="store_true",
+        help="Skip automatic bootstrap before running TLC.",
+    )
+
+    return parser.parse_args()
+
+
+def ensure_dir(path: Path) -> None:
+    path.mkdir(parents=True, exist_ok=True)
+
+
+def build_jar_url(version: str, url_template: str) -> str:
+    return url_template.format(version=version)
+
+
+def download_tla_tools(url: str, target: Path, overwrite: bool = False) -> None:
+    if target.exists() and not overwrite:
+        print(f"tla2tools.jar already present at {target}.")
+        return
+
+    ensure_dir(target.parent)
+    tmp = target.with_suffix(target.suffix + ".tmp")
+
+    print(f"Downloading tla2tools.jar from {url} ...")
+    try:
+        with urlopen(url) as resp, tmp.open("wb") as f:
+            chunk = resp.read(8192)
+            while chunk:
+                f.write(chunk)
+                chunk = resp.read(8192)
+    except Exception as exc:
+        if tmp.exists():
+            tmp.unlink()
+        raise SystemExit(f"Failed to download tla2tools.jar: {exc}") from exc
+
+    tmp.replace(target)
+    target.chmod(0o644)
+    print(f"Saved tla2tools.jar to {target}.")
+
+
+def ensure_java_available(java_exe: str) -> None:
+    if shutil.which(java_exe) is None:
+        raise SystemExit(
+            f"Java executable {java_exe!r} not found in PATH. "
+            "Install Java or pass --java with a full path."
+        )
+
+
+def tee_process_output(
+    proc: subprocess.Popen,
+    log_path: Path,
+) -> int:
+    ensure_dir(log_path.parent)
+    with log_path.open("w", encoding="utf-8", errors="replace") as log:
+        assert proc.stdout is not None
+        for line in proc.stdout:
+            sys.stdout.write(line)
+            sys.stdout.flush()
+            log.write(line)
+            log.flush()
+    return proc.wait()
+
+
+def build_tlc_command(
+    java_exe: str,
+    extra_java_args: Iterable[str],
+    jar_path: Path,
+    cfg_path: Path,
+    module_path: Path,
+) -> List[str]:
+    cmd: List[str] = [java_exe]
+    cmd.extend(extra_java_args)
+    cmd.extend(
+        [
+            "-cp",
+            str(jar_path),
+            "tlc2.TLC",
+            "-config",
+            str(cfg_path),
+            str(module_path),
+        ]
+    )
+    return cmd
+
+
+def run_tlc(
+    java_exe: str,
+    extra_java_args: Iterable[str],
+    tools_dir: Path,
+    spec_dir: Path,
+    module: str,
+    cfg: Path,
+    results_dir: Path,
+) -> int:
+    ensure_java_available(java_exe)
+
+    jar_path = tools_dir / "tla2tools.jar"
+    if not jar_path.exists():
+        raise SystemExit(
+            f"{jar_path} does not exist. Run with 'bootstrap' first "
+            "or omit --no-bootstrap on the 'run' command."
+        )
+
+    module_path = spec_dir / f"{module}.tla"
+    if not module_path.exists():
+        raise SystemExit(f"Spec file not found: {module_path}")
+
+    cfg_path = cfg
+    if not cfg_path.exists():
+        raise SystemExit(f"Config file not found: {cfg_path}")
+
+    ensure_dir(results_dir)
+    log_path = results_dir / f"{module}.tlc.log"
+
+    cmd = build_tlc_command(
+        java_exe=java_exe,
+        extra_java_args=list(extra_java_args),
+        jar_path=jar_path,
+        cfg_path=cfg_path,
+        module_path=module_path,
+    )
+
+    print("Running TLC with command:")
+    print("  " + " ".join(str(c) for c in cmd))
+    print(f"Logging output to {log_path}")
+
+    proc = subprocess.Popen(
+        cmd,
+        stdout=subprocess.PIPE,
+        stderr=subprocess.STDOUT,
+        text=True,
+        bufsize=1,
+        universal_newlines=True,
+    )
+    return tee_process_output(proc, log_path)
+
+
+def main() -> None:
+    args = parse_args()
+    tools_dir = Path(args.tools_dir)
+    url = build_jar_url(args.version, args.url_template)
+    jar_target = tools_dir / "tla2tools.jar"
+
+    if args.command == "bootstrap":
+        download_tla_tools(url, jar_target, overwrite=args.force)
+        return
+
+    if args.command == "run":
+        if not args.no_bootstrap:
+            download_tla_tools(url, jar_target, overwrite=False)
+
+        exit_code = run_tlc(
+            java_exe=args.java,
+            extra_java_args=args.extra_java_arg,
+            tools_dir=tools_dir,
+            spec_dir=Path(args.spec_dir),
+            module=args.module,
+            cfg=Path(args.config),
+            results_dir=Path(args.results_dir),
+        )
+        raise SystemExit(exit_code)
+
+    raise SystemExit("No command given; use --help for usage.")
+
+
+if __name__ == "__main__":
+    main()