You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
The text was updated successfully, but these errors were encountered:
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.
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:
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
The text was updated successfully, but these errors were encountered: