Run model checker in 1ES GHA pool (#5707)

.github/workflows/tlaplus.yml

@@ -12,30 +12,35 @@ on:
 jobs:
   model-checking:
     name: Model Checking
-    runs-on: ubuntu-latest
+    runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub]
+    container:
+      image: ccfmsrc.azurecr.io/ccf/ci:05-09-2023-virtual-clang15
 
     steps:
       - uses: actions/checkout@v3
-      - run: python ./tla/install_deps.py
+      - run: |
+          sudo apt update
+          sudo apt install -y default-jre
+          python3 ./tla/install_deps.py
 
       - name: MCccfraft.cfg
         run: |
-          set -exo pipefail
           cd tla/
-          ./tlc.sh -workers auto MCccfraft.tla 2>&1 | tee MCccfraft.out
+          ./tlc.sh -workers auto MCccfraft.tla -dumpTrace tla MCccfraft.trace.tla -dumpTrace json MCccfraft.json
 
       - name: MCccfraftWithReconfig.cfg
         run: |
-          set -exo pipefail
           cd tla/
-          ./tlc.sh -workers auto -config MCccfraftWithReconfig.cfg MCccfraft.tla 2>&1 | tee MCccfraftWithReconfig.out
+          ./tlc.sh -workers auto -config MCccfraftWithReconfig.cfg MCccfraft.tla -dumpTrace tla MCccfraftWithReconfig.trace.tla -dumpTrace json MCccfraftWithReconfig.json
 
-      - name: Upload TLC's out file as an artifact. Can be imported into the TLA+ Toolbox.
-        uses: actions/upload-artifact@v2
+      - name: Upload traces in TLA and JSON format
+        uses: actions/upload-artifact@v3
         if: ${{ failure() }}
         with:
           name: tlc
-          path: tla/*.out
+          path: |
+            tla/*.trace.tla
+            tla/*.json
 
   simulation:
     name: Simulation
@@ -43,17 +48,18 @@ jobs:
 
     steps:
       - uses: actions/checkout@v3
-      - run: python ./tla/install_deps.py
+      - run: python3 ./tla/install_deps.py
 
       - name: SIMccfraft.tla
         run: |
-          set -exo pipefail
           cd tla/
-          ./tlc.sh -workers auto -simulate -depth 500 SIMccfraft.tla 2>&1 | tee SIMccfraft.out
+          ./tlc.sh -workers auto -simulate -depth 500 SIMccfraft.tla -dumpTrace tla SIMccfraft.trace.tla -dumpTrace json SIMccfraft.json
 
-      - name: Upload TLC's out file as an artifact. Can be imported into the TLA+ Toolbox.
-        uses: actions/upload-artifact@v2
+      - name: Upload traces in TLA and JSON format
+        uses: actions/upload-artifact@v3
         if: ${{ failure() }}
         with:
           name: tlc
-          path: tla/*.out
+          path: |
+            tla/*.trace.tla
+            tla/*.json

tla/install_deps.py

@@ -9,27 +9,24 @@ import subprocess
 import tarfile
 
 TLA_DIR = os.path.dirname(os.path.realpath(__file__))
-HOME_DIR = os.path.expanduser('~')
+HOME_DIR = os.path.expanduser("~")
 
 
 def append_bashrc(line: str):
-
     bashrc_path = f"{HOME_DIR}/.bashrc"
-    with open(bashrc_path, "r+", encoding="utf-8") as bashrc_file:
+    with open(bashrc_path, "a+", encoding="utf-8") as bashrc_file:
+        bashrc_file.seek(0)
         bashrc_lines = bashrc_file.readlines()
         if line not in bashrc_lines:
-            if not bashrc_lines[-1].endswith("\n"):
-                bashrc_file.write("\n")
+            bashrc_file.write("\n")
             bashrc_file.writelines(line)
 
 
 def set_alias(key: str, value: str):
-
     append_bashrc(f"alias {key}='{value}'\n")
 
 
 def fetch_latest(url: str, dest: str = "."):
-
     subprocess.Popen(f"wget -N {url} -P /tmp".split()).wait()
     file_name = url.split("/")[-1]
     file_path = f"/tmp/{file_name}"
@@ -45,7 +42,8 @@ def fetch_latest(url: str, dest: str = "."):
         with tarfile.open(f"/tmp/{file_name}") as tar:
             tar.extractall(dest)
             rel_bin_path = next(
-                member.name for member in tar.getmembers() if "bin" in member.name)
+                member.name for member in tar.getmembers() if "bin" in member.name
+            )
             bin_path = os.path.join(dest, rel_bin_path)
 
     elif file_name.endswith(".jar"):
@@ -56,7 +54,6 @@ def fetch_latest(url: str, dest: str = "."):
 
 
 def _parse_args() -> argparse.Namespace:
-
     parser = argparse.ArgumentParser(
         description="Install CCF TLA+ dependencies",
     )
@@ -74,17 +71,13 @@ def _parse_args() -> argparse.Namespace:
     )
 
     parser.add_argument(
-        "--skip-apt-packages",
-        action="store_false",
-        default=True,
-        dest="apt_packages"
+        "--skip-apt-packages", action="store_false", default=True, dest="apt_packages"
     )
 
     return parser.parse_args()
 
 
 def install_tlc():
-
     java = "java"
     tlaplus_path = "~/.vscode-remote/extensions/alygin.vscode-tlaplus-nightly-*/tools/tla2tools.jar"
     copy_tlaplus = f"-cp {tlaplus_path} tlc2.TLC"
@@ -94,9 +87,9 @@ def install_tlc():
 
 
 def install_deps(args: argparse.Namespace):
-
     # Setup tools directory
     tools_dir = os.path.join(TLA_DIR, "tools")
+
     def create_tools_dir():
         if not os.path.exists(tools_dir):
             os.mkdir(tools_dir)
@@ -119,7 +112,8 @@ def install_deps(args: argparse.Namespace):
 
     if args.apt_packages:
         subprocess.Popen(
-            "sudo apt-get install -y --no-install-recommends".split() + [
+            "sudo apt-get install -y --no-install-recommends".split()
+            + [
                 "wget",
                 "graphviz",
                 "htop",