Adjust module name in README and invariant script

cosmos · Oct 11, 2023 · 852dac4 · 852dac4
1 parent 13a32fc
commit 852dac4
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 7 deletions.
diff --git a/tests/difference/core/quint_model/README.md b/tests/difference/core/quint_model/README.md
@@ -22,18 +22,18 @@ The parameters of the protocol are defined as consts in [ccv.qnt](ccv.qnt).
 
 To run unit tests, run 
 ```
-quint test ccv_test.qnt --main CCVTest
+quint test ccv_test.
 ```
 and 
 ```
-quint test ccv_statemachine.qnt --main CCVDefaultStateMachine
+quint test ccv_statemachine.qnt
 ```
 
 ### Invariants
 
 The invariants to check are in [ccv_statemachine.qnt](ccv_statemachine.qnt).
 Check a single invariant by running
-`quint run --invariant INVARIANT_NAME ccv_statemachine.qnt --main CCVDefaultStateMachine`,
+`quint run --invariant INVARIANT_NAME ccv_statemachine.qnt`,
 or all invariants one after another with the help of the script `run_invariants.sh`.
 Each invariant takes about a minute to run.
 
@@ -53,7 +53,7 @@ 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 ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv \
---main CCVDefaultStateMachine ccv_statemachine.qnt
+ ccv_statemachine.qnt
 ```
 
 ### Sanity Checks
@@ -63,7 +63,7 @@ In detail, they are invariant checks that we expect to fail.
 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`.
+They are run like invariant checks, i.e. `quint run --invariant SANITY_CHECK_NAME ccv_statemachine.qnt`.
 The available sanity checks are:
 - CanRunConsumer
 - CanStopConsumer

diff --git a/tests/difference/core/quint_model/run_invariants.sh b/tests/difference/core/quint_model/run_invariants.sh
@@ -1,4 +1,4 @@
 #! /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
+quint test ccv_statemachine.qnt
+quint run --invariant "all{ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" ccv_statemachine.qnt --max-steps 500 --max-samples 200