From cd94919087779d9ee49c921390309851dc1667e2 Mon Sep 17 00:00:00 2001
From: Andrew Helwer <2n8rn1w1f@mozmail.com>
Date: Wed, 10 Apr 2024 15:32:42 -0400
Subject: [PATCH 01/16] Added basic translation script

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
---
 .github/scripts/translate_pluscal.py  | 72 +++++++++++++++++++++++++++
 .github/scripts/unicode_conversion.py |  1 +
 2 files changed, 73 insertions(+)
 create mode 100644 .github/scripts/translate_pluscal.py

diff --git a/.github/scripts/translate_pluscal.py b/.github/scripts/translate_pluscal.py
new file mode 100644
index 00000000..6c11a721
--- /dev/null
+++ b/.github/scripts/translate_pluscal.py
@@ -0,0 +1,72 @@
+"""
+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 PlusCal in {module_path}')
+    result = subprocess.run(
+        ['java', '-cp', tools_path, 'pcal.trans', module_path],
+        stdout=subprocess.PIPE,
+        stderr=subprocess.STDOUT,
+        text=True
+    )
+    match result:
+        case CompletedProcess():
+            if result.returncode == 0:
+                logging.info(result.stdout)
+                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
+thread_count = 1
+logging.info(f'Translating using {thread_count} threads')
+with ThreadPoolExecutor(thread_count) as executor:
+    results = executor.map(translate_module, modules)
+    exit(0 if all(results) else 1)
+
diff --git a/.github/scripts/unicode_conversion.py b/.github/scripts/unicode_conversion.py
index 3808285d..9d4ea68d 100644
--- a/.github/scripts/unicode_conversion.py
+++ b/.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

From 926215bfd58e8bc46ae57c19b84679082caa61ab Mon Sep 17 00:00:00 2001
From: Andrew Helwer <2n8rn1w1f@mozmail.com>
Date: Wed, 10 Apr 2024 15:33:52 -0400
Subject: [PATCH 02/16] Don't write cfg

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
---
 .github/scripts/translate_pluscal.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/scripts/translate_pluscal.py b/.github/scripts/translate_pluscal.py
index 6c11a721..8fbd6f56 100644
--- a/.github/scripts/translate_pluscal.py
+++ b/.github/scripts/translate_pluscal.py
@@ -45,7 +45,7 @@
 def translate_module(module_path):
     logging.info(f'Translating PlusCal in {module_path}')
     result = subprocess.run(
-        ['java', '-cp', tools_path, 'pcal.trans', module_path],
+        ['java', '-cp', tools_path, 'pcal.trans', '-nocfg', module_path],
         stdout=subprocess.PIPE,
         stderr=subprocess.STDOUT,
         text=True

From c2e1c6b7f5e62053fb82bb54bb02599816a4b657 Mon Sep 17 00:00:00 2001
From: Andrew Helwer <2n8rn1w1f@mozmail.com>
Date: Wed, 10 Apr 2024 16:43:35 -0400
Subject: [PATCH 03/16] Parallelize check

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
---
 .github/scripts/translate_pluscal.py | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/.github/scripts/translate_pluscal.py b/.github/scripts/translate_pluscal.py
index 8fbd6f56..6f824d60 100644
--- a/.github/scripts/translate_pluscal.py
+++ b/.github/scripts/translate_pluscal.py
@@ -53,7 +53,6 @@ def translate_module(module_path):
     match result:
         case CompletedProcess():
             if result.returncode == 0:
-                logging.info(result.stdout)
                 return True
             else:
                 logging.error(f'Module {module_path} conversion failed with return code {result.returncode}; output:\n{result.stdout}')
@@ -63,8 +62,7 @@ def translate_module(module_path):
             return False
 
 success = True
-#thread_count = cpu_count() if not args.verbose else 1
-thread_count = 1
+thread_count = cpu_count() if not args.verbose else 1
 logging.info(f'Translating using {thread_count} threads')
 with ThreadPoolExecutor(thread_count) as executor:
     results = executor.map(translate_module, modules)

From 59d239f1a1102bdc8faf65d364f2076422bb639a Mon Sep 17 00:00:00 2001
From: Andrew Helwer <2n8rn1w1f@mozmail.com>
Date: Wed, 10 Apr 2024 16:47:28 -0400
Subject: [PATCH 04/16] Added pluscal script to CI

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
---
 .github/workflows/CI.yml | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml
index a338c9c2..4b68f853 100644
--- a/.github/workflows/CI.yml
+++ b/.github/workflows/CI.yml
@@ -75,6 +75,12 @@ 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: |
+          python $SCRIPT_DIR/parse_modules.py                            \
+            --tools_jar_path $DEPS_DIR/tools/tla2tools.jar               \
+            --manifest_path manifest.json
       - name: Parse all modules
         run: |
           # Need to have a nonempty list to pass as a skip parameter

From 779cb3706b569a24388ed645e4aa492ac6030d16 Mon Sep 17 00:00:00 2001
From: Andrew Helwer <2n8rn1w1f@mozmail.com>
Date: Wed, 10 Apr 2024 16:49:11 -0400
Subject: [PATCH 05/16] Changed pcal translate messages

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
---
 .github/scripts/translate_pluscal.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/scripts/translate_pluscal.py b/.github/scripts/translate_pluscal.py
index 6f824d60..324fbf3d 100644
--- a/.github/scripts/translate_pluscal.py
+++ b/.github/scripts/translate_pluscal.py
@@ -43,7 +43,7 @@
     logging.info(f'Skipping {path}')
 
 def translate_module(module_path):
-    logging.info(f'Translating PlusCal in {module_path}')
+    logging.info(f'Translating {module_path}')
     result = subprocess.run(
         ['java', '-cp', tools_path, 'pcal.trans', '-nocfg', module_path],
         stdout=subprocess.PIPE,
@@ -63,7 +63,7 @@ def translate_module(module_path):
 
 success = True
 thread_count = cpu_count() if not args.verbose else 1
-logging.info(f'Translating using {thread_count} threads')
+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)

From d96b943409eb21e2d8c1a3fcb3d43ecb5523ba14 Mon Sep 17 00:00:00 2001
From: Andrew Helwer <2n8rn1w1f@mozmail.com>
Date: Wed, 10 Apr 2024 16:56:49 -0400
Subject: [PATCH 06/16] Trivial pluscal spec updates

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
---
 specifications/DiningPhilosophers/DiningPhilosophers.tla  | 2 +-
 specifications/LoopInvariance/BinarySearch.tla            | 6 ++++--
 specifications/LoopInvariance/Quicksort.tla               | 6 ++++--
 specifications/LoopInvariance/SumSequence.tla             | 6 ++++--
 specifications/MisraReachability/ParReach.tla             | 7 +++++--
 specifications/MisraReachability/Reachable.tla            | 7 ++++---
 specifications/MultiPaxos-SMR/MultiPaxos.tla              | 2 +-
 specifications/N-Queens/QueensPluscal.tla                 | 8 +++++---
 .../QueensPluscal.toolbox/FourQueens/QueensPluscal.tla    | 8 +++++---
 specifications/TLC/TLCMC.tla                              | 6 ++++--
 specifications/TeachingConcurrency/Simple.tla             | 7 +++++--
 specifications/TeachingConcurrency/SimpleRegular.tla      | 7 +++++--
 specifications/echo/Echo.tla                              | 4 ++--
 specifications/ewd687a/EWD687aPlusCal.tla                 | 2 +-
 14 files changed, 50 insertions(+), 28 deletions(-)

diff --git a/specifications/DiningPhilosophers/DiningPhilosophers.tla b/specifications/DiningPhilosophers/DiningPhilosophers.tla
index a8eeb4be..2fbce81f 100644
--- a/specifications/DiningPhilosophers/DiningPhilosophers.tla
+++ b/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 *)
diff --git a/specifications/LoopInvariance/BinarySearch.tla b/specifications/LoopInvariance/BinarySearch.tla
index 4a0736a3..eb66434d 100644
--- a/specifications/LoopInvariance/BinarySearch.tla
+++ b/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)
diff --git a/specifications/LoopInvariance/Quicksort.tla b/specifications/LoopInvariance/Quicksort.tla
index f92dcd65..8c0f80ef 100644
--- a/specifications/LoopInvariance/Quicksort.tla
+++ b/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)
diff --git a/specifications/LoopInvariance/SumSequence.tla b/specifications/LoopInvariance/SumSequence.tla
index 7e8e0b21..e3a33c03 100644
--- a/specifications/LoopInvariance/SumSequence.tla
+++ b/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)
diff --git a/specifications/MisraReachability/ParReach.tla b/specifications/MisraReachability/ParReach.tla
index ea991f1b..d218066c 100644
--- a/specifications/MisraReachability/ParReach.tla
+++ b/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))
diff --git a/specifications/MisraReachability/Reachable.tla b/specifications/MisraReachability/Reachable.tla
index f44b5dbf..30fec9bc 100644
--- a/specifications/MisraReachability/Reachable.tla
+++ b/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)
diff --git a/specifications/MultiPaxos-SMR/MultiPaxos.tla b/specifications/MultiPaxos-SMR/MultiPaxos.tla
index 54b627e0..bd13bd90 100644
--- a/specifications/MultiPaxos-SMR/MultiPaxos.tla
+++ b/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 *)
diff --git a/specifications/N-Queens/QueensPluscal.tla b/specifications/N-Queens/QueensPluscal.tla
index 27b8dbe2..a7429621 100644
--- a/specifications/N-Queens/QueensPluscal.tla
+++ b/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
 
diff --git a/specifications/N-Queens/QueensPluscal.toolbox/FourQueens/QueensPluscal.tla b/specifications/N-Queens/QueensPluscal.toolbox/FourQueens/QueensPluscal.tla
index 27b8dbe2..a7429621 100644
--- a/specifications/N-Queens/QueensPluscal.toolbox/FourQueens/QueensPluscal.tla
+++ b/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
 
diff --git a/specifications/TLC/TLCMC.tla b/specifications/TLC/TLCMC.tla
index efaf2eef..b81f1431 100644
--- a/specifications/TLC/TLCMC.tla
+++ b/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)
diff --git a/specifications/TeachingConcurrency/Simple.tla b/specifications/TeachingConcurrency/Simple.tla
index 49894e42..3f5721eb 100644
--- a/specifications/TeachingConcurrency/Simple.tla
+++ b/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
 
diff --git a/specifications/TeachingConcurrency/SimpleRegular.tla b/specifications/TeachingConcurrency/SimpleRegular.tla
index eb5909f4..d04aa034 100644
--- a/specifications/TeachingConcurrency/SimpleRegular.tla
+++ b/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
 
diff --git a/specifications/echo/Echo.tla b/specifications/echo/Echo.tla
index 6677121c..4d496bee 100644
--- a/specifications/echo/Echo.tla
+++ b/specifications/echo/Echo.tla
@@ -115,7 +115,7 @@ n1(self) == /\ pc[self] = "n1"
                               /\ rcvd' = [rcvd EXCEPT ![self] = rcvd[self]+1]
                               /\ IF self # initiator /\ rcvd'[self] = 1
                                     THEN /\ Assert((msg.kind = "m"), 
-                                                   "Failure of assertion at line 50, column 16.")
+                                                   "Failure of assertion at line 55, column 16.")
                                          /\ parent' = [parent EXCEPT ![self] = msg.sndr]
                                          /\ inbox' = multicast(net, self, nbrs[self] \ {msg.sndr}, "m")
                                     ELSE /\ inbox' = net
@@ -132,7 +132,7 @@ n1(self) == /\ pc[self] = "n1"
 n2(self) == /\ pc[self] = "n2"
             /\ IF self # initiator
                   THEN /\ Assert((parent[self] \in nbrs[self]), 
-                                 "Failure of assertion at line 65, column 10.")
+                                 "Failure of assertion at line 70, column 10.")
                        /\ inbox' = send(inbox, self, parent[self], "c")
                   ELSE /\ TRUE
                        /\ inbox' = inbox
diff --git a/specifications/ewd687a/EWD687aPlusCal.tla b/specifications/ewd687a/EWD687aPlusCal.tla
index 1a3b1a23..c229cfeb 100644
--- a/specifications/ewd687a/EWD687aPlusCal.tla
+++ b/specifications/ewd687a/EWD687aPlusCal.tla
@@ -88,7 +88,7 @@ l:  while (TRUE) {
   }
 }
 *)
-\* BEGIN TRANSLATION (chksum(pcal) = "2130f031" /\ chksum(tla) = "7d13cf45")
+\* BEGIN TRANSLATION (chksum(pcal) = "d18d3150" /\ chksum(tla) = "7d13cf45")
 VARIABLES terminationDetected, network
 
 (* define statement *)

From 0675c537cc6203193bc54007fa505d87f519201a Mon Sep 17 00:00:00 2001
From: Andrew Helwer <2n8rn1w1f@mozmail.com>
Date: Wed, 10 Apr 2024 16:59:03 -0400
Subject: [PATCH 07/16] Write out status and diff

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
---
 .github/workflows/CI.yml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml
index 4b68f853..422a2611 100644
--- a/.github/workflows/CI.yml
+++ b/.github/workflows/CI.yml
@@ -81,6 +81,8 @@ jobs:
           python $SCRIPT_DIR/parse_modules.py                            \
             --tools_jar_path $DEPS_DIR/tools/tla2tools.jar               \
             --manifest_path manifest.json
+          git status
+          git diff
       - name: Parse all modules
         run: |
           # Need to have a nonempty list to pass as a skip parameter

From 55c2822e8b9f503c059f8bdde57154372a4a6c76 Mon Sep 17 00:00:00 2001
From: Andrew Helwer <2n8rn1w1f@mozmail.com>
Date: Wed, 10 Apr 2024 17:04:00 -0400
Subject: [PATCH 08/16] Fix script call in CI

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
---
 .github/workflows/CI.yml | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml
index 422a2611..8d7e5a91 100644
--- a/.github/workflows/CI.yml
+++ b/.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
@@ -78,8 +78,8 @@ jobs:
       - name: Translate PlusCal
         if: (!matrix.unicode) # PlusCal does not yet support unicode
         run: |
-          python $SCRIPT_DIR/parse_modules.py                            \
-            --tools_jar_path $DEPS_DIR/tools/tla2tools.jar               \
+          python $SCRIPT_DIR/translate_pluscal.py           \
+            --tools_jar_path $DEPS_DIR/tools/tla2tools.jar  \
             --manifest_path manifest.json
           git status
           git diff

From 901f69840d34ab839269fc312724ac5345f80ffa Mon Sep 17 00:00:00 2001
From: Andrew Helwer <2n8rn1w1f@mozmail.com>
Date: Wed, 10 Apr 2024 17:18:20 -0400
Subject: [PATCH 09/16] Skip Slush.tla on windows

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
---
 .github/workflows/CI.yml | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml
index 8d7e5a91..510543cc 100644
--- a/.github/workflows/CI.yml
+++ b/.github/workflows/CI.yml
@@ -78,9 +78,18 @@ jobs:
       - name: Translate PlusCal
         if: (!matrix.unicode) # PlusCal does not yet support unicode
         run: |
+          # Need to have a nonempty list to pass as a skip parameter
+          SKIP=("does/not/exist")
+          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
+            --manifest_path manifest.json                   \
+            --skip "${SKIP[@]}"
           git status
           git diff
       - name: Parse all modules

From 51390a645043a646d38f7fcac386d743ee8f4d3a Mon Sep 17 00:00:00 2001
From: Andrew Helwer <2n8rn1w1f@mozmail.com>
Date: Wed, 10 Apr 2024 17:32:43 -0400
Subject: [PATCH 10/16] Ignore some pcal translate specs

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
---
 .github/workflows/CI.yml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml
index 510543cc..4a38bebd 100644
--- a/.github/workflows/CI.yml
+++ b/.github/workflows/CI.yml
@@ -78,8 +78,12 @@ jobs:
       - name: Translate PlusCal
         if: (!matrix.unicode) # PlusCal does not yet support unicode
         run: |
-          # Need to have a nonempty list to pass as a skip parameter
-          SKIP=("does/not/exist")
+          # 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

From 70271839ce3694aca065d9c02c97610e3b1a78c2 Mon Sep 17 00:00:00 2001
From: Andrew Helwer <2n8rn1w1f@mozmail.com>
Date: Wed, 10 Apr 2024 17:50:04 -0400
Subject: [PATCH 11/16] Translate Dijkstra mutex with updated version of
 PlusCal

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
---
 .../dijkstra-mutex/DijkstraMutex.tla          | 20 +++++++------------
 .../LSpec-model/DijkstraMutex.tla             | 20 +++++++------------
 .../Safety-4-processors/DijkstraMutex.tla     | 20 +++++++------------
 3 files changed, 21 insertions(+), 39 deletions(-)

diff --git a/specifications/dijkstra-mutex/DijkstraMutex.tla b/specifications/dijkstra-mutex/DijkstraMutex.tla
index 0ec95305..bf8d1d68 100644
--- a/specifications/dijkstra-mutex/DijkstraMutex.tla
+++ b/specifications/dijkstra-mutex/DijkstraMutex.tla
@@ -107,7 +107,7 @@ Init == (* Global variables *)
         /\ k \in Proc
         (* Process P *)
         /\ temp = [self \in Proc |-> defaultInitValue]
-        /\ pc = [self \in ProcSet |-> CASE self \in Proc -> "Li0"]
+        /\ pc = [self \in ProcSet |-> "Li0"]
 
 Li0(self) == /\ pc[self] = "Li0"
              /\ b' = [b EXCEPT ![self] = FALSE]
@@ -154,15 +154,12 @@ Li4a(self) == /\ pc[self] = "Li4a"
 Li4b(self) == /\ pc[self] = "Li4b"
               /\ IF temp[self] # {}
                     THEN /\ \E j \in temp[self]:
-                              /\ temp' = [temp EXCEPT 
-                                            ![self] = temp[self] \ {j}]
+                              /\ temp' = [temp EXCEPT ![self] = temp[self] \ {j}]
                               /\ IF ~c[j]
-                                    THEN /\ pc' = [pc EXCEPT 
-                                                     ![self] = "Li1"]
-                                    ELSE /\ pc' = [pc EXCEPT 
-                                                     ![self] = "Li4b"]
+                                    THEN /\ pc' = [pc EXCEPT ![self] = "Li1"]
+                                    ELSE /\ pc' = [pc EXCEPT ![self] = "Li4b"]
                     ELSE /\ pc' = [pc EXCEPT ![self] = "cs"]
-                         /\ UNCHANGED temp
+                         /\ temp' = temp
               /\ UNCHANGED << b, c, k >>
 
 cs(self) == /\ pc[self] = "cs"
@@ -190,12 +187,9 @@ P(self) == Li0(self) \/ Li1(self) \/ Li2(self) \/ Li3a(self) \/ Li3b(self)
               \/ cs(self) \/ Li5(self) \/ Li6(self) \/ ncs(self)
 
 Next == (\E self \in Proc: P(self))
-           \/ (* Disjunct to prevent deadlock on termination *)
-              ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)
 
-Spec == Init /\ [][Next]_vars /\ \A self \in Proc: WF_vars(P(self))
-
-Termination == <>(\A self \in ProcSet: pc[self] = "Done")
+Spec == /\ Init /\ [][Next]_vars
+        /\ \A self \in Proc : WF_vars(P(self))
 
 \* END TRANSLATION
 
diff --git a/specifications/dijkstra-mutex/DijkstraMutex.toolbox/LSpec-model/DijkstraMutex.tla b/specifications/dijkstra-mutex/DijkstraMutex.toolbox/LSpec-model/DijkstraMutex.tla
index b72d3de6..d25e4aa0 100644
--- a/specifications/dijkstra-mutex/DijkstraMutex.toolbox/LSpec-model/DijkstraMutex.tla
+++ b/specifications/dijkstra-mutex/DijkstraMutex.toolbox/LSpec-model/DijkstraMutex.tla
@@ -107,7 +107,7 @@ Init == (* Global variables *)
         /\ k \in Proc
         (* Process P *)
         /\ temp = [self \in Proc |-> defaultInitValue]
-        /\ pc = [self \in ProcSet |-> CASE self \in Proc -> "Li0"]
+        /\ pc = [self \in ProcSet |-> "Li0"]
 
 Li0(self) == /\ pc[self] = "Li0"
              /\ b' = [b EXCEPT ![self] = FALSE]
@@ -154,15 +154,12 @@ Li4a(self) == /\ pc[self] = "Li4a"
 Li4b(self) == /\ pc[self] = "Li4b"
               /\ IF temp[self] # {}
                     THEN /\ \E j \in temp[self]:
-                              /\ temp' = [temp EXCEPT 
-                                            ![self] = temp[self] \ {j}]
+                              /\ temp' = [temp EXCEPT ![self] = temp[self] \ {j}]
                               /\ IF ~c[j]
-                                    THEN /\ pc' = [pc EXCEPT 
-                                                     ![self] = "Li1"]
-                                    ELSE /\ pc' = [pc EXCEPT 
-                                                     ![self] = "Li4b"]
+                                    THEN /\ pc' = [pc EXCEPT ![self] = "Li1"]
+                                    ELSE /\ pc' = [pc EXCEPT ![self] = "Li4b"]
                     ELSE /\ pc' = [pc EXCEPT ![self] = "cs"]
-                         /\ UNCHANGED temp
+                         /\ temp' = temp
               /\ UNCHANGED << b, c, k >>
 
 cs(self) == /\ pc[self] = "cs"
@@ -190,12 +187,9 @@ P(self) == Li0(self) \/ Li1(self) \/ Li2(self) \/ Li3a(self) \/ Li3b(self)
               \/ cs(self) \/ Li5(self) \/ Li6(self) \/ ncs(self)
 
 Next == (\E self \in Proc: P(self))
-           \/ (* Disjunct to prevent deadlock on termination *)
-              ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)
 
-Spec == Init /\ [][Next]_vars /\ \A self \in Proc: WF_vars(P(self))
-
-Termination == <>(\A self \in ProcSet: pc[self] = "Done")
+Spec == /\ Init /\ [][Next]_vars
+        /\ \A self \in Proc : WF_vars(P(self))
 
 \* END TRANSLATION
 
diff --git a/specifications/dijkstra-mutex/DijkstraMutex.toolbox/Safety-4-processors/DijkstraMutex.tla b/specifications/dijkstra-mutex/DijkstraMutex.toolbox/Safety-4-processors/DijkstraMutex.tla
index b72d3de6..d25e4aa0 100644
--- a/specifications/dijkstra-mutex/DijkstraMutex.toolbox/Safety-4-processors/DijkstraMutex.tla
+++ b/specifications/dijkstra-mutex/DijkstraMutex.toolbox/Safety-4-processors/DijkstraMutex.tla
@@ -107,7 +107,7 @@ Init == (* Global variables *)
         /\ k \in Proc
         (* Process P *)
         /\ temp = [self \in Proc |-> defaultInitValue]
-        /\ pc = [self \in ProcSet |-> CASE self \in Proc -> "Li0"]
+        /\ pc = [self \in ProcSet |-> "Li0"]
 
 Li0(self) == /\ pc[self] = "Li0"
              /\ b' = [b EXCEPT ![self] = FALSE]
@@ -154,15 +154,12 @@ Li4a(self) == /\ pc[self] = "Li4a"
 Li4b(self) == /\ pc[self] = "Li4b"
               /\ IF temp[self] # {}
                     THEN /\ \E j \in temp[self]:
-                              /\ temp' = [temp EXCEPT 
-                                            ![self] = temp[self] \ {j}]
+                              /\ temp' = [temp EXCEPT ![self] = temp[self] \ {j}]
                               /\ IF ~c[j]
-                                    THEN /\ pc' = [pc EXCEPT 
-                                                     ![self] = "Li1"]
-                                    ELSE /\ pc' = [pc EXCEPT 
-                                                     ![self] = "Li4b"]
+                                    THEN /\ pc' = [pc EXCEPT ![self] = "Li1"]
+                                    ELSE /\ pc' = [pc EXCEPT ![self] = "Li4b"]
                     ELSE /\ pc' = [pc EXCEPT ![self] = "cs"]
-                         /\ UNCHANGED temp
+                         /\ temp' = temp
               /\ UNCHANGED << b, c, k >>
 
 cs(self) == /\ pc[self] = "cs"
@@ -190,12 +187,9 @@ P(self) == Li0(self) \/ Li1(self) \/ Li2(self) \/ Li3a(self) \/ Li3b(self)
               \/ cs(self) \/ Li5(self) \/ Li6(self) \/ ncs(self)
 
 Next == (\E self \in Proc: P(self))
-           \/ (* Disjunct to prevent deadlock on termination *)
-              ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)
 
-Spec == Init /\ [][Next]_vars /\ \A self \in Proc: WF_vars(P(self))
-
-Termination == <>(\A self \in ProcSet: pc[self] = "Done")
+Spec == /\ Init /\ [][Next]_vars
+        /\ \A self \in Proc : WF_vars(P(self))
 
 \* END TRANSLATION
 

From 976d5bac7c011abe1e4d65980dac0cc2c4affc98 Mon Sep 17 00:00:00 2001
From: Andrew Helwer <2n8rn1w1f@mozmail.com>
Date: Wed, 10 Apr 2024 17:52:46 -0400
Subject: [PATCH 12/16] Fixed out of date pcal translation in
 transaction_commit

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
---
 specifications/transaction_commit/2PCwithBTM.tla | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/specifications/transaction_commit/2PCwithBTM.tla b/specifications/transaction_commit/2PCwithBTM.tla
index 80d8432e..4cfec75f 100644
--- a/specifications/transaction_commit/2PCwithBTM.tla
+++ b/specifications/transaction_commit/2PCwithBTM.tla
@@ -30,7 +30,7 @@ Transaction manager (TM) is added.
    }
 
   macro Fail(p) {
-    if (RMMAYFAIL) rmState[p] := "failed";
+    if (RMMAYFAIL /\ ~\E rm \in RM:rmState[rm]="failed") rmState[p] := "failed";
    }
 
   fair process (RManager \in RM) {
@@ -153,10 +153,13 @@ BTA == /\ pc[10] = "BTA"
 
 BTManager == BTS \/ BTC \/ BTA
 
+(* Allow infinite stuttering to prevent deadlock on termination. *)
+Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
+               /\ UNCHANGED vars
+
 Next == TManager \/ BTManager
            \/ (\E self \in RM: RManager(self))
-           \/ (* Disjunct to prevent deadlock on termination *)
-              ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)
+           \/ Terminating
 
 Spec == /\ Init /\ [][Next]_vars
         /\ \A self \in RM : WF_vars(RManager(self))

From ff30ade6c72e82c33f110d0abce09252f708696e Mon Sep 17 00:00:00 2001
From: Andrew Helwer <2n8rn1w1f@mozmail.com>
Date: Wed, 10 Apr 2024 18:16:43 -0400
Subject: [PATCH 13/16] Fixed proof by expanding new Terminating def

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
---
 specifications/LoopInvariance/BinarySearch.tla       | 2 +-
 specifications/MisraReachability/ParReachProofs.tla  | 6 +++---
 specifications/MisraReachability/ReachableProofs.tla | 4 ++--
 specifications/TeachingConcurrency/Simple.tla        | 2 +-
 specifications/TeachingConcurrency/SimpleRegular.tla | 2 +-
 5 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/specifications/LoopInvariance/BinarySearch.tla b/specifications/LoopInvariance/BinarySearch.tla
index eb66434d..9d7d371a 100644
--- a/specifications/LoopInvariance/BinarySearch.tla
+++ b/specifications/LoopInvariance/BinarySearch.tla
@@ -247,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
diff --git a/specifications/MisraReachability/ParReachProofs.tla b/specifications/MisraReachability/ParReachProofs.tla
index 06327663..4cba9ba2 100644
--- a/specifications/MisraReachability/ParReachProofs.tla
+++ b/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
 
diff --git a/specifications/MisraReachability/ReachableProofs.tla b/specifications/MisraReachability/ReachableProofs.tla
index 2f99e39b..5015bd06 100644
--- a/specifications/MisraReachability/ReachableProofs.tla
+++ b/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
 
diff --git a/specifications/TeachingConcurrency/Simple.tla b/specifications/TeachingConcurrency/Simple.tla
index 3f5721eb..a84c598c 100644
--- a/specifications/TeachingConcurrency/Simple.tla
+++ b/specifications/TeachingConcurrency/Simple.tla
@@ -151,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
diff --git a/specifications/TeachingConcurrency/SimpleRegular.tla b/specifications/TeachingConcurrency/SimpleRegular.tla
index d04aa034..8f6b4084 100644
--- a/specifications/TeachingConcurrency/SimpleRegular.tla
+++ b/specifications/TeachingConcurrency/SimpleRegular.tla
@@ -169,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

From 35b09bef1af63f5b3e9d677d6a91d9e88f7dd657 Mon Sep 17 00:00:00 2001
From: Andrew Helwer <2n8rn1w1f@mozmail.com>
Date: Wed, 10 Apr 2024 19:25:20 -0400
Subject: [PATCH 14/16] Error in CI if PlusCal is out of date

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
---
 .github/workflows/CI.yml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml
index 4a38bebd..50cafd08 100644
--- a/.github/workflows/CI.yml
+++ b/.github/workflows/CI.yml
@@ -94,8 +94,12 @@ jobs:
             --tools_jar_path $DEPS_DIR/tools/tla2tools.jar  \
             --manifest_path manifest.json                   \
             --skip "${SKIP[@]}"
-          git status
-          git diff
+          if [ ! ${{ matrix.unicode }} ]; 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

From aac2b135e26fee7459e0f20fc82d1b9a11f55d72 Mon Sep 17 00:00:00 2001
From: Andrew Helwer <2n8rn1w1f@mozmail.com>
Date: Wed, 10 Apr 2024 19:42:05 -0400
Subject: [PATCH 15/16] I love bash

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
---
 .github/workflows/CI.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml
index 50cafd08..f422eb06 100644
--- a/.github/workflows/CI.yml
+++ b/.github/workflows/CI.yml
@@ -94,7 +94,7 @@ jobs:
             --tools_jar_path $DEPS_DIR/tools/tla2tools.jar  \
             --manifest_path manifest.json                   \
             --skip "${SKIP[@]}"
-          if [ ! ${{ matrix.unicode }} ]; then
+          if [[ ! ${{ matrix.unicode }} ]]; then
             git status
             git diff
             diff_count=$(git status --porcelain=v1 2>/dev/null | wc -l)

From 56552025eeee0fe1b4805a2de62a60925c8908d4 Mon Sep 17 00:00:00 2001
From: Andrew Helwer <2n8rn1w1f@mozmail.com>
Date: Wed, 10 Apr 2024 19:48:10 -0400
Subject: [PATCH 16/16] I love bash

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
---
 .github/workflows/CI.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml
index f422eb06..6a7fec8c 100644
--- a/.github/workflows/CI.yml
+++ b/.github/workflows/CI.yml
@@ -94,7 +94,7 @@ jobs:
             --tools_jar_path $DEPS_DIR/tools/tla2tools.jar  \
             --manifest_path manifest.json                   \
             --skip "${SKIP[@]}"
-          if [[ ! ${{ matrix.unicode }} ]]; then
+          if [[ "${{ matrix.unicode }}" == "false" ]]; then
             git status
             git diff
             diff_count=$(git status --porcelain=v1 2>/dev/null | wc -l)