// 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)
package mbt