CI.yml

name: Check Specs & Metadata
on:
  push:
    branches:
      - master
  pull_request:
    branches:
      - master
  repository_dispatch:
    types: [tlaplus-dispatch]

jobs:
  validate:
    name: Validate Manifest, Specs, & Models
    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" \
            --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               \
            --ci_ignore_path .ciignore
      - name: Check manifest feature flags
        run: |
          python "$SCRIPT_DIR/check_manifest_features.py" \
            --manifest_path manifest.json
      - name: Check README spec table
        run: |
          python "$SCRIPT_DIR/check_markdown_table.py"  \
            --manifest_path manifest.json               \
            --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"      \
            --manifest_path manifest.json
      - name: Add unicode shims
        if: matrix.unicode
        run: |
          python "$SCRIPT_DIR/unicode_number_set_shim.py" \
            --manifest_path manifest.json
      - 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  \
            --manifest_path manifest.json                   \
            --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 \
            --manifest_path manifest.json
      - name: Check small models
        run: |
          # Need to have a nonempty list to pass as a skip parameter
          SKIP=("does/not/exist")
          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 \
            --manifest_path manifest.json                                \
            --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 \
            --manifest_path manifest.json                                \
            --skip "${SKIP[@]}"
      - name: Check proofs
        if: matrix.os != 'windows-latest' && !matrix.unicode
        run: |
          SKIP=(
            # Failing; see https://github.com/tlaplus/Examples/issues/67
            specifications/Bakery-Boulangerie/Bakery.tla
            specifications/Bakery-Boulangerie/Boulanger.tla
            specifications/Paxos/Consensus.tla
            specifications/PaxosHowToWinATuringAward/Consensus.tla
            specifications/lamport_mutex/LamportMutex_proofs.tla
            specifications/ewd998/EWD998_proof.tla
            specifications/byzpaxos/VoteProof.tla
            # Long-running; see https://github.com/tlaplus/tlapm/issues/85
            specifications/LoopInvariance/Quicksort.tla
            specifications/LoopInvariance/SumSequence.tla
            specifications/bcastByz/bcastByz.tla
            specifications/MisraReachability/ReachabilityProofs.tla
            specifications/byzpaxos/BPConProof.tla # Takes about 30 minutes
          )
          python $SCRIPT_DIR/check_proofs.py       \
            --tlapm_path $DEPS_DIR/tlapm-install   \
            --manifest_path manifest.json          \
            --skip "${SKIP[@]}"
      - name: Smoke-test manifest generation script
        run: |
          python $SCRIPT_DIR/generate_manifest.py \
            --manifest_path manifest.json         \
            --ci_ignore_path .ciignore
          git diff -a