Add script for generating happy and normal traces

cosmos · Nov 22, 2023 · db16905 · db16905
1 parent c510e61
commit db16905
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/tests/difference/core/quint_model/driver/generate_happy_traces.sh 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
diff --git 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
+go run ./... -modelPath=../ccv_model.qnt -init init -step step -traceFolder traces -numTraces 50
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		go run ./... -modelPath=../ccv_happy.qnt -init initHappy -step stepHappy -invariant CanReceiveMaturations -traceFolder traces -numTraces 50
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		go run ./... -modelPath=../ccv_happy.qnt -init initHappy -step stepHappy -invariant CanReceiveMaturations -traceFolder traces -numTraces 50
		go run ./... -modelPath=../ccv_model.qnt -init init -step step -traceFolder traces -numTraces 50