Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Develop a set of model-based tests for the LightClient #414

Closed
andrey-kuprianov opened this issue Jul 7, 2020 · 1 comment · Fixed by #525, #546, #547, #548 or #549
Closed

Develop a set of model-based tests for the LightClient #414

andrey-kuprianov opened this issue Jul 7, 2020 · 1 comment · Fixed by #525, #546, #547, #548 or #549
Assignees
@andrey-kuprianov
Labels
help wanted Extra attention is needed light-client Issues/features which involve the light client question Further information is requested
Milestone
v0.17.0

Comments

@andrey-kuprianov
Copy link
Contributor

Hi everyone!

Model-based testing is coming into shape: Apalache counterexamples can now be automatically translated into LightClient integrations tests: e.g., this spec transforms this counterexample into this test, which then can be used for testing the LightClient implementation using this driver.

The current MBT handles only single-step test cases, but now, when most of the infrastructure is in place, it should be relatively easy to extend it to bisection cases, for example. Besides, the above counterexample was produced from one of the earlier specs, but it should be also relatively easy to adapt the process to the most recent spec.

Now comes the creative part: we need to come up with testing scenarios, that can be encoded as spec invariants, model-checked with Apalache to get counterexamples, which then will be translated into tests. For a motivation about possible invariants, you can look here.

Formulating the invariants can be not an easy task, but if you come up with an interesting scenario to test, more precisely those that potentially can reveal some bugs in the code, please post your ideas here. We will take care of turning plain text ideas into invariants, counterexamples, and, eventually, tests.

Looking forward to your input!
@andrey-kuprianov andrey-kuprianov added help wanted Extra attention is needed question Further information is requested labels Jul 7, 2020
@andrey-kuprianov
Copy link
Contributor Author

Here is the current set of LightClient tests

@andrey-kuprianov andrey-kuprianov added the light-client Issues/features which involve the light client label Jul 8, 2020
@andrey-kuprianov andrey-kuprianov self-assigned this Jul 9, 2020
@andrey-kuprianov andrey-kuprianov changed the title Ideas for model-based testing of the LightClient Develop a set of model-based tests for the LightClient Jul 9, 2020
andrey-kuprianov added a commit that referenced this issue Jul 31, 2020
@andrey-kuprianov
#414: factor out common parts from tests/lite.rs into tests/lite_tests
d9c6b5e
andrey-kuprianov added a commit that referenced this issue Jul 31, 2020
@andrey-kuprianov
#414: lite_tests: add Command/CommandRun wrapper for running external…
0ac86a3 
… commands (e.g. apalache, jsonatr)
andrey-kuprianov added a commit that referenced this issue Aug 4, 2020
@andrey-kuprianov
#414: add history variables to Lightclient_A_1.tla
e435ae3
andrey-kuprianov added a commit that referenced this issue Aug 4, 2020
@andrey-kuprianov
#414: add use default index in testgen vote
f0e7599
andrey-kuprianov added a commit that referenced this issue Aug 4, 2020
@andrey-kuprianov
#414: add first model-based test
b361b51 
* 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 added a commit that referenced this issue Aug 5, 2020
@andrey-kuprianov
#414: more structure for test cases
08450a7
andrey-kuprianov added a commit that referenced this issue Aug 6, 2020
@andrey-kuprianov
#414: simplify running external commands
04ab1aa
andrey-kuprianov added a commit that referenced this issue Aug 6, 2020
@andrey-kuprianov
#414: add simple TLA+ test
f7b3165
andrey-kuprianov added a commit that referenced this issue Aug 6, 2020
@andrey-kuprianov
#414: run apalache on TLA+ test; fix Command spawn errors
cb478f2
andrey-kuprianov added a commit that referenced this issue Aug 6, 2020
@andrey-kuprianov
#414: fix small typos
d65a72e
andrey-kuprianov added a commit that referenced this issue Aug 6, 2020
@andrey-kuprianov
#414: refactor: add commonly used test utils
a720487
andrey-kuprianov added a commit that referenced this issue Aug 6, 2020
@andrey-kuprianov
#414: more refactoring
49ef36d
andrey-kuprianov added a commit that referenced this issue Aug 7, 2020
@andrey-kuprianov
#414: add tests/utils/jsonatr.rs
b80159c
andrey-kuprianov added a commit that referenced this issue Aug 7, 2020
@andrey-kuprianov
#414: add tests/utils/jsonatr-lib
6a3831b
andrey-kuprianov added a commit that referenced this issue Aug 7, 2020
@andrey-kuprianov
#414: full model-based test TLA+ -> Apalache -> Jsonatr -> lite::veri…
e36ba00 
…fy_single
andrey-kuprianov added a commit that referenced this issue Aug 7, 2020
@andrey-kuprianov
#414: check for tendermint-testgen in PATH
368975c
andrey-kuprianov added a commit that referenced this issue Aug 10, 2020
@andrey-kuprianov
#414: testgen: add absent votes in the commit
da11fc1
andrey-kuprianov added a commit that referenced this issue Aug 10, 2020
@andrey-kuprianov
#414: testgen: add time command; make timestamps abstract
8ff0f93
andrey-kuprianov added a commit that referenced this issue Aug 10, 2020
@andrey-kuprianov
#414: make lite test timestamps abstract
4715e18
andrey-kuprianov added a commit that referenced this issue Aug 10, 2020
@andrey-kuprianov
#414: LightClient_A_1: add time to history variables
d223773
andrey-kuprianov added a commit that referenced this issue Aug 10, 2020
@andrey-kuprianov
#414: Blockchain_A_1.tla: fix discrepancy between the model and the …
ec2ba4c 
…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 added a commit that referenced this issue Aug 10, 2020
@andrey-kuprianov
#414: Lightclient_A_1.tla: store whole state sequence in history
0df4320
andrey-kuprianov added a commit that referenced this issue Aug 10, 2020
@andrey-kuprianov
#414: more TLA+ lite tests
e9a099f
andrey-kuprianov added a commit that referenced this issue Aug 11, 2020
@andrey-kuprianov
#414: Blockchain_A_1.tla: disallow generating headers with negative time
f04a163
This was linked to pull requests Sep 11, 2020
Testgen -- add abstract time and various other updates #548
Merged
Testgen external commands #549
Merged
Model-based test driver for LightClient #550
Merged
Model-based tests for LightClient #551
Merged
@andrey-kuprianov andrey-kuprianov mentioned this issue Sep 11, 2020
Open
andrey-kuprianov added a commit that referenced this issue Sep 23, 2020
@andrey-kuprianov
#414 fix testgen tester: wrong dir was removed
85b8814
andrey-kuprianov added a commit that referenced this issue Sep 23, 2020
@andrey-kuprianov
#414 move history out of LightClient.tla into LightTests.tla
97844a6
andrey-kuprianov added a commit that referenced this issue Sep 23, 2020
@andrey-kuprianov
#414 adapt apalache test runner to changes in specs
45ab864
andrey-kuprianov added a commit that referenced this issue Sep 23, 2020
@andrey-kuprianov
#414 minor changes to model_based.rs
ef474ff
andrey-kuprianov added a commit that referenced this issue Sep 24, 2020
@andrey-kuprianov
#414 account for Igor's naming suggestions
6ab98d3
andrey-kuprianov added a commit that referenced this issue Sep 24, 2020
@andrey-kuprianov
#414 copy and rename into Blockchain/Lightclient_002_draft.tla
c1a421b
andrey-kuprianov added a commit that referenced this issue Sep 24, 2020
@andrey-kuprianov
#414 restore original Blockchain/Lightclient_A_1.tla
65bd05a
andrey-kuprianov added a commit that referenced this issue Sep 24, 2020
@andrey-kuprianov
Changes to TLA+ specs for model-based testing (#546)
856084e 
See #414 
* changes to TLA+ specs for model-based testing
* Lightclient_A_1.tla: add check for header from the future
* fix testgen tester: wrong dir was removed
* move history out of LightClient.tla into LightTests.tla
* adapt apalache test runner to changes in specs
* account for Igor's naming suggestions
* copy and rename into  Blockchain/Lightclient_002_draft.tla
* restore original  Blockchain/Lightclient_A_1.tla
andrey-kuprianov added a commit that referenced this issue Sep 25, 2020
@andrey-kuprianov
#414 fix testgen tester: wrong dir was removed
6a209df
andrey-kuprianov added a commit that referenced this issue Sep 25, 2020
@andrey-kuprianov
#414 move history out of LightClient.tla into LightTests.tla
03f57c1
andrey-kuprianov added a commit that referenced this issue Sep 25, 2020
@andrey-kuprianov
#414 adapt apalache test runner to changes in specs
44b5a22
andrey-kuprianov added a commit that referenced this issue Sep 25, 2020
@andrey-kuprianov
#414 minor changes to model_based.rs
ec05594
andrey-kuprianov added a commit that referenced this issue Sep 25, 2020
@andrey-kuprianov
#414 LightTests: store prev(*)' in history to avoid loosing the last …
bbf954c 
…history state
andrey-kuprianov added a commit that referenced this issue Sep 25, 2020
@andrey-kuprianov
#414 LightTests: store next history state under correct index
6ef740e
andrey-kuprianov added a commit that referenced this issue Sep 25, 2020
@andrey-kuprianov
#414 cleanup previous model based test run
48a2819
andrey-kuprianov added a commit that referenced this issue Sep 25, 2020
@andrey-kuprianov
#414 regenerate static test files
718bf4f
andrey-kuprianov added a commit that referenced this issue Sep 25, 2020
@andrey-kuprianov
#414 more TLA+ tests
6ecedd0
andrey-kuprianov added a commit that referenced this issue Sep 25, 2020
@andrey-kuprianov
#414 more auto-generated tests
362d0e3
andrey-kuprianov added a commit that referenced this issue Sep 25, 2020
@andrey-kuprianov
#414 update description field for auto-generated tests
600f31b
andrey-kuprianov added a commit that referenced this issue Sep 25, 2020
@andrey-kuprianov
#414 update Abstract.md
14b6628
andrey-kuprianov added a commit that referenced this issue Sep 25, 2020
@andrey-kuprianov
#414 update README.md
3c6ff5c
andrey-kuprianov added a commit that referenced this issue Sep 25, 2020
@andrey-kuprianov
#414 cargo fmt
babb18c
andrey-kuprianov added a commit that referenced this issue Sep 25, 2020
@andrey-kuprianov
#414 update CHANGELOG.md
d81f52e
andrey-kuprianov added a commit that referenced this issue Sep 26, 2020
@andrey-kuprianov
Model-based tests for LightClient (#551)
b5797e3 
See #414
* LightTests: more TLA+ tests
* LightTests: store prev(*)' in history to avoid loosing the last history state
* LightTests: store next history state under correct index
* add auto-generated static model-based tests
* cleanup previous model based test run
* update Abstract.md
* update README.md
* update CHANGELOG.md
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@andrey-kuprianov andrey-kuprianov

Labels
help wanted Extra attention is needed light-client Issues/features which involve the light client question Further information is requested
Projects
None yet
Milestone
v0.17.0
2 participants
@ebuchman @andrey-kuprianov