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.

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

test: Replace difftest model with Quint=>MBT #1369

Merged
merged 117 commits into from
Dec 18, 2023
Merged
Changes from 1 commit
Commits
Show all changes
117 commits
Select commit Hold shift + click to select a range
a4840fc
Start adding mbt using Quint model
p-offtermatt Oct 19, 2023
5ffe647
Clean up dependencies
p-offtermatt Oct 19, 2023
5f96643
Start taking difftest code for mbt
p-offtermatt Nov 1, 2023
2285a4c
Implement chain startup
p-offtermatt Nov 2, 2023
ae5b106
Rewrite chain startup
p-offtermatt Nov 2, 2023
50231fb
Continue chain setup
p-offtermatt Nov 6, 2023
2d29208
Add trusting period
p-offtermatt Nov 6, 2023
81bcd3b
Adjust tests for fee testing
p-offtermatt Nov 7, 2023
eedcf46
Use correct validators in RequestInitChain
p-offtermatt Nov 7, 2023
1bb6ed0
Remove min and max functions
p-offtermatt Nov 7, 2023
065f458
Add type annotations
p-offtermatt Nov 8, 2023
b1fde43
Make state printing more robust
p-offtermatt Nov 8, 2023
44914e2
Fix setting default power reduction
p-offtermatt Nov 8, 2023
e9d7107
Adjust max steps and run all tests
p-offtermatt Nov 8, 2023
b8640d9
Change semantics of VotingPowerChange to take change amount, not new …
p-offtermatt Nov 8, 2023
a8f45c4
Adjust voting power choices to be changes instead of absolute values
p-offtermatt Nov 8, 2023
ef7a80e
Start refactoring relaying code
p-offtermatt Nov 8, 2023
6336273
Refactor map to list of pairs
p-offtermatt Nov 10, 2023
dd9d878
Add libraries for map rewrite
p-offtermatt Nov 10, 2023
61b6a85
Start fixing client updates
p-offtermatt Nov 10, 2023
abc12cf
Add ccv_happy module as a happyPath variant
p-offtermatt Nov 14, 2023
ad25029
Fix model: packets are emitted based on the timestamp of the last blo…
p-offtermatt Nov 16, 2023
fea71dc
Add viewer for ModelState and fix model-system equivalence checks
p-offtermatt Nov 16, 2023
8f8d2c4
Add type annotations
p-offtermatt Nov 20, 2023
6dacc09
Add ack delivery after each step
p-offtermatt Nov 22, 2023
2c3a6d5
Add programmatic ways of generating traces
p-offtermatt Nov 22, 2023
71a3b80
Make invariant optional
p-offtermatt Nov 22, 2023
c510e61
Pretty up the output
p-offtermatt Nov 22, 2023
db16905
Add script for generating happy and normal traces
p-offtermatt Nov 22, 2023
436aec4
Remove message sends for consumers that were started in this block
p-offtermatt Nov 23, 2023
5d17552
Use .itf extension instead of .json
p-offtermatt Nov 23, 2023
d085cce
Start adjusting behaviour for started/stopped consumers
p-offtermatt Nov 23, 2023
3a7564e
Use GetEmptyProtocolState instead of verbose declaration
p-offtermatt Nov 24, 2023
1b8ae7b
Add expired status and set timestamps of new consumers
p-offtermatt Nov 24, 2023
c7cba8b
Add note to split up timestamps
p-offtermatt Nov 24, 2023
2d130df
Advance MBT prototype
p-offtermatt Nov 24, 2023
8f31705
Add test case for expired clients
p-offtermatt Nov 27, 2023
8681895
Adjust tests for new timestamp handling
p-offtermatt Nov 28, 2023
f229db7
Use -1 as last timestamp when no block was comitted
p-offtermatt Nov 28, 2023
8bbb86a
Fix client expiration conditions
p-offtermatt Nov 28, 2023
9237c34
Start writing model with boundeddrift
p-offtermatt Nov 28, 2023
2b9873a
Add model with bounded drift
p-offtermatt Nov 28, 2023
dd2cd7c
Rename module to match filename
p-offtermatt Nov 28, 2023
603a668
Add extra log output and trace gen scripts
p-offtermatt Nov 28, 2023
719614c
Add Apalache output folder to gitignore
p-offtermatt Nov 28, 2023
468dc7f
Remove expired clients
p-offtermatt Nov 28, 2023
31bd231
Remove different time offsets for different chains
p-offtermatt Nov 29, 2023
76dcc15
Fix timestamp
p-offtermatt Nov 29, 2023
3286e09
Fix error where we would choose nondet from empty sets
p-offtermatt Nov 29, 2023
1433ee4
Add timeout timestamps to packets
p-offtermatt Nov 29, 2023
0f8228d
Adapt tests to the empty-validator-power behaviour
p-offtermatt Nov 29, 2023
6887906
Adjust timeout test
p-offtermatt Nov 29, 2023
ab1430a
Add logic for comparing timestamps of packets
p-offtermatt Nov 29, 2023
dbbe2b0
Fix: VSCTimeout is based on EndBlocj
p-offtermatt Nov 29, 2023
680f3c4
Add logic for timed out vsc packets
p-offtermatt Nov 29, 2023
4238978
Fix vsc timeouts should happen during endblock
p-offtermatt Nov 29, 2023
2d1a874
Revert the timestamp change
p-offtermatt Nov 29, 2023
bcdd85c
Add more diverse traces
p-offtermatt Nov 29, 2023
eacfd87
Fix acct sequences not incrementing when messages error ot
p-offtermatt Nov 30, 2023
33de97b
Move from difference folder to mbt folder
p-offtermatt Nov 30, 2023
0e584c3
Add back consumer chain stopping
p-offtermatt Nov 30, 2023
95e5253
Disallow empty validator sets
p-offtermatt Nov 30, 2023
d272b73
Add README and generate fewer traces
p-offtermatt Nov 30, 2023
5dcf517
merge in main
p-offtermatt Nov 30, 2023
684a2e5
Remove difftest link from old docs
p-offtermatt Nov 30, 2023
703e462
Fix merge conflicts
p-offtermatt Nov 30, 2023
b8db7bc
Revert changes to e2e tests
p-offtermatt Nov 30, 2023
ce62ab0
Fix link to MBT
p-offtermatt Nov 30, 2023
7eeb540
Tidy go mod and use go 1.20
p-offtermatt Nov 30, 2023
2a9c39b
Start linting
p-offtermatt Nov 30, 2023
b533d1f
Lint files
p-offtermatt Nov 30, 2023
4c205f6
Add nolint instruction from main
p-offtermatt Nov 30, 2023
4c74bcb
Do not check for errors for consumer chain stopping
p-offtermatt Nov 30, 2023
fc48575
Add mbt to makefile and CI
p-offtermatt Nov 30, 2023
680b9df
Move reference to difftests into reference to MBT
p-offtermatt Nov 30, 2023
10ced0a
Remove cache npm
p-offtermatt Nov 30, 2023
8bce148
Fix test-mbt-cov Make instructions
p-offtermatt Nov 30, 2023
d00a1cc
Generate less traces and fix path for testing
p-offtermatt Nov 30, 2023
df7ea65
Fix test path
p-offtermatt Nov 30, 2023
6b99c02
Archive traces in workflow
p-offtermatt Dec 1, 2023
e2ee8a2
Add long version of MBT to makefile
p-offtermatt Dec 1, 2023
0ac3c8a
Use variable instead of true to better signal semantics
p-offtermatt Dec 4, 2023
db9a697
Update testutil/simibc/chain_util.go
p-offtermatt Dec 4, 2023
bf2d8d5
Address comments
p-offtermatt Dec 5, 2023
064188e
Merge branch 'main' into ph/mbt
p-offtermatt Dec 5, 2023
d689142
Add punctuation remoced due to main merge
p-offtermatt Dec 6, 2023
e730ebf
Remove outdated doc line
p-offtermatt Dec 6, 2023
d103bda
Add Quint tests to CI
p-offtermatt Dec 8, 2023
5d97774
Update tests/mbt/model/ccv_model.qnt
p-offtermatt Dec 8, 2023
5fecff1
Address comments
p-offtermatt Dec 8, 2023
90acddc
Add zero check to VotingPowerChangeToEmptyTest
p-offtermatt Dec 8, 2023
1798924
Incorporate Karolos' comments
p-offtermatt Dec 8, 2023
30a79ad
Add spacing between jobs
p-offtermatt Dec 11, 2023
2396038
Update tests/mbt/model/ccv_model.qnt
p-offtermatt Dec 11, 2023
1659892
Address comments
p-offtermatt Dec 11, 2023
21813de
Remove 4 week time advancement
p-offtermatt Dec 11, 2023
a3df827
Upload traces even when test fails
p-offtermatt Dec 11, 2023
e52d186
Fix condition for trace archival
p-offtermatt Dec 11, 2023
b74a09f
Remove unused index
p-offtermatt Dec 11, 2023
e039ef9
Remove outdated for loop
p-offtermatt Dec 11, 2023
b13ead1
Fix if condition for trace upload
p-offtermatt Dec 11, 2023
e7807bf
Add comment about timestamps
p-offtermatt Dec 11, 2023
a052b21
Remove long time advancements
p-offtermatt Dec 11, 2023
60589a1
Address comments
p-offtermatt Dec 11, 2023
82ca137
Make comment clearer
p-offtermatt Dec 11, 2023
6d68920
Update tests/mbt/driver/generate_traces.sh
p-offtermatt Dec 15, 2023
49ba056
Update tests/mbt/run_invariants.sh
p-offtermatt Dec 15, 2023
d04e140
Update tests/mbt/driver/README.md
p-offtermatt Dec 15, 2023
f5f5d6e
Merge branch 'main' into ph/mbt
p-offtermatt Dec 15, 2023
4af62df
Merge branch 'main' into ph/mbt
p-offtermatt Dec 15, 2023
d01e561
Update testutil/simibc/relayed_path.go
p-offtermatt Dec 15, 2023
2a1db2b
Update tests/mbt/driver/generate_more_traces.sh
p-offtermatt Dec 15, 2023
2488377
Remove difftest folder
p-offtermatt Dec 15, 2023
357541f
Merge branch 'ph/mbt' of https://github.com/cosmos/interchain-securit…
p-offtermatt Dec 15, 2023
73ba96f
Minor fixes based on PR comments
p-offtermatt Dec 15, 2023
44e6145
Make timedout status a const
p-offtermatt Dec 18, 2023
7940d0f
Lengthen retention to 6 days
p-offtermatt Dec 18, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Update tests/mbt/driver/README.md
Co-authored-by: Simon Noetzlin <simon.ntz@gmail.com>
p-offtermatt and sainoe authored Dec 15, 2023
commit d04e1400b33758fc4b4fd1b8e8342c6fe686b067
2 changes: 1 addition & 1 deletion tests/mbt/driver/README.md
Original file line number Diff line number Diff line change
@@ -15,7 +15,7 @@ To generate traces, run

This will generate several "families" of traces in the `traces` folder.

Here is what one of the lines from `./generate traces` looks like:
Here is what one of the lines from `./generate_traces.sh` looks like:
```
go run ./... -modelPath=../model/ccv_boundeddrift.qnt -step stepBoundedDrift -invariant CanTimeoutConsumer -traceFolder traces/bound_timeout -numTraces 10 -numSteps 200 -numSamples 200
```