Improve light-client README

light-client/README.md

@@ -66,22 +66,14 @@ The Tendermint Light Client is primarily tested through unit tests.
 ### Core Verification
 
 The logic for the core verification of light blocks is entirely self-contained in
-the [`predicates`](./src/predicates.rs) module. This code is exercised in a family
-of tests called `single_step` via a set of [JSON fixtures](./tests/support/single_step)
-which encode an initial trusted state, a target block to verify, and the
-expected result of the core verification algorithm.
-
-These tests come in two flavours:
-
-- `skipping` tests, where there is a gap between the initial trusted state and the target block.
-- `sequential` tests, where there the initial trusted state and the target block are adjacent.
+the [`predicates`](./src/predicates.rs) module.
+This code is exercised through unit tests which test each predicate in isolation
+by giving it a set of data along with the expected outcome of each check.
 
 The following command can be used to run only these tests:
 
-TODO: the following runs 0 tests
-
 ```bash
-$ cargo test -p tendermint-light-client --test light_client single_step
+cargo test -p tendermint-light-client predicates
 ```
 
 #### Model-based tests

light-client/tests/model_based.rs

@@ -662,7 +662,11 @@ fn model_based_test(
         }
         true
     };
-    if !check_program("apalache-mc") || !check_program("jsonatr") || !check_program("timeout") {
+    if !check_program("tendermint-testgen")
+        || !check_program("apalache-mc")
+        || !check_program("jsonatr")
+        || !check_program("timeout")
+    {
         output_env.logln("    failed to find necessary programs; consider adding them to your PATH. skipping the test");
         return;
     }

light-client/tests/support/model_based/README.md

@@ -23,7 +23,7 @@ When you run `cargo test` some machinery will run under the hood, namely:
   takes care of translating abstract values from the model into the concrete implementation values.
 * `timeout` command is used to limit the test execution time.
 
-So, for the model-based test to run, the programs `apalache-mc`, `jsonatr`,
+So, for the model-based test to run, the programs `apalache-mc`, `jsonatr`, `tendermint-testgen`
 and `timeout` should be present in your `PATH`. 
 If any of the programs is not found, execution of a model-based test will be skipped.
 
@@ -48,6 +48,12 @@ $ cd jsonatr/
 $ cargo install --path .
 ```
 
+#### Installing `tendermint-testgen`
+
+```bash
+$ cargo install tendermint-testgen
+```
+
 #### Installing `timeout`
 `timeout` should be present by default on all Linux distributions, but may be absent on Macs. In that case it can be installed using `brew install coreutils`.