SVA/LTL property instrumentation #797
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
instrument_property
branch
2 times, most recently
from
3bcb3a7 to
9525b7b
Compare
kroening
force-pushed
the
instrument_property
branch
3 times, most recently
from
e5ff5b3 to
e6564c8
Compare
kroening
force-pushed
the
instrument_property
branch
5 times, most recently
from
8ec6355 to
dfbcbbe
Compare
kroening
force-pushed
the
instrument_property
branch
from
dfbcbbe to
40f22fe
Compare
kroening
force-pushed
the
instrument_property
branch
from
40f22fe to
d73abf5
Compare
kroening
force-pushed
the
instrument_property
branch
9 times, most recently
from
6c470e6 to
7f74cae
Compare
kroening
force-pushed
the
instrument_property
branch
6 times, most recently
from
8bf29c8 to
e78b65d
Compare
kroening
force-pushed
the
instrument_property
branch
3 times, most recently
from
9f052f8 to
2c10033
Compare
tautschnig
approved these changes
May 28, 2025
Comment on lines
+42
to
+43
| namespacet ns(transition_system.symbol_table); | ||
| auto property_symbol = ns.lookup(property.identifier); |
There was a problem hiding this comment.
Since you don't actually need the namespace you might just do auto property_symbol = transition_system.symbol_table.lookup_ref(property.identifier);
kroening
force-pushed
the
instrument_property
branch
6 times, most recently
from
3c55b93 to
c113caa
Compare
This adds --buechi, which triggers an instrumentation pass that turns LTL and select SVA properties into a Buechi automaton. The automaton is then added to the model, and the property is replaced by the Buechi acceptance condition. The translation is done via ltl2tgba. This enables checking arbitrary LTL properties via the BDD engine.
kroening
force-pushed
the
instrument_property
branch
from
c113caa to
d682fe4
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.
This adds
--buechi, which triggers an instrumentation pass that turns LTL and select SVA properties into a Büchi automaton. The automaton is then added to the model, and the property is replaced by the Büchi acceptance condition.The translation is done via
ltl2tgba.This enables checking arbitrary LTL properties via the BDD engine.