Add TLAi linter.

.github/workflows/tlaplus.yml

@@ -9,7 +9,10 @@ on:
       - "tla/**"
   workflow_dispatch:
 
-permissions: read-all
+permissions:
+  actions: read
+  contents: read
+  security-events: write
 
 jobs:
   model-checking-consistency:
@@ -108,3 +111,45 @@ jobs:
           path: |
             tla/consistency/*_TTrace_*.tla
             tla/*.json
+
+  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 }}
+
+    steps:
+      - name: Clone repo
+        uses: actions/checkout@v4
+        with:
+          ## All history for git diff below to succeed.
+          fetch-depth: 0
+
+      - name: Check if HEAD commit contains TLA changes.
+        id: git_commit
+        run: echo "::set-output name=contains_tla::$(git diff --name-only HEAD^ | grep -q '\.tla' && echo 'true' || echo 'false')"
+
+      - name: Setup NodeJS
+        if: steps.git_commit.outputs.contains_tla == 'true'
+        ## 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.
+        if: steps.git_commit.outputs.contains_tla == 'true'
+        ## 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/ (redirect other output to /dev/null for GH not to also show the annotations)
+        run: npx --yes genaiscript run scripts/TLAi-linter.genai.js $(git diff --name-only HEAD^ | grep '\.tla') --max-tokens 2000 --out-annotations results.sarif > /dev/null
+
+      - name: Upload SARIF file
+        if: (success() || failure()) && steps.git_commit.outputs.contains_tla == 'true'
+        ## https://sarifweb.azurewebsites.net
+        ## https://docs.github.com/en/code-security/code-scanning/integrating-with-code-scanning/uploading-a-sarif-file-to-github
+        uses: github/codeql-action/upload-sarif@v3
+        with:
+          sarif_file: results.sarif

scripts/TLAi-linter.genai.js

@@ -0,0 +1,33 @@
+// 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\`.
+`;

tla/StatsFile.tla

@@ -20,7 +20,8 @@
 SerialiseCoverageConstraint ==
     LET interval == 500000
     IN IF TLCGet("distinct") % interval = 0 
-       THEN Serialize(<<TLCGet("spec")>>, CoverageFilename, [format |-> "NDJSON", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "APPEND">>])
+       THEN /\ Serialize(<<TLCGet("spec")>>, CoverageFilename, [format |-> "NDJSON", charset |-> "UTF-8", openOptions |-> <<"WRITE", "CREATE", "APPEND">>])
+            /\ PrintT("Writing coverage to file: " \o CoverageFilename)
        ELSE TRUE
 
 ====