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

Recent fix of --no-deadlock does not report an error sometimes #1707

Open
konnov opened this issue May 3, 2022 · 0 comments
Open

Recent fix of --no-deadlock does not report an error sometimes #1707

konnov opened this issue May 3, 2022 · 0 comments
Assignees
Labels
bug product-owner-triage This should be triaged by the product owner

Comments

@konnov
Copy link
Collaborator

konnov commented May 3, 2022

With flag --no-deadlock introduced in #1679 this now prints:

All executions are shorter than the provided bound.               W@12:50:52.595
Found 2 error(s)                                                  I@12:50:52.598
The outcome is: ExecutionsTooShort                                I@12:50:52.601
Checker reports no error up to computation length 10              I@12:50:52.601
It took me 0 days  0 hours  0 min  4 sec                          I@12:50:52.603
Total time: 4.790 sec                                             I@12:50:52.603
EXITCODE: OK

@konnov I'd say this is resolved?

Actually, it's not. With --no-deadlock, Apalache finishes with an OK result, even if there were previous counter-examples:

All executions are shorter than the provided bound.               W@12:50:52.595
Found 2 error(s)                                                  I@12:50:52.598
The outcome is: ExecutionsTooShort                                I@12:50:52.601
Checker reports no error up to computation length 10              I@12:50:52.601
It took me 0 days  0 hours  0 min  4 sec                          I@12:50:52.603
Total time: 4.790 sec                                             I@12:50:52.603
EXITCODE: OK

Originally posted by @thpani in #1040 (comment)

@konnov konnov added the bug label May 3, 2022
@konnov konnov self-assigned this May 3, 2022
@konnov konnov added this to the X10: Bugfixing & maintenance milestone Jul 6, 2022
@konnov konnov added the product-owner-triage This should be triaged by the product owner label Jul 13, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug product-owner-triage This should be triaged by the product owner
Projects
None yet
Development

No branches or pull requests

2 participants