From 1bc4610ec05b8d32baf590d44b989e0ef2727a0a Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Mon, 2 Oct 2023 13:46:16 +0200 Subject: [PATCH] Add model checking to README --- tests/difference/core/quint_model/README.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/tests/difference/core/quint_model/README.md b/tests/difference/core/quint_model/README.md index 9c2197170e..7687c50036 100644 --- a/tests/difference/core/quint_model/README.md +++ b/tests/difference/core/quint_model/README.md @@ -50,6 +50,12 @@ with a timestamp >= t + UnbondingPeriod on that consumer. - [X] EventuallyMatureOnProviderInv: If we send a VSCPacket, this is eventually responded to by all consumers 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 +``` + ### Sanity Checks Sanity checks verify that certain patterns of behaviour can appear in the model.