Documentation
¶
Overview ¶
Package mbt provides a test runner for model-based tests
Model-based tests are generated by https://github.com/informalsystems/tendermint-rs/tree/master/testgen, which first turns TLA+ specifications into test scenarios. Those test scenarios are then in turn used to generate actual fixtures representing light blocks.
The test runner initializes the light client with a trusted light block. For each next light block, it tries to verify the block and asserts the outcome ("verdict" field in .json files).
In the first version (v1), JSON files are directly added to the repo. In the future (v2), they will be generated by the testgen binary right before testing on CI (the number of files will be around thousands).
NOTE (v1): If a breaking change is introduced into the SignedHeader or ValidatorSet, you will need to regenerate the JSON files using testgen binary (may also require modifying tendermint-rs, e.g. https://github.com/informalsystems/tendermint-rs/pull/647)
Source Files