From 099170388754816664f9f455ddfc8b569fc31601 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sat, 27 Dec 2025 02:50:16 +0000 Subject: [PATCH] Address code review: remove unused imports and add documentation Co-authored-by: johndoe6345789 <224850594+johndoe6345789@users.noreply.github.com> --- scripts/tlaplus.py | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/scripts/tlaplus.py b/scripts/tlaplus.py index fb6dc78..8ff5699 100755 --- a/scripts/tlaplus.py +++ b/scripts/tlaplus.py @@ -9,12 +9,9 @@ The TLC model checker verifies invariants and temporal properties of the WizardMerge merge algorithm specification. """ -import os import sys import subprocess import urllib.request -import zipfile -import shutil from pathlib import Path @@ -100,7 +97,14 @@ def parse_spec(jar_path: Path, spec_dir: Path, spec_name: str, output_dir: Path) def run_tlc(jar_path: Path, spec_dir: Path, spec_name: str, output_dir: Path) -> int: - """Run TLC model checker on the specification.""" + """ + Run TLC model checker on the specification. + + Note: This function is currently not used in the main workflow because + WizardMergeSpec is a parametric specification requiring concrete constant + values. It's kept for future use when test harness modules with specific + instantiations are added. + """ spec_file = spec_dir / f"{spec_name}.tla" cfg_file = spec_dir / f"{spec_name}.cfg"