Update EWD998PCal.tla comments

.github/scripts/tlAI-Linter.genai.js

@@ -0,0 +1,26 @@
+// metadata (including model parameters)
+// learn more at https://aka.ms/genaiscript
+script({ title: "tlAI-Linter", description: "Check if the prose comments and their TLA+ declarations and definitions are syntactically and semantically consistent" })
+
+// use def to emit LLM variables
+def("TLA+", env.files.filter(f => f.filename.endsWith(".tla")), {lineNumbers: true})
+
+// use $ to output formatted text to the prompt
+$`You are an expert at TLA+/TLAPLUS. Your task is to check if the prose comments and their TLA+ declarations and definitions are syntactically and semantically consistent!!!
+Explain any consistencies and inconsistencies you may find.  Report inconsistent and consistent pairs in a single ANNOTATION section.
+
+## TLA+ Syntax Hints
+- A formula [A]_v is called a temporal formula, and is shorthand for the formula A \/ v' = v.  In other words, the formula is true if A is true or if the value of v remains unchanged.  Usually v is a tuple of the spec's variables.
+- The symbol \`#\` is alternative syntax used for inequality in TLA+; the other symbol is \`/=\".
+
+## TLA+ Semantics Hints
+- Do NOT add any invariants or properties to the behavior specification Spec or any of its subformulas.  This would change THEOREM Spec => Inv into THEOREM Spec /\ Inv => Inv, which is vacuously true.
+- TLA+ specs are always stuttering insensitive, i.e., the next-state relation is always [A]_v.  In other words, one cannot write a stuttering sensitive specification.
+
+## TLA+ Convention Hints
+- The type correctness invariant is typically called TypeOK.
+- Users can employ TLA labels as a means to conceptually associate a comment with a sub-formula like a specific disjunct or conjunct of a TLA formula. Even though these labels have no other function, they facilitate referencing particular parts of the formula from a comment.
+
+## Formal and informal math Hints
+- Take into account that humans may write informal math that is syntactically different from the formal math, yet semantically equivalent.  For example, humans may write \`N > 3T\` instead of \`N > 3 * T\`.
+`        

.github/workflows/PR.yml

@@ -0,0 +1,49 @@
+name: tlAI-linter
+
+on:
+  pull_request:
+    branches:
+      - master
+
+jobs:
+  linting:
+    name: tlAI-linter
+
+    runs-on: ubuntu-latest
+
+    env:
+      ## https://microsoft.github.io/genaiscript/reference/token/
+      OPENAI_API_KEY: ${{ secrets.OPENAI_API_KEY }}
+      OPENAI_API_BASE: ${{ secrets.OPENAI_API_BASE }}
+      OPENAI_API_TYPE: ${{ secrets.OPENAI_API_TYPE }}
+
+    defaults:
+      run:
+        shell: bash
+
+    steps:
+      - name: Clone repo
+        uses: actions/checkout@v4
+        with:
+            ## All history for git diff below to succeed.
+            fetch-depth: 0
+
+      - name: Setup NodeJS
+        ## https://github.com/actions/setup-node
+        uses: actions/setup-node@v4
+        with:
+            node-version: "20"
+
+      - name: Run GenAIscript on the TLA+ specs that are added in this pull request.
+        ## Identify git diff: $(git diff --name-only HEAD^ | grep '.tla')
+        ## Install genaiscript runtime: https://microsoft.github.io/genaiscript/reference/cli/
+        ## Output LLM response in SARIF format: https://microsoft.github.io/genaiscript/reference/scripts/annotations/
+        run: npx --yes genaiscript-cli run .github/scripts/tlAI-Linter.genai.js $(git diff --name-only HEAD^ | grep '.tla') -oa results.sarif > /dev/null
+
+      - name: Upload SARIF file
+        ## https://sarifweb.azurewebsites.net
+        ## https://docs.github.com/en/code-security/code-scanning/integrating-with-code-scanning/uploading-a-sarif-file-to-github
+        if: success() || failure()
+        uses: github/codeql-action/upload-sarif@v3
+        with:
+            sarif_file: results.sarif

specifications/ewd998/EWD998PCal.tla

@@ -8,7 +8,7 @@
 EXTENDS Integers, Bags, BagsExt
 
 CONSTANT N
-ASSUME NAssumption == N \in Nat \ {0} \* At least one node.
+ASSUME NAssumption == N \in Nat \ {0} \* Any number of nodes between zero and infinitely many.
 
 Node == 0 .. N-1
 
@@ -61,13 +61,13 @@
       } or { \* terminate the current node.
         active := FALSE
 
-      } or { \* pass the token to the next node.
+      } or { \* pass the token to some node.
         when self # Initiator;
         with (tok \in pendingMsgs(network, self)) {
             when tok.type = "tok" /\ ~active;
             network := passMsg(network, self, tok, self-1, [type|-> "tok", q |-> tok.q + counter, color |-> (IF color = "black" THEN "black" ELSE tok.color)]);
             color := "white";
         }
 
       } or { \* Initiate token.
         when self = Initiator;