tla.yml

name: TLA

on:
  push:
    branches: [ "main" ]
  pull_request:
    branches: [ "main" ]
  workflow_dispatch:

jobs:
  apalache:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: actions/setup-java@v4
        with:
          distribution: 'microsoft'
          java-version: '17'
      - name: Setup
        run: |
          wget https://github.com/informalsystems/apalache/releases/latest/download/apalache.tgz
          tar zxvf apalache.tgz
      - name: Type- and (ordinary) invariant checking with Apalache
        run: |
          ./apalache/bin/apalache-mc check --config=APApbft.cfg APApbft.tla
      - name: Upload Apalache's counterexample (if any)
        uses: actions/upload-artifact@v4
        if: always()
        with:
            path: |
              _apalache-out/APApbft.tla/

  tlc:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - name: Install TLA+ Tools
        run: |
          git clone https://github.com/pmer/tla-bin.git
          cd tla-bin
          ./download_or_update_tla.sh --nightly
          sudo ./install.sh
      - name: Sany
        run: sany *.tla
      - name: Random exploration with TLC
        run: tlc -workers auto -generate num=1000 -depth 25 MCpbft.tla