Run tests before running invariants

cosmos · Oct 10, 2023 · 90f6652 · 90f6652
1 parent 3630846
commit 90f6652
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/tests/difference/core/quint_model/run_invariants.sh b/tests/difference/core/quint_model/run_invariants.sh
@@ -1 +1,4 @@
-quint run --invariant "all{ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVSCPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" ccv_statemachine.qnt --main CCVDefaultStateMachine --max-steps 500 --max-samples 200 --out out.log
+#! /bin/sh
+
+quint test ccv_statemachine.qnt --main CCVDefaultStateMachine
+quint run --invariant "all{ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" ccv_statemachine.qnt --main CCVDefaultStateMachine --max-steps 500 --max-samples 200