Inductive invariant validation. #60
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 |