Run experiments with APALACHE on the Relayer TLA+ spec

[istoilkovska]

Summary

The properties in the current Relayer TLA+ spec are checked with TLC. We should experiment with APALACHE as well.

Problem Definition

TLC takes a long time, even for small values of the chain height. For example, running TLC on the Relayer TLA+ spec in a configuration with two relayers that create client, connection handshake, and channel opening handshake, for height 2, produces the following result for the properties ICS18Delivery and ICS18Safety:

• total states: 5.046.661
• distinct states: 388.895
• diameter: 29
• time: 26h11min40s

We anticipate that checking invariants with APALACHE should be faster.

Proposal

The goal is to identify invariants, and try to check them with APALACHE. Reporting on the experience of running APALACHE would also be useful to the APALACHE team, as they are aiming at improving the user experience.

---

For Admin Use

• Not duplicate issue
• Appropriate labels applied
• Appropriate contributors tagged
• Contributor assigned/self-assigned

[josef-widder]

@konnov @andrey-kuprianov

[ebuchman]

time: 26h11min40s

Lol wow. We're also going to want to leverage model based testing here

[konnov]

The number of states is actually not large. Do you know where the complexity is coming from? Maybe you first try apalache and tell us about all the bumps. Then we can go over it together and see where things could be made faster.