ltlcross/ltldo/autcross support for newer owl
Owl 21.0 will have a single binary with multiple commands. We need to teach ltlcross
,ltldo
, and autcross
how to recognize those. Recognizing owl ltl2nba
, owl ltl2ldgba
, etc. would work, but in order to support concurrent versions of Owl to be installed it would be better to match owl[^ ]* ltlnba
, owl[^ ]* ltl2ldgba
, etc.
Usage: owl [-hV] COMMAND
A tool collection and library for ω-words, ω-automata and linear temporal logic.
-h, --help Show this help message and exit.
-V, --version Print version information and exit.
Commands:
ltl2nba Translate a linear temporal logic (LTL) formula into a non-deterministic Büchi
automaton (NBA).
ltl2ngba Translate a linear temporal logic (LTL) formula into a non-deterministic generalized
Büchi automaton (NGBA).
ltl2ldba Translate a linear temporal logic (LTL) formula into a limit-deterministic Büchi
automaton (LDBA).
ltl2ldgba Translate a linear temporal logic (LTL) formula into a limit-deterministic
generalized Büchi automaton (LDGBA).
ltl2dpa Translate a linear temporal logic (LTL) formula into a deterministic parity automaton
(DPA).
ltl2dra Translate a linear temporal logic (LTL) formula into a deterministic Rabin automaton
(DRA).
ltl2dgra Translate a linear temporal logic (LTL) formula into a deterministic generalized
Rabin automaton (DGRA).
ltl2dela Translate a linear temporal logic (LTL) formula into a deterministic Emerson-Lei
automaton (DELA).
ltl2delta2 Rewrite a linear temporal logic (LTL) formula into the Δ₂-normal-form using the
construction of [SE20].
ngba2ldba Convert a non-deterministic (generalised) Büchi automaton to a limit-deterministic
Büchi automaton.
nba2dpa, nbadet Convert a non-deterministic Büchi automaton to a deterministic parity automaton.
nbasim Computes the quotient automaton based on a computed set of similar state pairs.
aut2parity Convert any type of automaton into a parity automaton. The branching mode of the
automaton is preserved, e.g., if the input automaton is deterministic then the
output automaton is also deterministic.
gfg-minimisation Compute the minimal, equivalent, transition-based Good-for-Games Co-Büchi automaton
for the given deterministic Co-Büchi automaton. The polynomial construction is
described in [AK19].
bibliography Print the bibliography of all implemented algorithms and constructions. Single
references can be looked up by listing them, e.g. 'owl bibliography SE20'. If you
want to cite Owl as a whole, it is recommended to use reference [KMS18].
delag The functionality of the 'delag' subcommand has been moved to the 'ltl2dela'
subcommand. You can use 'owl ltl2dela -t=MS17' to access the original 'delag'
construction.
ltl-utilities A collection of various linear temporal logic related rewriters.
rltl2ltl Convert a robust linear temporal logic (rLTL) formula into a linear temporal logic
formula.
aut-utilities A collection of various automata related utilities.