CI.yml

name: Check Specs & Metadata
on:
  push:
    branches:
      - master
  pull_request:
    branches:
      - master
  repository_dispatch:
    types: [tlaplus-dispatch]
concurrency:
  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
  cancel-in-progress: true

jobs:
  validate:
    runs-on: ${{ matrix.os }}
    strategy:
      matrix:
        os: [windows-latest, ubuntu-latest, macos-latest]
        unicode: [true, false]
      fail-fast: false
    env:
      SCRIPT_DIR: .github/scripts
      DEPS_DIR: deps
    defaults:
      run:
        shell: bash
    steps:
      - name: Clone repo
        uses: actions/checkout@v4
      - name: Install python
        uses: actions/setup-python@v5
        with:
          python-version: '3.12'
      - name: Install Java
        uses: actions/setup-java@v4
        with:
          distribution: adopt
          java-version: 17
      - name: Download TLA⁺ dependencies (Windows)
        if: matrix.os == 'windows-latest'
        run: $SCRIPT_DIR/windows-setup.sh $SCRIPT_DIR $DEPS_DIR false
      - name: Download TLA⁺ dependencies (Linux & macOS)
        if: matrix.os != 'windows-latest'
        run: $SCRIPT_DIR/linux-setup.sh $SCRIPT_DIR $DEPS_DIR false
      - name: Check manifest.json format
        run: |
          python "$SCRIPT_DIR/check_manifest_schema.py" \
            --schema_path manifest-schema.json
      - name: Check manifest files
        run: |
          python "$SCRIPT_DIR/check_manifest_files.py"  \
            --ci_ignore_path .ciignore
      - name: Check manifest feature flags
        run: |
          python "$SCRIPT_DIR/check_manifest_features.py" \
            --examples_root .
      - name: Check README spec table
        run: |
          python "$SCRIPT_DIR/check_markdown_table.py"  \
            --readme_path README.md
      - name: Convert specs to unicode
        if: matrix.unicode
        run: |
          python "$SCRIPT_DIR/unicode_conversion.py"  \
            --tlauc_path "$DEPS_DIR/tlauc/tlauc"      \
            --examples_root .
      - name: Translate PlusCal
        # PlusCal translations will be reverted at the end of this step,
        # since we want to support people manually editing the generated TLA+
        # code in specs they submit as examples. However, running the PlusCal
        # translator is currently the only way to ensure that specs contain
        # valid PlusCal syntax. So, we have to run the translator and then
        # discard the results. However, discarding the results with git reset
        # also would discard the Unicode translation. So, only execute this
        # step if we did not perform Unicode translation.
        if: (!matrix.unicode)
        run: |
          # https://github.com/tlaplus/tlaplus/issues/906
          SKIP=(
            "specifications/byzpaxos/BPConProof.tla"
            "specifications/byzpaxos/PConProof.tla"
            "specifications/byzpaxos/VoteProof.tla"
          )
          python $SCRIPT_DIR/translate_pluscal.py           \
            --tools_jar_path $DEPS_DIR/tools/tla2tools.jar  \
            --examples_root .                               \
            --skip "${SKIP[@]}"
          git reset --hard HEAD # Restore specs to their original state
      - name: Parse all modules
        run: |
          python $SCRIPT_DIR/parse_modules.py                            \
            --tools_jar_path $DEPS_DIR/tools/tla2tools.jar               \
            --apalache_path $DEPS_DIR/apalache                           \
            --tlapm_lib_path $DEPS_DIR/tlapm/library                     \
            --community_modules_jar_path $DEPS_DIR/community/modules.jar \
            --examples_root .
      - name: Check small models
        run: |
          # Need to have a nonempty list to pass as a skip parameter
          # SKIP=("does/not/exist")
          # strange issue with parsing TLC output
          SKIP=("specifications/ewd840/EWD840.cfg")
          if [ ${{ matrix.unicode }} ]; then
            # Apalache does not yet support Unicode
            SKIP+=("specifications/EinsteinRiddle/Einstein.cfg")
          fi
          python $SCRIPT_DIR/check_small_models.py                       \
            --verbose                                                    \
            --tools_jar_path $DEPS_DIR/tools/tla2tools.jar               \
            --apalache_path $DEPS_DIR/apalache                           \
            --tlapm_lib_path $DEPS_DIR/tlapm/library                     \
            --community_modules_jar_path $DEPS_DIR/community/modules.jar \
            --examples_root .                                            \
            --skip "${SKIP[@]}"
      - name: Smoke-test large models
        run: |
          # SimKnuthYao requires certain number of states to have been generated
          # before termination or else it fails. This makes it not amenable to
          # smoke testing.
          SKIP=("specifications/KnuthYao/SimKnuthYao.cfg")
          # SimTokenRing does not work on Windows systems.
          if [[ "${{ matrix.os }}" == "windows-latest" ]]; then
            SKIP+=("specifications/ewd426/SimTokenRing.cfg")
          fi
          python $SCRIPT_DIR/smoke_test_large_models.py                  \
            --verbose                                                    \
            --tools_jar_path $DEPS_DIR/tools/tla2tools.jar               \
            --apalache_path $DEPS_DIR/apalache                           \
            --tlapm_lib_path $DEPS_DIR/tlapm/library                     \
            --community_modules_jar_path $DEPS_DIR/community/modules.jar \
            --examples_root .                                            \
            --skip "${SKIP[@]}"
      - name: Check proofs
        if: matrix.os != 'windows-latest' && !matrix.unicode
        run: |
          set -o pipefail
          find specifications -iname "manifest.json" -print0 \
          | xargs --null --no-run-if-empty \
          jq --join-output '
            .modules
            | map(select(has("proof")))
            | map(select(.path != "specifications/LoopInvariance/SumSequence.tla"))
            | map(.path + "\u0000")
            | join("")' \
          | xargs --verbose --null --no-run-if-empty -I {TLA_FILE} \
          "$DEPS_DIR/tlapm/bin/tlapm" "{TLA_FILE}" -I "$DEPS_DIR/community" --stretch 5
      - name: Smoke-test manifest generation script
        run: |
          python $SCRIPT_DIR/generate_manifest.py \
            --ci_ignore_path .ciignore
          git diff -a
      - name: Smoke-test state space script
        run: |
          git reset --hard HEAD
          python $SCRIPT_DIR/record_model_state_space.py                  \
            --tools_jar_path $DEPS_DIR/tools/tla2tools.jar                \
            --tlapm_lib_path $DEPS_DIR/tlapm/library                      \
            --community_modules_jar_path $DEPS_DIR/community/modules.jar  \
            --examples_root .
          git diff -a