Skip to content

Commit

Permalink
Generate more traces, but less steps
Browse files Browse the repository at this point in the history
p-offtermatt committed Mar 7, 2024
1 parent 12e69e1 commit 8b2906e
Showing 1 changed file with 6 additions and 6 deletions.
12 changes: 6 additions & 6 deletions tests/mbt/driver/generate_traces.sh
Original file line number Diff line number Diff line change
@@ -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
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

0 comments on commit 8b2906e

Please sign in to comment.