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

Refactor error handling #53

Closed
2 tasks done
Tracked by #65
andrey-kuprianov opened this issue Aug 13, 2021 · 2 comments
Closed
2 tasks done
Tracked by #65

Refactor error handling #53

andrey-kuprianov opened this issue Aug 13, 2021 · 2 comments
Assignees
@rnbguy
Labels
enhancement New (user-facing) feature or request
Milestone
v0.3.0 Factory

Comments

@andrey-kuprianov
Copy link
Contributor

andrey-kuprianov commented Aug 13, 2021 •
edited by rnbguy
Loading

We do indeed need to refactor the error reporting, as highlighted by #52:

  • make the errors as specific as possible, not bundle them together into a huge super-error (e.g. report per each test assertion, not per file with a bunch of assertions)
  • propagate a reasonable amount of information from the model checkers, to help the user understanding the errors
@andrey-kuprianov andrey-kuprianov added the enhancement New (user-facing) feature or request label Aug 13, 2021
@rnbguy rnbguy self-assigned this Aug 13, 2021
@andrey-kuprianov andrey-kuprianov mentioned this issue Aug 19, 2021
Closed
5 tasks
@andrey-kuprianov andrey-kuprianov added this to the v0.3.0 Factory milestone Aug 19, 2021
@rnbguy
Copy link
Member

rnbguy commented Aug 19, 2021

By looking at the error traces, I propose that I create multiple error enums.

  • TLC
  • Apalache
  • TLA-parser
  • MBT-core
  • etc.

This way, we can track each case. Also, if we split the current crate into multiple crates, we can just take the Error enums for each module.

PS. I will also start looking at TLC and Apalache as different modules for a future-proof refactor.

rnbguy added a commit that referenced this issue Aug 25, 2021
@rnbguy
one test one error (#53)
e44bb46
danwt pushed a commit that referenced this issue Aug 26, 2021
@rnbguy
Failure per test (#74)
c722ec4 
* one test one error (#53)

* rename

Co-authored-by: Daniel Tisdall <daniel@informal.systems>
@andrey-kuprianov
Copy link
Contributor Author

Closed via #68 and #74.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@rnbguy rnbguy

Labels
enhancement New (user-facing) feature or request
Projects
None yet
Milestone
v0.3.0 Factory
Development

No branches or pull requests
2 participants
@rnbguy @andrey-kuprianov