Skip to content

Commit

Permalink
Update tests/difference/core/quint_model/README.md
Browse files Browse the repository at this point in the history
Co-authored-by: insumity <[email protected]>
  • Loading branch information
p-offtermatt and insumity authored Oct 6, 2023
1 parent 7cd826b commit 7df2b1f
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion tests/difference/core/quint_model/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ quint verify --invariant ValidatorUpdatesArePropagatedInv,ValidatorSetHasExisted

Sanity checks verify that certain patterns of behaviour can appear in the model.
In detail, they are invariant checks that we expect to fail.
They usually negate the appearance of some behaviour, i.e. not(DesirableBehaviour).
They usually negate the appearance of some behaviour, i.e. `not(DesirableBehaviour)`.
Then, a counterexample for this is an example trace exhibiting the behaviour.

They are run like invariant checks, i.e. `quint run --invariant SANITY_CHECK_NAME ccv_statemachine.qnt --main CCVDefaultStateMachine`.
Expand Down

0 comments on commit 7df2b1f

Please sign in to comment.