From db16905a6ed126160173cd3123188271685a9795 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Wed, 22 Nov 2023 13:40:28 +0100 Subject: [PATCH] Add script for generating happy and normal traces --- .../difference/core/quint_model/driver/generate_happy_traces.sh | 1 + tests/difference/core/quint_model/driver/generate_traces.sh | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) create mode 100755 tests/difference/core/quint_model/driver/generate_happy_traces.sh diff --git a/tests/difference/core/quint_model/driver/generate_happy_traces.sh b/tests/difference/core/quint_model/driver/generate_happy_traces.sh new file mode 100755 index 0000000000..7dc347bd89 --- /dev/null +++ b/tests/difference/core/quint_model/driver/generate_happy_traces.sh @@ -0,0 +1 @@ +go run ./... -modelPath=../ccv_happy.qnt -init initHappy -step stepHappy -invariant CanReceiveMaturations -traceFolder traces -numTraces 50 \ No newline at end of file diff --git a/tests/difference/core/quint_model/driver/generate_traces.sh b/tests/difference/core/quint_model/driver/generate_traces.sh index 7dc347bd89..2b9a7b6b88 100755 --- a/tests/difference/core/quint_model/driver/generate_traces.sh +++ b/tests/difference/core/quint_model/driver/generate_traces.sh @@ -1 +1 @@ -go run ./... -modelPath=../ccv_happy.qnt -init initHappy -step stepHappy -invariant CanReceiveMaturations -traceFolder traces -numTraces 50 \ No newline at end of file +go run ./... -modelPath=../ccv_model.qnt -init init -step step -traceFolder traces -numTraces 50 \ No newline at end of file