#414: factor out common parts from tests/lite.rs into tests/lite_tests

andrey-kuprianov committed Jul 31, 2020

#414: lite_tests: add Command/CommandRun wrapper for running external… …

… commands (e.g. apalache, jsonatr)

andrey-kuprianov committed Jul 31, 2020

#414: add history variables to Lightclient_A_1.tla

andrey-kuprianov committed Aug 4, 2020

#414: add use default index in testgen vote

andrey-kuprianov committed Aug 4, 2020

#414: add first model-based test …

* defined structure for model-based single-step light client tests
* added a simple driver for such tests modeled after original one in
tests/lite.rs
* add the first auto-generated model-based test
* add symlinks to the TLA+ model

The important change in the test structure is that now each input block
carries with it the expected verdict, not a single expected result for the whole
input array: the latter is unclear how to interpret in case of failures.

Besides, having such more fine-grained verdicts allows to differentialte
between different types of errors returned by the light client.

andrey-kuprianov committed Aug 4, 2020

#414: more structure for test cases

andrey-kuprianov committed Aug 5, 2020

#414: simplify running external commands

andrey-kuprianov committed Aug 6, 2020

#414: add simple TLA+ test

andrey-kuprianov committed Aug 6, 2020

#414: run apalache on TLA+ test; fix Command spawn errors

andrey-kuprianov committed Aug 6, 2020

#414: fix small typos

andrey-kuprianov committed Aug 6, 2020

#414: refactor: add commonly used test utils

andrey-kuprianov committed Aug 6, 2020

#414: more refactoring

andrey-kuprianov committed Aug 6, 2020

#414: add tests/utils/jsonatr.rs

andrey-kuprianov committed Aug 7, 2020

#414: add tests/utils/jsonatr-lib

andrey-kuprianov committed Aug 7, 2020

#414: full model-based test TLA+ -> Apalache -> Jsonatr -> lite::veri… …

…fy_single

andrey-kuprianov committed Aug 7, 2020

#414: check for tendermint-testgen in PATH

andrey-kuprianov committed Aug 7, 2020

#414: testgen: add absent votes in the commit

andrey-kuprianov committed Aug 10, 2020

#414: testgen: add time command; make timestamps abstract

andrey-kuprianov committed Aug 10, 2020

#414: make lite test timestamps abstract

andrey-kuprianov committed Aug 10, 2020

#414: LightClient_A_1: add time to history variables

andrey-kuprianov committed Aug 10, 2020

#414: Blockchain_A_1.tla: fix discrepancy between the model and the … …

…implementation

In the current model (Blockchain_A_1.tla) the check InTrustingPeriod
treats the edge case now = header.time + TRUSTING_PERIOD as valid,
while the implementation treats it as invalid.
`
Changed the model to follow the implementation.

andrey-kuprianov committed Aug 10, 2020

#414: Lightclient_A_1.tla: store whole state sequence in history

andrey-kuprianov committed Aug 10, 2020

#414: more TLA+ lite tests

andrey-kuprianov committed Aug 10, 2020

#414: Blockchain_A_1.tla: disallow generating headers with negative time

andrey-kuprianov committed Aug 11, 2020

#414 adjust static test to the new format

andrey-kuprianov committed Aug 11, 2020

#414 adapt jsonatr-lib to history variables in the lite model

andrey-kuprianov committed Aug 11, 2020

#414 testgen header: handle the case of empty validators

andrey-kuprianov committed Aug 11, 2020

#414 lite-model-based: account for apalache run w/o counterexample

andrey-kuprianov committed Aug 11, 2020

#414: auto-run model-based test batches

andrey-kuprianov committed Aug 11, 2020

#414: add first test batch

andrey-kuprianov committed Aug 11, 2020

#414 Merge branch 'master' into andrey/lite-model-based

andrey-kuprianov committed Aug 12, 2020

Merge branch 'andrey/testgen-tester' into andrey/lite-model-based

andrey-kuprianov committed Aug 18, 2020

#414 move utilities for running commands into testgen

andrey-kuprianov committed Aug 18, 2020

#414 move model-based tests into light-client crate

andrey-kuprianov committed Aug 18, 2020

#414 move files around

andrey-kuprianov committed Aug 19, 2020

#414 cargo fmt

andrey-kuprianov committed Aug 19, 2020

#414: testgen/Tester: better handling of test environments …

* various utility functions for TestEnv
* use temporary directories to run tests

andrey-kuprianov committed Aug 19, 2020

#414: factor out verify_single/bisection into tests.rs

andrey-kuprianov committed Aug 19, 2020

#414 adapted LightClient model-based tests to the new testgen/tester

andrey-kuprianov committed Aug 19, 2020

#414 align LightClient spec verdicts with the implementation verdicts

andrey-kuprianov committed Aug 19, 2020

#414 add symlink to jsonatr-lib

andrey-kuprianov committed Aug 19, 2020

#414 Merge branch 'master' into andrey/lite-model-based

andrey-kuprianov committed Aug 19, 2020

#414 better handling of Apalache runs

andrey-kuprianov committed Aug 20, 2020

#414 adapt model-based tests to changes in LightClient model

andrey-kuprianov committed Aug 20, 2020

#414 testgen/tester: remove redundant test environments from function… …

… signatures

andrey-kuprianov committed Aug 20, 2020

#414 testgen/tester: add test batches

andrey-kuprianov committed Aug 20, 2020

#414 adapt LightClient model-based test to use test batches

andrey-kuprianov committed Aug 20, 2020

#414 adapt LightClient model to implementation: headers with equal ti… …

…me are considered invalid

andrey-kuprianov committed Aug 20, 2020

#414 model-based test: add model mutation to negate test into invariant

andrey-kuprianov committed Aug 20, 2020

#414 testgen/tester: add logging

andrey-kuprianov committed Aug 20, 2020

#414 testgen/tester: add reporting

andrey-kuprianov committed Aug 20, 2020

#414 testgen/tester: better reporting

andrey-kuprianov committed Aug 20, 2020

#414 cargo fmt

andrey-kuprianov committed Aug 20, 2020

#414 cargo clippy

andrey-kuprianov committed Aug 20, 2020

#414 shift model mutation and error messages from model-based test to… …

… apalache command run

andrey-kuprianov committed Aug 21, 2020

#414: remove first-model-based-test

andrey-kuprianov committed Aug 21, 2020

#414 add some static tests

andrey-kuprianov committed Aug 21, 2020

#414 add model-based README.md

andrey-kuprianov committed Aug 21, 2020

#414 update link in model-based README.md

andrey-kuprianov committed Aug 21, 2020

#414 cargo fmt

andrey-kuprianov committed Aug 21, 2020

#414 add some docs to testgen/Tester

andrey-kuprianov committed Aug 21, 2020

#414: remove redundant files

andrey-kuprianov committed Aug 21, 2020