Test PlusCal translation in CI

.github/scripts/translate_pluscal.py

@@ -0,0 +1,70 @@
+"""
+Runs PlusCal translation on all PlusCal specs.
+"""
+
+from argparse import ArgumentParser
+from concurrent.futures import ThreadPoolExecutor
+import logging
+from os import cpu_count
+from os.path import dirname, normpath
+import subprocess
+from subprocess import CompletedProcess
+import tla_utils
+
+parser = ArgumentParser(description='Run PlusCal translation on all modules.')
+parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=True)
+parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True)
+parser.add_argument('--skip', nargs='+', help='Space-separated list of .tla modules to skip converting', required=False, default=[])
+parser.add_argument('--only', nargs='+', help='If provided, only convert models in this space-separated list', required=False, default=[])
+parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true')
+args = parser.parse_args()
+
+logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO)
+
+tools_path = normpath(args.tools_jar_path)
+manifest_path = normpath(args.manifest_path)
+examples_root = dirname(manifest_path)
+skip_modules = [normpath(path) for path in args.skip]
+only_modules = [normpath(path) for path in args.only]
+
+manifest = tla_utils.load_json(manifest_path)
+
+# List of all modules to translate
+modules = [
+    tla_utils.from_cwd(examples_root, module['path'])
+    for spec in manifest['specifications']
+    for module in spec['modules']
+        if 'pluscal' in module['features']
+        and normpath(module['path']) not in skip_modules
+        and (only_modules == [] or normpath(module['path']) in only_modules)
+]
+
+for path in skip_modules:
+    logging.info(f'Skipping {path}')
+
+def translate_module(module_path):
+    logging.info(f'Translating {module_path}')
+    result = subprocess.run(
+        ['java', '-cp', tools_path, 'pcal.trans', '-nocfg', module_path],
+        stdout=subprocess.PIPE,
+        stderr=subprocess.STDOUT,
+        text=True
+    )
+    match result:
+        case CompletedProcess():
+            if result.returncode == 0:
+                return True
+            else:
+                logging.error(f'Module {module_path} conversion failed with return code {result.returncode}; output:\n{result.stdout}')
+                return False
+        case _:
+            logging.error(f'Unhandled result type {type(result)}: {result.stdout}')
+            return False
+
+success = True
+thread_count = cpu_count() if not args.verbose else 1
+logging.info(f'Translating PlusCal using {thread_count} threads')
+with ThreadPoolExecutor(thread_count) as executor:
+    results = executor.map(translate_module, modules)
+    exit(0 if all(results) else 1)
+

.github/scripts/unicode_conversion.py

@@ -60,6 +60,7 @@ def convert_module(module_path):
                 return False
         case _:
             logging.error(f'Unhandled TLAUC result type {type(result)}: {result.stdout}')
+            return False
 
 success = True
 thread_count = cpu_count() if not args.verbose else 1

.github/workflows/CI.yml

@@ -45,23 +45,23 @@ jobs:
         run: $SCRIPT_DIR/linux-setup.sh $SCRIPT_DIR $DEPS_DIR false
       - name: Check manifest.json format
         run: |
-          python $SCRIPT_DIR/check_manifest_schema.py \
-            --manifest_path manifest.json             \
+          python "$SCRIPT_DIR/check_manifest_schema.py" \
+            --manifest_path manifest.json               \
             --schema_path manifest-schema.json
       - name: Check manifest files
         run: |
-          python $SCRIPT_DIR/check_manifest_files.py  \
-            --manifest_path manifest.json             \
+          python "$SCRIPT_DIR/check_manifest_files.py"  \
+            --manifest_path manifest.json               \
             --ci_ignore_path .ciignore
       - name: Check manifest feature flags
         run: |
-          python $SCRIPT_DIR/check_manifest_features.py \
-            --manifest_path manifest.json               \
+          python "$SCRIPT_DIR/check_manifest_features.py" \
+            --manifest_path manifest.json                 \
             --ts_path $DEPS_DIR/tree-sitter-tlaplus
       - name: Check README spec table
         run: |
-          python $SCRIPT_DIR/check_markdown_table.py  \
-            --manifest_path manifest.json             \
+          python "$SCRIPT_DIR/check_markdown_table.py"  \
+            --manifest_path manifest.json               \
             --readme_path README.md
       - name: Convert specs to unicode
         if: matrix.unicode
@@ -75,6 +75,31 @@ jobs:
           python "$SCRIPT_DIR/unicode_number_set_shim.py" \
             --ts_path "$DEPS_DIR/tree-sitter-tlaplus"     \
             --manifest_path manifest.json
+      - name: Translate PlusCal
+        if: (!matrix.unicode) # PlusCal does not yet support unicode
+        run: |
+          # https://github.com/tlaplus/tlaplus/issues/906
+          SKIP=(
+            "specifications/byzpaxos/BPConProof.tla"
+            "specifications/byzpaxos/PConProof.tla"
+            "specifications/byzpaxos/VoteProof.tla"
+          )
+          if [[ "${{ matrix.os }}" == "windows-latest" ]]; then
+            # Slush.tla includes unicode characters in comments,
+            # and on Windows the PlusCal translator can't handle
+            # this for some reason.
+            SKIP+=("specifications/SlushProtocol/Slush.tla")
+          fi
+          python $SCRIPT_DIR/translate_pluscal.py           \
+            --tools_jar_path $DEPS_DIR/tools/tla2tools.jar  \
+            --manifest_path manifest.json                   \
+            --skip "${SKIP[@]}"
+          if [[ "${{ matrix.unicode }}" == "false" ]]; then
+            git status
+            git diff
+            diff_count=$(git status --porcelain=v1 2>/dev/null | wc -l)
+            exit $diff_count
+          fi
       - name: Parse all modules
         run: |
           # Need to have a nonempty list to pass as a skip parameter

specifications/DiningPhilosophers/DiningPhilosophers.tla

@@ -113,7 +113,7 @@ Think:
 end process;
 
 end algorithm; *)
-\* BEGIN TRANSLATION (chksum(pcal) = "8d8268d4" /\ chksum(tla) = "16352822")
+\* BEGIN TRANSLATION (chksum(pcal) = "ea877089" /\ chksum(tla) = "16352822")
 VARIABLES forks, pc
 
 (* define statement *)

specifications/LoopInvariance/BinarySearch.tla

@@ -67,9 +67,11 @@ a == /\ pc = "a"
                 /\ UNCHANGED << low, high, result >>
      /\ UNCHANGED << seq, val >>
 
+(* Allow infinite stuttering to prevent deadlock on termination. *)
+Terminating == pc = "Done" /\ UNCHANGED vars
+
 Next == a
-           \/ (* Disjunct to prevent deadlock on termination *)
-              (pc = "Done" /\ UNCHANGED vars)
+           \/ Terminating
 
 Spec == /\ Init /\ [][Next]_vars
         /\ WF_vars(Next)
@@ -245,7 +247,7 @@ THEOREM Spec => []resultCorrect
   <2>2. CASE UNCHANGED vars
     BY <2>2 DEF Inv, TypeOK,  vars
   <2>3. QED
-    BY <2>1,  <2>2 DEF Next
+    BY <2>1,  <2>2 DEF Next, Terminating
 <1>3. Inv => resultCorrect
    BY  DEF resultCorrect, Inv, TypeOK
 <1>4. QED

specifications/LoopInvariance/Quicksort.tla

@@ -152,9 +152,11 @@ a == /\ pc = "a"
                 /\ UNCHANGED << seq, U >>
      /\ seq0' = seq0
 
+(* Allow infinite stuttering to prevent deadlock on termination. *)
+Terminating == pc = "Done" /\ UNCHANGED vars
+
 Next == a
-           \/ (* Disjunct to prevent deadlock on termination *)
-              (pc = "Done" /\ UNCHANGED vars)
+           \/ Terminating
 
 Spec == /\ Init /\ [][Next]_vars
         /\ WF_vars(Next)

specifications/LoopInvariance/SumSequence.tla

@@ -74,9 +74,11 @@ a == /\ pc = "a"
                 /\ UNCHANGED << sum, n >>
      /\ seq' = seq
 
+(* Allow infinite stuttering to prevent deadlock on termination. *)
+Terminating == pc = "Done" /\ UNCHANGED vars
+
 Next == a
-           \/ (* Disjunct to prevent deadlock on termination *)
-              (pc = "Done" /\ UNCHANGED vars)
+           \/ Terminating
 
 Spec == /\ Init /\ [][Next]_vars
         /\ WF_vars(Next)

specifications/MisraReachability/ParReach.tla

@@ -137,9 +137,12 @@ c(self) == /\ pc[self] = "c"
 
 p(self) == a(self) \/ b(self) \/ c(self)
 
+(* Allow infinite stuttering to prevent deadlock on termination. *)
+Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
+               /\ UNCHANGED vars
+
 Next == (\E self \in Procs: p(self))
-           \/ (* Disjunct to prevent deadlock on termination *)
-              ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)
+           \/ Terminating
 
 Spec == /\ Init /\ [][Next]_vars
         /\ \A self \in Procs : WF_vars(p(self))

specifications/MisraReachability/ParReachProofs.tla

@@ -11,7 +11,7 @@ LEMMA TypeInvariant == Spec  => []Inv
 <1>1. Init => Inv
     BY RootAssump DEF Init, Inv, ProcSet  
 <1>2. Inv /\ [Next]_vars => Inv'
-   BY SuccAssump DEF Inv, Next, vars, ProcSet, p, a, b, c
+   BY SuccAssump DEF Inv, Next, Terminating, vars, ProcSet, p, a, b, c
 <1>3. QED
   BY <1>1, <1>2, PTL DEF Spec
 
@@ -23,7 +23,7 @@ THEOREM Spec => R!Init /\ [][R!Next]_R!vars
                       [Next]_vars
                PROVE  [R!Next]_R!vars
     OBVIOUS
-  <2> USE DEF Inv, Next, vars, R!Next, R!vars, vrootBar, pcBar
+  <2> USE DEF Inv, Next, Terminating, vars, R!Next, R!vars, vrootBar, pcBar
   <2>1. ASSUME NEW self \in Procs,
                a(self)
         PROVE  [R!Next]_R!vars
@@ -58,7 +58,7 @@ THEOREM Spec => R!Init /\ [][R!Next]_R!vars
   <2>4. CASE UNCHANGED vars
     BY <2>4
   <2>5. QED
-    BY <2>1, <2>2, <2>3, <2>4 DEF Next, p
+    BY <2>1, <2>2, <2>3, <2>4 DEF Next, Terminating, p
 <1>3. QED
   BY <1>1, <1>2, TypeInvariant, PTL DEF Spec
 

specifications/MisraReachability/Reachable.tla

@@ -81,7 +81,6 @@ node and does the following:
 \* BEGIN TRANSLATION    Here is the TLA+ translation of the PlusCal code.
 VARIABLES marked, vroot, pc
 
-\*Reachable == ReachableFrom(marked)  (* added for a test *)
 vars == << marked, vroot, pc >>
 
 Init == (* Global variables *)
@@ -101,9 +100,11 @@ a == /\ pc = "a"
            ELSE /\ pc' = "Done"
                 /\ UNCHANGED << marked, vroot >>
 
+(* Allow infinite stuttering to prevent deadlock on termination. *)
+Terminating == pc = "Done" /\ UNCHANGED vars
+
 Next == a
-           \/ (* Disjunct to prevent deadlock on termination *)
-              (pc = "Done" /\ UNCHANGED vars)
+           \/ Terminating
 
 Spec == /\ Init /\ [][Next]_vars
         /\ WF_vars(Next)

specifications/MisraReachability/ReachableProofs.tla

@@ -74,7 +74,7 @@ THEOREM Thm1 == Spec => []Inv1
     <2>2. CASE UNCHANGED vars
       BY <2>2 DEF Inv1, TypeOK, vars
     <2>3. QED
-      BY <2>1, <2>2 DEF Next
+      BY <2>1, <2>2 DEF Next, Terminating
   <1>3. QED
     BY <1>1, <1>2, PTL DEF Spec  
 
@@ -189,7 +189,7 @@ THEOREM Thm3 == Spec => []Inv3
       (*********************************************************************)
       BY <2>1, <2>3 DEF Inv3, TypeOK, vars  
     <2>4. QED
-      BY <2>2, <2>3 DEF Next  
+      BY <2>2, <2>3 DEF Next, Terminating
   <1>3. QED
     BY <1>1, <1>2, Thm2, PTL DEF Spec
 

specifications/MultiPaxos-SMR/MultiPaxos.tla

@@ -424,7 +424,7 @@ end algorithm; *)
 
 ----------
 
-\* BEGIN TRANSLATION (chksum(pcal) = "d7327cb9" /\ chksum(tla) = "bfbfd945")
+\* BEGIN TRANSLATION (chksum(pcal) = "2be53042" /\ chksum(tla) = "bfbfd945")
 VARIABLES msgs, node, pending, observed, pc
 
 (* define statement *)

specifications/N-Queens/QueensPluscal.tla

@@ -86,14 +86,16 @@ nxtQ == /\ pc = "nxtQ"
                                  THEN /\ todo' = todo \ {queens}
                                       /\ sols' = (sols \union exts)
                                  ELSE /\ todo' = ((todo \ {queens}) \union exts)
-                                      /\ UNCHANGED sols
+                                      /\ sols' = sols
                    /\ pc' = "nxtQ"
               ELSE /\ pc' = "Done"
                    /\ UNCHANGED << todo, sols >>
 
+(* Allow infinite stuttering to prevent deadlock on termination. *)
+Terminating == pc = "Done" /\ UNCHANGED vars
+
 Next == nxtQ
-           \/ (* Disjunct to prevent deadlock on termination *)
-              (pc = "Done" /\ UNCHANGED vars)
+           \/ Terminating
 
 Spec == Init /\ [][Next]_vars
 

specifications/N-Queens/QueensPluscal.toolbox/FourQueens/QueensPluscal.tla

@@ -86,14 +86,16 @@ nxtQ == /\ pc = "nxtQ"
                                  THEN /\ todo' = todo \ {queens}
                                       /\ sols' = (sols \union exts)
                                  ELSE /\ todo' = ((todo \ {queens}) \union exts)
-                                      /\ UNCHANGED sols
+                                      /\ sols' = sols
                    /\ pc' = "nxtQ"
               ELSE /\ pc' = "Done"
                    /\ UNCHANGED << todo, sols >>
 
+(* Allow infinite stuttering to prevent deadlock on termination. *)
+Terminating == pc = "Done" /\ UNCHANGED vars
+
 Next == nxtQ
-           \/ (* Disjunct to prevent deadlock on termination *)
-              (pc = "Done" /\ UNCHANGED vars)
+           \/ Terminating
 
 Spec == Init /\ [][Next]_vars
 

specifications/TLC/TLCMC.tla

@@ -258,9 +258,11 @@ trc == /\ pc = "trc"
                   /\ UNCHANGED counterexample
        /\ UNCHANGED << S, C, state, successors, i, T >>
 
+(* Allow infinite stuttering to prevent deadlock on termination. *)
+Terminating == pc = "Done" /\ UNCHANGED vars
+
 Next == init \/ initPost \/ scsr \/ each \/ trc
-           \/ (* Disjunct to prevent deadlock on termination *)
-              (pc = "Done" /\ UNCHANGED vars)
+           \/ Terminating
 
 Spec == /\ Init /\ [][Next]_vars
         /\ WF_vars(Next)

specifications/TeachingConcurrency/Simple.tla

@@ -57,9 +57,12 @@ b(self) == /\ pc[self] = "b"
 
 proc(self) == a(self) \/ b(self)
 
+(* Allow infinite stuttering to prevent deadlock on termination. *)
+Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
+               /\ UNCHANGED vars
+
 Next == (\E self \in 0..N-1: proc(self))
-           \/ (* Disjunct to prevent deadlock on termination *)
-              ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)
+           \/ Terminating
 
 Spec == Init /\ [][Next]_vars
 
@@ -148,7 +151,7 @@ THEOREM Spec => []PCorrect
   <2>3. CASE UNCHANGED vars
     BY <2>3 DEF TypeOK, Inv, vars
   <2>4. QED
-    BY <2>1, <2>2, <2>3 DEF Next, proc
+    BY <2>1, <2>2, <2>3 DEF Next, Terminating, proc
 <1>3. Inv => PCorrect
   BY DEF Inv, TypeOK, PCorrect
 <1>4. QED

specifications/TeachingConcurrency/SimpleRegular.tla

@@ -98,9 +98,12 @@ b(self) == /\ pc[self] = "b"
 
 proc(self) == a1(self) \/ a2(self) \/ b(self)
 
+(* Allow infinite stuttering to prevent deadlock on termination. *)
+Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
+               /\ UNCHANGED vars
+
 Next == (\E self \in 0..N-1: proc(self))
-           \/ (* Disjunct to prevent deadlock on termination *)
-              ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)
+           \/ Terminating
 
 Spec == Init /\ [][Next]_vars
 
@@ -166,7 +169,7 @@ THEOREM Spec => []PCorrect
   <2>4. CASE UNCHANGED vars
     BY <2>4 DEF TypeOK, Inv, vars
   <2>5. QED
-    BY <2>1, <2>2, <2>3, <2>4 DEF Next, proc
+    BY <2>1, <2>2, <2>3, <2>4 DEF Next, Terminating, proc
 <1>3. Inv => PCorrect
   BY DEF Inv, TypeOK, PCorrect
 <1>4. QED