Skip to content

Improve counterexamples diagnostics#791

Open
ydah wants to merge 1 commit into
masterfrom
fix/counterexamples-diagnostics
Open

Improve counterexamples diagnostics#791
ydah wants to merge 1 commit into
masterfrom
fix/counterexamples-diagnostics

Conversation

@ydah

@ydah ydah commented Apr 1, 2026

Copy link
Copy Markdown
Member

This PR closes several gaps between Lrama's counterexamples diagnostics and Bison's behavior.

Summary

  • Add warning-category support for -Wcounterexamples / -Wcex, and honor -Wnone / --warnings=none.
  • Emit a follow-up note suggesting -Wcounterexamples when conflicts exist but counterexample warnings are not enabled.
  • Render counterexamples in a Bison-style structure:
    • Example: when both sides share the same witness
    • First example: / Second example: when the witnesses differ
    • derivation sections for each side
  • Compute counterexamples per conflict token instead of only using the first token in a conflict.
  • Avoid misleadingly merging multi-token counterexamples when the witness differs by lookahead.
  • Render counterexamples in situ in the state/automaton report.

Refs:

@ydah ydah force-pushed the fix/counterexamples-diagnostics branch from 3a4b89d to 96df8ef Compare April 1, 2026 03:15
@ydah ydah force-pushed the fix/counterexamples-diagnostics branch from 96df8ef to 2c800a5 Compare April 1, 2026 03:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

1 participant