From 2000272940a84186d9bdc32eaf22e1250e5c4090 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Fri, 6 Oct 2023 08:47:51 +0200 Subject: [PATCH] Correct verify command by adding \ --- tests/difference/core/quint_model/README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/difference/core/quint_model/README.md b/tests/difference/core/quint_model/README.md index 66e34fd947..a2f66945b4 100644 --- a/tests/difference/core/quint_model/README.md +++ b/tests/difference/core/quint_model/README.md @@ -52,8 +52,8 @@ that were running at the time the packet was sent (and are still running). Invariants can also be model-checked by Apalache, using this command: ``` -quint verify --invariant ValidatorUpdatesArePropagated,ValidatorSetHasExistedInv,SameVSCPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv --main CCVDefaultState -Machine ccv_statemachine.qnt +quint verify --invariant ValidatorUpdatesArePropagated,ValidatorSetHasExistedInv,SameVSCPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv \ +--main CCVDefaultStateMachine ccv_statemachine.qnt ``` ### Sanity Checks