MBT: check that the chain state (height, clients, connections, ...) matches the one in the model

[vitorenesduarte]

Crate

modules

Problem Definition

MBT is coming in #601, but in a very limited form. After performing each model action and checking that the outcomes match, we only check that the height of each chain matches the one in the model. This last step can be extended to check that the state of each client also matches (same for connections once we have ICS03, and so on). Doing so is not so easy as easy-to-parse counterexamples are not yet generated automatically.

Proposal

Easy-to-parse counterexamples are coming (apalache-mc/apalache#530), at which point we can easily extend what's being checked with MBT.

---

For Admin Use

• Not duplicate issue
• Appropriate labels applied
• Appropriate milestone (priority) applied
• Appropriate contributors tagged
• Contributor assigned/self-assigned