Files
tendermint/light/mbt/doc.go
Anton Kaliaev 8e6194626e light: model-based tests (#5461)
This is the first iteration of model-based testing in Go Tendermint. The test runner is using the static JSON fixtures located under the ./json directory. In the future, the Rust tensgen binary will be used to generate those (given the static intermediate scenarios and the test seed, which will be published along with each testgen release).

Closes: #5322
2020-11-02 12:07:18 +04:00

21 lines
1.0 KiB
Go

// 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