tlc.yaml

name: TLC

on:
  pull_request:
    branches: [ "main" ]
    paths:
      - ".github/workflows/tlc.yaml"
      - "**.tla"
      - "**.cfg"
  push:
    branches: [ "main" ]
    paths:
      - ".github/workflows/tlc.yaml"
      - "**.tla"
      - "**.cfg"

jobs:
  tlc:
    timeout-minutes: 10
    runs-on: ubuntu-latest
    strategy:
      matrix:
        file:
          - multi-paxos-eb0/MultiPaxos.tla
          - paxos-eb0/PaxosEb0.tla
          - percolator/Transfer.tla
          - percolator/SnapshotRead.tla
          - percolator/MC_SIB_SNAPSHOT.tla
          - sequencer/Sequencer.tla
          - simplified-fast-paxos/SimplifiedFastPaxos.tla
          - isolation-models/ALL_TESTS.tla
    steps:
      - uses: actions/checkout@v4
      - uses: actions/setup-java@v4
        with:
          distribution: 'corretto'
          java-version: '21'
      - name: downloads tla2tools
        run: |
          wget https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar
      - name: model checking
        run: |
          java -cp tla2tools.jar tlc2.TLC ${{ matrix.file }}