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.

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

Testgen tester -- utilities to run multiple tests with logs and reports #547

Merged
merged 13 commits into from
Sep 10, 2020

Conversation

andrey-kuprianov
Copy link
Contributor

@andrey-kuprianov andrey-kuprianov commented Sep 2, 2020

Part 2 or #529. See also #414.

This PR introduces Testgen Tester. The preliminary version of it appeared in #525, but as that PR has not received sufficient number of reviews, please consider the whole code of tester.rs as new.

  • Referenced an issue explaining the need for the change
  • Updated all relevant documentation in docs
  • Updated all code comments where relevant
  • Wrote tests
  • Updated CHANGELOG.md

@andrey-kuprianov andrey-kuprianov added enhancement New feature or request tests labels Sep 2, 2020
@andrey-kuprianov andrey-kuprianov self-assigned this Sep 2, 2020
@andrey-kuprianov andrey-kuprianov changed the title #414: testgen tester -- utilities to run multiple tests with logs and reports Testgen tester -- utilities to run multiple tests with logs and reports Sep 2, 2020
Copy link
Member

@romac romac left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good, I only have a few minor comments (mostly related to the use of String vs Path types). Great job :)

testgen/src/tester.rs Show resolved Hide resolved
testgen/src/tester.rs Outdated Show resolved Hide resolved
testgen/src/tester.rs Outdated Show resolved Hide resolved
testgen/src/tester.rs Outdated Show resolved Hide resolved
testgen/src/tester.rs Outdated Show resolved Hide resolved
testgen/src/tester.rs Outdated Show resolved Hide resolved
testgen/src/tester.rs Show resolved Hide resolved
testgen/src/tester.rs Outdated Show resolved Hide resolved
testgen/src/tester.rs Outdated Show resolved Hide resolved
testgen/src/tester.rs Outdated Show resolved Hide resolved
@andrey-kuprianov
Copy link
Contributor Author

@romac I think I've addressed all of your comments; thanks a lot for them; helped to improve the code substantially:) could you please take a look?

@andrey-kuprianov
Copy link
Contributor Author

@romac The integration tests are failing, but that's probably because I've merged master. Also, of everything is OK from your point of view, could you may be merge, and review the 549?

Thanks a lot!

@romac
Copy link
Member

romac commented Sep 10, 2020

Yeah the tests are currently failing on master too (cf. #527 (comment)).

Let's merge this!

@romac romac merged commit 26ec803 into master Sep 10, 2020
@romac romac deleted the andrey/mbt-testgen-tester branch September 10, 2020 15:58
romac pushed a commit that referenced this pull request Sep 11, 2020
* #414: testgen tester -- utilities to run multiple tests with logs and reports

* 14: add testgen commands, in particular to call apalache and jsonatr

* #547 add missing file updates from #529

* fix merge typo

* remove ref to time: it's in another PR

* fix clippy warning

* TestEnv: change path parameters into AsRef<Path>

* change TestEnv::full_path to return PathBuf

* apply simplifications suggested by Romain

* apply simplification from Romain

* account for WOW Romain's suggestion on RefUnwindSafe

* address Romain's suggestion on TestEnv::cleanup

* cargo clippy

* update CHANGELOG.md

* addressed Romains's suggestions
romac pushed a commit that referenced this pull request Sep 11, 2020
* #414: testgen tester -- utilities to run multiple tests with logs and reports

* 14: add testgen commands, in particular to call apalache and jsonatr

* #414: add model-based test driver to LightClient tests

* add talk abstract

* #547 add missing file updates from #529

* fix merge typo

* remove ref to time: it's in another PR

* fix clippy warning

* fix merging typo

* cargo fmt
@andrey-kuprianov andrey-kuprianov linked an issue Sep 11, 2020 that may be closed by this pull request
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request tests
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Develop a set of model-based tests for the LightClient
2 participants