From 90f6652ce1584fa4f02dd6c6bc53597b3b86c178 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Tue, 10 Oct 2023 16:47:39 +0200 Subject: [PATCH] Run tests before running invariants --- tests/difference/core/quint_model/run_invariants.sh | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/tests/difference/core/quint_model/run_invariants.sh b/tests/difference/core/quint_model/run_invariants.sh index 142095682f..5acd79e49c 100755 --- 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 \ No newline at end of file +#! /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 \ No newline at end of file