Run validation test suite against latest tla2tools.jar.

Author: lemmy

.github/workflows/main.yml

@@ -26,6 +26,10 @@ jobs:
         with:
           distribution: adopt
           java-version: 17
+      - name: Get (nightly) TLC
+        run: |
+            mkdir -p tools/1.8.0
+            wget https://nightly.tlapl.us/dist/tla2tools.jar -O tools/1.8.0/tla2tools.jar
       - name: Install testgen dependencies
         run: pip install -r requirements.txt
       - name: Configure App armor profile to allow testgen to use bubblewrap ## https://github.com/DevToys-app/DevToys/issues/1198#issuecomment-2985517203
@@ -43,7 +47,7 @@ jobs:
         with:
           switches: -avzr --delete
           path: reports/
-          remote_path: validation-test-suite/1.7.2/
+          remote_path: validation-test-suite/1.8.0/
           remote_host: upload.tlapl.us
           remote_user: github
           remote_key: ${{ secrets.INRIA_SSH_PRIVKEY }}

testgen/runner.py

@@ -66,7 +66,7 @@
 def setup():
     global tlc_jar, apalache_jar, tmp_dir, jacoco_jar
     working_dir = os.getcwd()
-    tlc_jar = os.path.join(working_dir, 'tools', '1.7.2', 'tla2tools.jar')
+    tlc_jar = os.path.join(working_dir, 'tools', '1.8.0', 'tla2tools.jar')
     apalache_jar = os.path.join(working_dir, 'tools', 'apalache-0.28.0.jar')
     jacoco_jar = os.path.join(working_dir, 'tools', 'jacoco-0.8.8', 'jacocoagent.jar')
 

tools/coverage_report.sh

@@ -28,7 +28,7 @@ SOURCES="
 java \
     -jar ${TOOL_DIR}/jacoco-0.8.8/jacococli.jar \
     report $1 \
-    --classfiles ${TOOL_DIR}/1.7.2/tla2tools.jar \
+    --classfiles ${TOOL_DIR}/1.8.0/tla2tools.jar \
     --html $1.report \
     --name the-report \
     ${SOURCES}