Skip to content

Commit

Permalink
Rename statemachine to model
Browse files Browse the repository at this point in the history
  • Loading branch information
p-offtermatt committed Oct 16, 2023
1 parent 6ed82c8 commit 38010c8
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 8 deletions.
12 changes: 6 additions & 6 deletions tests/difference/core/quint_model/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ This folder contains a Quint model for the core logic of Cross-Chain Validation
The files are as follows:
- ccv.qnt: Contains the type definitions, data structures, functional logic for CCV.
The core of the protocol.
- ccv_statemachine.qnt: Contains the state machine layer for CCV. Very roughly speaking, this could be seen as "e2e tests".
- ccv_model.qnt: Contains the stateful part of the model for CCV. Very roughly speaking, this could be seen as "e2e tests".
Also contains invariants.
- ccv_test.qnt: Contains unit tests for the functional layer of CCV.
- libraries/*: Libraries that don't belong to CCV, but are used by it.
Expand All @@ -26,14 +26,14 @@ quint test ccv_test.qnt
```
and
```
quint test ccv_statemachine.qnt
quint test ccv_model.qnt
```

### Invariants

The invariants to check are in [ccv_statemachine.qnt](ccv_statemachine.qnt).
The invariants to check are in [ccv_model.qnt](ccv_model.qnt).
Check a single invariant by running
`quint run --invariant INVARIANT_NAME ccv_statemachine.qnt`,
`quint run --invariant INVARIANT_NAME ccv_model.qnt`,
or all invariants one after another with the help of the script `run_invariants.sh`.
Each invariant takes about a minute to run.

Expand All @@ -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 \
ccv_statemachine.qnt
ccv_model.qnt
```

### Sanity Checks
Expand All @@ -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`.
They are run like invariant checks, i.e. `quint run --invariant SANITY_CHECK_NAME ccv_model.qnt`.
The available sanity checks are:
- CanRunConsumer
- CanStopConsumer
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// -*- mode: Bluespec; -*-
module ccv_statemachine {
// A basic state machine that utilizes the CCV protocol.
module ccv_model {
// A basic stateful model that utilizes the CCV protocol.
import ccv_types.* from "./ccv"
import Time.* from "./libraries/Time"
import extraSpells.* from "./libraries/extraSpells"
Expand Down

0 comments on commit 38010c8

Please sign in to comment.