Skip to content

Commit

Permalink
Add mbt to makefile and CI
Browse files Browse the repository at this point in the history
  • Loading branch information
p-offtermatt committed Nov 30, 2023
1 parent 4c74bcb commit fc48575
Show file tree
Hide file tree
Showing 3 changed files with 16 additions and 8 deletions.
10 changes: 8 additions & 2 deletions .github/workflows/test.yml
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,7 @@ jobs:
name: "${{ github.sha }}-integration-coverage"
path: ./integration-profile.out

test-difference:
test-mbt:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
Expand All @@ -99,6 +99,12 @@ jobs:
check-latest: true
cache: true
cache-dependency-path: go.sum
- uses: actions/setup-node@v4
with:
node-version: ">= 18"
check-latest: true
cache: 'npm'
- run: npm i @informalsystems/quint -g
- uses: technote-space/[email protected]
id: git_diff
with:
Expand Down Expand Up @@ -145,7 +151,7 @@ jobs:
- uses: actions/download-artifact@v3
if: env.GIT_DIFF
with:
name: "${{ github.sha }}-difference-coverage"
name: "${{ github.sha }}-mbt-coverage"
continue-on-error: true
- name: sonarcloud
if: ${{ env.GIT_DIFF && !github.event.pull_request.draft }}
Expand Down
4 changes: 3 additions & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,9 @@ test-integration-cov:

# run mbt tests
test-mbt:
go test ./tests/mbt/... -timeout 30m
cd tests/mbt/driver;\
sh generate_traces.sh;\
go test ./... -timeout 30m

test-mbt-cov:
go test ./tests/mbt/... -timeout 30m -coverpkg=./... -coverprofile=mbt-profile.out -covermode=atomic
Expand Down
10 changes: 5 additions & 5 deletions tests/mbt/driver/generate_traces.sh
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
echo "Generating bounded drift traces with timeouts"
go run ./... -modelPath=../model/ccv_boundeddrift.qnt -step stepBoundedDrift -invariant CanTimeoutConsumer -traceFolder traces/bound_timeout -numTraces 10 -numSteps 200 -numSamples 200
go run ./... -modelPath=../model/ccv_boundeddrift.qnt -step stepBoundedDrift -invariant CanTimeoutConsumer -traceFolder traces/bound_timeout -numTraces 2 -numSteps 200 -numSamples 200
echo "Generating long bounded drift traces without invariants"
go run ./... -modelPath=../model/ccv_boundeddrift.qnt -step stepBoundedDrift -traceFolder traces/bound_noinv -numTraces 10 -numSteps 500 -numSamples 1
go run ./... -modelPath=../model/ccv_boundeddrift.qnt -step stepBoundedDrift -traceFolder traces/bound_noinv -numTraces 2 -numSteps 500 -numSamples 1
echo "Generating bounded drift traces with maturations"
go run ./... -modelPath=../model/ccv_boundeddrift.qnt -step stepBoundedDrift -invariant CanReceiveMaturations -traceFolder traces/bound_mat -numTraces 10 -numSteps 100 -numSamples 20
go run ./... -modelPath=../model/ccv_boundeddrift.qnt -step stepBoundedDrift -invariant CanReceiveMaturations -traceFolder traces/bound_mat -numTraces 2 -numSteps 100 -numSamples 20
echo "Generating synced traces with maturations"
go run ./... -modelPath=../model/ccv_sync.qnt -init initHappy -step stepHappy -invariant CanReceiveMaturations -traceFolder traces/sync_mat -numTraces 10 -numSteps 300 -numSamples 20
go run ./... -modelPath=../model/ccv_sync.qnt -init initHappy -step stepHappy -invariant CanReceiveMaturations -traceFolder traces/sync_mat -numTraces 2 -numSteps 300 -numSamples 20
echo "Generating long synced traces without invariants"
go run ./... -modelPath=../model/ccv_sync.qnt -init initHappy -step stepHappy -traceFolder traces/sync_noinv -numTraces 10 -numSteps 500 -numSamples 1
go run ./... -modelPath=../model/ccv_sync.qnt -init initHappy -step stepHappy -traceFolder traces/sync_noinv -numTraces 2 -numSteps 500 -numSamples 1

0 comments on commit fc48575

Please sign in to comment.