LTL/SVA->Buechi: reject error traces early #1223
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
kroening
force-pushed
the
incomplete-buechi
branch
from
4c01e47 to
7a79dce
Compare
kroening
force-pushed
the
incomplete-buechi
branch
4 times, most recently
from
3bab967 to
367b584
Compare
tautschnig
approved these changes
Aug 6, 2025
| -- | ||
| ^warning: ignoring | ||
| -- | ||
| Back-end support is missing. |
There was a problem hiding this comment.
What does this comment mean when the lines above suggest that the properties are proved and refuted, respectively?
There was a problem hiding this comment.
It's a leftover; removed
| -- | ||
| ^warning: ignoring | ||
| -- | ||
| SMT-back end doesn't do cast from bool to bool. |
There was a problem hiding this comment.
How does this become apparent when this test isn't excluded from the tests run with the SMT back-end?
There was a problem hiding this comment.
Another leftover; removed
| @@ -155,6 +174,37 @@ ltl_to_buechi(const exprt &property, message_handlert &message_handler) | |||
| message.debug() << "Buechi liveness signal: " << format(liveness_signal) | |||
| << messaget::eom; | |||
|
|
|||
| // construct the error signal -- true when the next automaton state | |||
| // is nonaccepting with an unconditional self-loop. | |||
There was a problem hiding this comment.
Should this say "accepting" instead of "nonaccepting"?
The Buechi automaton accepts counterexamples to the original property. The Buechi acceptance condition requires a lasso where the loop contains an accepting state. A proof of that requires satisfying the looping condition, which may require a very long counterexample. This adds a shortcut using a sufficient condition for a counterexample: we can reject the property when we reach a state in which the Buechi automaton transitions into an accepting state that has an unconditional self-loop on it. Such traces can always be extended to a lasso as above.
kroening
force-pushed
the
incomplete-buechi
branch
from
367b584 to
9633ac8
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The Buechi automaton accepts counterexamples to the original property. The Buechi acceptance condition requires a lasso where the loop contains an accepting state. A proof of that requires satisfying the looping condition, which may require a very long counterexample.
This adds a shortcut using a sufficient condition for a counterexample: we can reject the property when we reach a state in which the Buechi automaton transitions into an accepting state that has an unconditional self-loop on it. Such traces can always be extended to a lasso as above.