Add long version of MBT to makefile

.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]

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/...

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