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

Replace difftests with model-based testing using Quint #1368

Closed
wants to merge 83 commits into from
Closed

Replace difftests with model-based testing using Quint #1368

wants to merge 83 commits into from

Conversation

p-offtermatt
Copy link
Contributor

Please go the the Preview tab and select the appropriate sub-template:

  • Production code - for types fix, feat, and refactor.
  • Docs - for documentation changes.
  • Others - for changes that do not affect production code.

p-offtermatt and others added 30 commits August 17, 2023 15:48
@p-offtermatt
Start new attempt on Quint model of ICS
e2b6407
@p-offtermatt
Advance quint model
283dc0a
@p-offtermatt
Add first finished draft of model
2155a4f
@p-offtermatt
Add test run to model
6ca6510
@p-offtermatt
Rename model, add test, use powerset for nondeterminism
e27e74b
@p-offtermatt
Reintroduce vsc changed tracking variables
50fae34
@p-offtermatt
Add text with what expliticly is modelled
78e890a
@p-offtermatt
Add bluespec to ccv.qnt
a1d57ef
@p-offtermatt
Add bluespec to expraSpells.qnt
6c91866
@p-offtermatt
Add docstring to extraSpells module
2126eac
@p-offtermatt
Start rewriting model
1320b95
@p-offtermatt
Revert "Start rewriting model"
5fa449c 
This reverts commit 1320b95.
@p-offtermatt
Start rewriting quint model
c05d9e6
@p-offtermatt
Continue seperating logic in Quint model
4bbe033
@p-offtermatt
Start debugging cryptic error message
5ebab39
@p-offtermatt
Start adding endAndBeginBlock defs
5bca6fc
@p-offtermatt
Diagnose Quint parser bug
4f77d68
@p-offtermatt
Fix type in Quint
fa233d6
@p-offtermatt
Add endBlock actions
66663bf
@p-offtermatt
Start adding state machine module
7b489fe
@p-offtermatt
Save status with crashing effect checker
b992f8c
@p-offtermatt
Resolve issue by removing undefined field
baaddb7
@p-offtermatt
Remove add
2c1341d
@p-offtermatt
Fix init
e09968d
@p-offtermatt
Snapshot spec with parser crasher
55ab595
@p-offtermatt
Snapshot model
0897e8c
@p-offtermatt
Start debugging tests
d227aee
@p-offtermatt
Finish test for quint model
09b1b87
@p-offtermatt
Add README and improve folder structure
96c101f
@p-offtermatt
Fix import
aa2989e
p-offtermatt and others added 27 commits October 10, 2023 12:57
@p-offtermatt
Rename VSC to Vsc
dc7e687
@p-offtermatt
Return plain ProtocolState in cases where no error is returned anyways
728b024
@p-offtermatt
Remove unused defs
641d845
@p-offtermatt
Fix indentation
c2aa6d0
@p-offtermatt
Rename to isRunningConsumer
75b1e11
@p-offtermatt
Unify naming for extraSpells
f46554b
@p-offtermatt
Remove HasSubsequence
3630846
@p-offtermatt
Run tests before running invariants
90f6652
@p-offtermatt
Rename modules to have same name as files
13a32fc
@p-offtermatt
Adjust module name in README and invariant script
852dac4
@p-offtermatt
Fix voting power change behaviour around 0
8aee401
@p-offtermatt
Adjust error message in test
d75d5c5
@p-offtermatt
Remove special treatment of 0 voting power
f294eec
@p-offtermatt
Rename sentVscPackets to sentVscPacketsToConsumer
4d87372
@p-offtermatt @insumity
Update tests/difference/core/quint_model/README.md
53d5bff 
Co-authored-by: insumity <[email protected]>
@p-offtermatt
Resolve comments
738a347
@p-offtermatt
Merge branch 'ph/quint-model-v2' of https://github.com/cosmos/interch…
c7fe7c5 
…ain-security into ph/quint-model-v2
@p-offtermatt
Adjust comment to fit actual time advancement
3a03fcd
@p-offtermatt
Remove hasError field and make it a function
d71dad3
@p-offtermatt
Adjust docstring
455696a
@p-offtermatt
Remove unused timedout val
d422cb4
@p-offtermatt
Update doc
6ed82c8
@p-offtermatt
Rename statemachine to model
b817f43
@p-offtermatt
Use ... syntax
70cd774
@p-offtermatt
Change Error type to string
86324b7
@p-offtermatt
Start adding mbt using Quint model
b856081
@p-offtermatt
Merge branch 'main' into ph/mbt
234a89e
@github-actions github-actions bot added the C:Testing Assigned automatically by the PR labeler label Oct 19, 2023
@p-offtermatt p-offtermatt deleted the ph/mbt branch October 19, 2023 08:10
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
C:Testing Assigned automatically by the PR labeler
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
1 participant
@p-offtermatt