From 4a9fd4d6e63f94026fe03d398b7136a04244623d Mon Sep 17 00:00:00 2001 From: JohnDoe6345789 Date: Thu, 27 Nov 2025 19:56:56 +0000 Subject: [PATCH] Create tlaplus.py --- scripts/tlaplus.py | 286 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 286 insertions(+) create mode 100644 scripts/tlaplus.py diff --git a/scripts/tlaplus.py b/scripts/tlaplus.py new file mode 100644 index 0000000..7985e04 --- /dev/null +++ b/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()