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

[BUG] When using --max-error=N where --view is not provided, Apalache reports the same counterexample N times #1004

Closed
Kukovec opened this issue Sep 30, 2021 · 1 comment · Fixed by #2144
Closed

[BUG] When using --max-error=N where --view is not provided, Apalache reports the same counterexample N times #1004

Kukovec opened this issue Sep 30, 2021 · 1 comment · Fixed by #2144
Assignees
@konnov @shonfeder
Labels
bug product-owner-triage This should be triaged by the product owner usability UX improvements
Milestone
MBT feature requests

Comments

@Kukovec
Copy link
Collaborator

Kukovec commented Sep 30, 2021

Description

See title.

Input specification

Any, where Inv has multiple counterexamples.

The command line parameters used to run the tool

apalache-mc check --inv=Inv --max-error=10 MySpec.tla

Expected behavior

N(+1) unique counterexamples.

Suggestion: force --view whenever --max-error is given
@Kukovec Kukovec added the bug label Sep 30, 2021
@Kukovec Kukovec changed the title [BUG] When using --max-error=N --view is not provided, Apalache reports the same counterexample N times [BUG] When using --max-error=N where --view is not provided, Apalache reports the same counterexample N times Sep 30, 2021
@konnov konnov added the usability UX improvements label Jan 17, 2022
@konnov konnov removed their assignment Jan 17, 2022
@konnov konnov added the product-owner-triage This should be triaged by the product owner label Jul 13, 2022
@konnov konnov mentioned this issue Sep 2, 2022
Closed
@konnov konnov added this to the MBT feature requests milestone Sep 2, 2022
@konnov
Copy link
Collaborator

konnov commented Sep 2, 2022

Actually, the command documentation says:

--view : the state view to use with --max-error=n, default: transition index

Apparently, the transition index is not used by default.

@konnov konnov mentioned this issue Sep 2, 2022
Merged
3 tasks
@will62794 will62794 mentioned this issue Aug 1, 2023
Closed
3 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@konnov konnov

@shonfeder shonfeder

Labels
bug product-owner-triage This should be triaged by the product owner usability UX improvements
Projects
None yet
Milestone
MBT feature requests
Development

Successfully merging a pull request may close this issue.

report an error when --max-error > 1 and no --view is provided apalache-mc/apalache
3 participants
@konnov @shonfeder @Kukovec