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: Typecheck
        run: |
          ./apalache/bin/apalache-mc typecheck --features=no-rows MCpbft.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
          sudo ./install.sh
      - name: Sany
        run: sany *.tla
      - name: Random exploration with TLC
        run: tlc -workers auto -simulate num=1000 MCpbft.tla