Inductive invariant validation. #66
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-check: | |
| 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: | |
| name: apalache-check | |
| path: | | |
| _apalache-out/ | |
| apalache-check-inductive: | |
| 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: Partial inductive invariant checking with Apalache | |
| if: always() | |
| run: | | |
| # Check that Init => SafetyInv | |
| ./apalache/bin/apalache-mc check --config=APApbft.cfg --init=GenInit --inv=SafetyInv --length=0 APAIndpbft.tla | |
| # Check that SafetyInv /\ Next => SafetyInv' | |
| ./apalache/bin/apalache-mc check --config=APApbft.cfg --init=GenInit --inv=SafetyInv --length=1 APAIndpbft.tla | |
| - name: Upload Apalache's counterexample (if any) | |
| uses: actions/upload-artifact@v4 | |
| if: always() | |
| with: | |
| name: apalache-check-inductive | |
| path: | | |
| _apalache-out/ | |
| apalache-simulate: | |
| 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 simulate --config=APApbft.cfg --length=25 APApbft.tla | |
| - name: Upload Apalache's counterexample (if any) | |
| uses: actions/upload-artifact@v4 | |
| if: always() | |
| with: | |
| name: apalache-simulate | |
| path: | | |
| _apalache-out/ | |
| tlc-generate: | |
| 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 generation with TLC | |
| run: JAVA_OPTS="-Dtlc2.TLC.stopAfter=600 -XX:+UseParallelGC" tlc -workers auto -generate MCpbft.tla | |
| tlc-simulate: | |
| 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 simulation with TLC | |
| run: JAVA_OPTS="-Dtlc2.TLC.stopAfter=600 -XX:+UseParallelGC" tlc -workers auto -simulate MCpbft.tla |