From e2ee8a297eb7089f0d50feb850d5725719837be0 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Fri, 1 Dec 2023 11:22:05 +0100 Subject: [PATCH] Add long version of MBT to makefile --- .github/workflows/test.yml | 3 ++- Makefile | 7 +++++++ tests/mbt/driver/generate_traces_long.sh | 10 ++++++++++ 3 files changed, 19 insertions(+), 1 deletion(-) create mode 100755 tests/mbt/driver/generate_traces_long.sh diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 9643c659d3..c7db082018 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -128,7 +128,8 @@ jobs: uses: actions/upload-artifact@v3 with: name: mbt-traces - path: tests/mbt/driver/traces + path: tests/mbt/driver/traces + retention-days: 2 repo-analysis: runs-on: ubuntu-latest needs: [tests, test-integration, test-mbt] diff --git a/Makefile b/Makefile index c5f817c0d7..9646bcae60 100644 --- a/Makefile +++ b/Makefile @@ -42,6 +42,13 @@ test-mbt-cov: cd ../../..;\ go test ./tests/mbt/... -timeout 30m -coverpkg=./... -coverprofile=mbt-profile.out -covermode=atomic +# runs mbt tests, but generates more traces +test-mbt-long: + cd tests/mbt/driver;\ + sh generate_traces_long.sh;\ + cd ../../..;\ + go test ./tests/mbt/... -timeout 30m + # run E2E tests test-e2e: go run ./tests/e2e/... diff --git a/tests/mbt/driver/generate_traces_long.sh b/tests/mbt/driver/generate_traces_long.sh new file mode 100755 index 0000000000..49089c5232 --- /dev/null +++ b/tests/mbt/driver/generate_traces_long.sh @@ -0,0 +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 20 -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 20 -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 20 -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 20 -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 20 -numSteps 500 -numSamples 1 \ No newline at end of file