Skip to content

Seperate MaxQuorums #48

Seperate MaxQuorums

Seperate MaxQuorums #48

Workflow file for this run

name: TLA
on:
push:
branches: [ "main" ]
pull_request:
branches: [ "main" ]
workflow_dispatch:
jobs:
tlc-simulate:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- name: Get (nightly) TLC
run: wget https://nightly.tlapl.us/dist/tla2tools.jar
- name: Get (nightly) CommunityModules
run: wget https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar
- name: Random simulation with TLC (crash)
run: java -Dtlc2.TLC.stopAfter=600 -XX:+UseParallelGC -jar tla2tools.jar -workers auto -simulate SIMpirateship.tla -config SIMpirateshipCrash.cfg
- name: Random simulation with TLC (byzantine)
run: java -Dtlc2.TLC.stopAfter=600 -XX:+UseParallelGC -jar tla2tools.jar -workers auto -simulate SIMpirateship.tla
tlc-verify:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- name: Get (nightly) TLC
run: wget https://nightly.tlapl.us/dist/tla2tools.jar
- name: Get (nightly) CommunityModules
run: wget https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar
- name: Exhaustive Verification with TLC
run: java -Dtlc2.TLC.stopAfter=600 -XX:+UseParallelGC -jar tla2tools.jar -workers auto -modelcheck MCpirateship.tla