Skip to content

GitLab

Open
Created by Sebastian Uchitel@suchitelOwner0 of 2 tasks completed0/2 tasks
Report abuse

Report tautologies as no LTL violation instead of missing acceptance states

Summary

  • When the Büchi automaton for the negated property has no acceptance labels, ProgressCheck.doLTLCheck() returned early with "No labeled acceptance states.", which reads like a warning rather than a verdict.
  • With no acceptance labels the negated property has no accepting runs, so the property holds on every trace. The message now says: "No LTL property violation detected. Property is a tautology."

Example: assert R = (a || !a) checked against A = (a->A).

Test plan

  • Check R = (a || !a) against A = (a->A) and confirm the new message is shown.
  • Check a non-trivial LTL property and confirm the normal check path is unchanged.

🤖 Generated with Claude Code