add "weak" and "inherently-weak" properties #22
Merged
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.
I would like to indicate in the property: line if an automaton is weak.
For Büchi automata, it is customary to distinguish two kinds of weakness:
Of course any weak automaton is also inherently weak, and any inherently weak automaton can be converted to a weak automaton by adjusting the acceptance set.
Essentially, a weak automaton is one in which the acceptance condition could be specified in terms of SCCs (instead of transitions or states). Presented this way (please see the wording in 947375b) the "weak" property generalizes nicely to non-Büchi automata.