-
Notifications
You must be signed in to change notification settings - Fork 329
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Model-based tests for ICS02 #601
Conversation
Codecov Report
@@ Coverage Diff @@
## master informalsystems/hermes#601 +/- ##
=========================================
+ Coverage 13.6% 46.8% +33.1%
=========================================
Files 69 150 +81
Lines 3752 10091 +6339
Branches 1374 0 -1374
=========================================
+ Hits 513 4725 +4212
- Misses 2618 5366 +2748
+ Partials 621 0 -621
Continue to review full report at Codecov.
|
5026721
to
70e70f6
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Impressive work!
My main worry is that we're introducing new TLA+ specs here, instead of leveraging (part of) what we already had. I'm curious what @ancazamfir, @andrey-kuprianov, and @istoilkovska think about this: would it be possible, at least eventually, to reuse Ilina's TLA+ specs for MBT?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good after a fist pass. Entered a few comments, will take another look.
Let's merge this one and address any pending comments in #633. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Good work Vitor!
Towards: cosmos/ibc-rs#30
Description
This PR is the first step towards cosmos/ibc-rs#30. For ease of reviewing, we plan to introduce one ICS at a time, starting now with ICS02.
For some details on MBT and current limitations, please check modules/tests/README.md (which steals ideas from the light-client one).
For contributor use:
docs/
) and code comments.Files changed
in the Github PR explorer.