From 8b2906e3c399cb0f8d832a20b02e2b33795d7887 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Thu, 7 Mar 2024 10:55:23 +0100 Subject: [PATCH] Generate more traces, but less steps --- tests/mbt/driver/generate_traces.sh | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/tests/mbt/driver/generate_traces.sh b/tests/mbt/driver/generate_traces.sh index 9f1134fb26..e64bd146bf 100755 --- a/tests/mbt/driver/generate_traces.sh +++ b/tests/mbt/driver/generate_traces.sh @@ -1,13 +1,13 @@ #!/bin/bash echo "Generating bounded drift traces with timeouts" -go run ./... -modelPath=../model/ccv_boundeddrift.qnt -step stepBoundedDrift -invariant CanTimeoutConsumer -traceFolder traces/bound_timeout -numTraces 1 -numSteps 200 -numSamples 200 +go run ./... -modelPath=../model/ccv_boundeddrift.qnt -step stepBoundedDrift -invariant CanTimeoutConsumer -traceFolder traces/bound_timeout -numTraces 2 -numSteps 30 -numSamples 200 echo "Generating long bounded drift traces without invariants" -go run ./... -modelPath=../model/ccv_boundeddrift.qnt -step stepBoundedDrift -traceFolder traces/bound_noinv -numTraces 1 -numSteps 500 -numSamples 1 +go run ./... -modelPath=../model/ccv_boundeddrift.qnt -step stepBoundedDrift -traceFolder traces/bound_noinv -numTraces 2 -numSteps 30 -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 1 -numSteps 100 -numSamples 20 +go run ./... -modelPath=../model/ccv_boundeddrift.qnt -step stepBoundedDrift -invariant CanReceiveMaturations -traceFolder traces/bound_mat -numTraces 2 -numSteps 30 -numSamples 20 echo "Generating synced traces with maturations" -go run ./... -modelPath=../model/ccv_sync.qnt -init initSync -step stepSync -invariant CanReceiveMaturations -traceFolder traces/sync_mat -numTraces 1 -numSteps 300 -numSamples 20 +go run ./... -modelPath=../model/ccv_sync.qnt -init initSync -step stepSync -invariant CanReceiveMaturations -traceFolder traces/sync_mat -numTraces 2 -numSteps 30 -numSamples 20 echo "Generating long synced traces without invariants" -go run ./... -modelPath=../model/ccv_sync.qnt -init initSync -step stepSync -traceFolder traces/sync_noinv -numTraces 1 -numSteps 500 -numSamples 1 -go run ./... -modelPath=../model/ccv_boundeddrift.qnt --step stepBoundedDriftKeyAssignment --traceFolder traces/bound_key -numTraces 1 -numSteps 100 -numSamples 20 \ No newline at end of file +go run ./... -modelPath=../model/ccv_sync.qnt -init initSync -step stepSync -traceFolder traces/sync_noinv -numTraces 2 -numSteps 30 -numSamples 1 +go run ./... -modelPath=../model/ccv_boundeddrift.qnt --step stepBoundedDriftKeyAssignment --traceFolder traces/bound_key -numTraces 2 -numSteps 30 -numSamples 20 \ No newline at end of file