Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Rewrite the TLA+ ICS model in Quint (see https://github.com/cosmos/ibc/pull/911) #1239

Closed
Tracked by #1238
p-offtermatt opened this issue Aug 25, 2023 · 0 comments · Fixed by #1336
Closed
Tracked by #1238

Rewrite the TLA+ ICS model in Quint (see https://github.com/cosmos/ibc/pull/911) #1239

p-offtermatt opened this issue Aug 25, 2023 · 0 comments · Fixed by #1336
Assignees
@p-offtermatt
Labels
S: Productivity Productivity: Developer tooling, infrastructure improvements enabling future growth scope: testing Code review, testing, making sure the code is following the specification.

Comments

@p-offtermatt
Copy link
Contributor

p-offtermatt commented Aug 25, 2023 •
edited
Loading

To make a step towards replacing the existing difftest model in model-based testing, we want to have a simpler model of ICS in Quint.
We chose to rewrite the existing TLA+ model in Quint, see cosmos/ibc#911
The Quint model is not supposed to be an exact replica, but to capture roughly the same part of the protocol at the same abstraction level and complexity.

Closing Criteria
The TLA+ model has been rewritten in Quint.
@p-offtermatt p-offtermatt mentioned this issue Aug 25, 2023
Closed
@p-offtermatt p-offtermatt self-assigned this Aug 25, 2023
@p-offtermatt p-offtermatt added the scope: testing Code review, testing, making sure the code is following the specification. label Aug 25, 2023
@p-offtermatt p-offtermatt mentioned this issue Aug 25, 2023
Closed
8 tasks
@p-offtermatt p-offtermatt added the S: Productivity Productivity: Developer tooling, infrastructure improvements enabling future growth label Sep 8, 2023
@p-offtermatt p-offtermatt mentioned this issue Sep 29, 2023
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@p-offtermatt p-offtermatt

Labels
S: Productivity Productivity: Developer tooling, infrastructure improvements enabling future growth scope: testing Code review, testing, making sure the code is following the specification.
Projects
Cosmos Hub
Status: ✅ Done
Milestone
No milestone
1 participant
@p-offtermatt