Skip to content

[release/4.x] Cherry pick: Upgrade base to open enclave 0.19.7 (#6293… #1986

[release/4.x] Cherry pick: Upgrade base to open enclave 0.19.7 (#6293…

[release/4.x] Cherry pick: Upgrade base to open enclave 0.19.7 (#6293… #1986

Workflow file for this run

name: "TLA+ Spec Verification"
on:
push:
paths:
- "tla/**"
pull_request:
paths:
- "tla/**"
workflow_dispatch:
jobs:
model-checking-consensus:
name: Model Checking - Consensus
runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub]
container:
image: ccfmsrc.azurecr.io/ccf/ci:2024-06-26-virtual-clang15
steps:
- uses: actions/checkout@v3
- run: |
sudo apt update
sudo apt install -y default-jre
python3 ./tla/install_deps.py
- name: MCccfraft.cfg
run: |
cd tla/
./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft.trace.tla -dumpTrace json MCccfraft.json
- name: MCccfraftWithReconfig.cfg
run: |
cd tla/
./tlc.sh -workers auto -config consensus/MCccfraftWithReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftWithReconfig.trace.tla -dumpTrace json MCccfraftWithReconfig.json
- name: Upload traces in TLA and JSON format
uses: actions/upload-artifact@v3
if: ${{ failure() }}
with:
name: tlc
path: |
tla/consensus/*_TTrace_*.tla
tla/consensus/*_TTrace_*.bin
tla/*.trace.tla
tla/*.json
simulation-consensus:
name: Simulation - Consensus
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- run: python3 ./tla/install_deps.py
- name: SIMccfraft.tla
run: |
cd tla/
./tlc.sh -workers auto -simulate -depth 500 consensus/SIMccfraft.tla -dumpTrace tla SIMccfraft.trace.tla -dumpTrace json SIMccfraft.json
- name: Upload traces in TLA and JSON format
uses: actions/upload-artifact@v3
if: ${{ failure() }}
with:
name: tlc
path: |
tla/consensus/*_TTrace_*.tla
tla/consensus/*_TTrace_*.bin
tla/*.trace.tla
tla/*.json
model-checking-consistency:
name: Model Checking - Consistency
runs-on: [self-hosted, 1ES.Pool=gha-virtual-ccf-sub]
container:
image: ccfmsrc.azurecr.io/ccf/ci:25-01-2024-virtual-clang15
steps:
- uses: actions/checkout@v3
- run: |
sudo apt update
sudo apt install -y default-jre
python3 ./tla/install_deps.py
- name: consistency/MCSingleNode.cfg
run: |
cd tla/
./tlc.sh -workers auto consistency/MCSingleNode.tla -dumpTrace json MCSingleNode.json
- name: consistency/MCSingleNodeReads.cfg
run: |
cd tla/
./tlc.sh -workers auto consistency/MCSingleNodeReads.tla -dumpTrace json MCSingleNodeReads.json
- name: consistency/MCMultiNode.cfg
run: |
cd tla/
./tlc.sh -workers auto consistency/MCMultiNode.tla -dumpTrace json MCMultiNode.json
- name: MCccfraft.tla
run: |
set -exo pipefail
cd tla/
java -XX:+UseParallelGC -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=be29f6283abeed2fb1fd0be898bc6601 -cp tla2tools.jar tlc2.TLC -workers auto -lncheck final -checkpoint 60 -coverage 60 -tool MCccfraft.tla 2>&1 | tee MCccfraft.out
- name: MCccfraftWithReconfig.tla
run: |
set -exo pipefail
cd tla/
java -XX:+UseParallelGC -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=be29f6283abeed2fb1fd0be898bc6601 -cp tla2tools.jar tlc2.TLC -workers auto -lncheck final -checkpoint 60 -coverage 60 -tool -config MCccfraft.cfg MCccfraftWithReconfig.tla 2>&1 | tee MCccfraftWithReconfig.out
- name: Upload TLC's out file as an artifact. Can be imported into the TLA+ Toolbox.
uses: actions/upload-artifact@v2
if: ${{ failure() }}
with:
name: tlc
path: tla/*.out
simulation:
name: Simulation
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- run: python ./tla/install_deps.py
- name: SIMccfraft.tla
run: |
set -exo pipefail
cd tla/
java -XX:+UseParallelGC -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=be29f6283abeed2fb1fd0be898bc6601 -cp tla2tools.jar tlc2.TLC -workers auto -lncheck final -checkpoint 60 -coverage 60 -tool -simulate -depth 500 SIMccfraft.tla 2>&1 | tee SIMccfraft.out
- name: Upload TLC's out file as an artifact. Can be imported into the TLA+ Toolbox.
uses: actions/upload-artifact@v2
if: ${{ failure() }}
with:
name: tlc
path: tla/*.out