Modules:
Added new general determinization construction for NBA based on papers presented at ICALP'19 and ATVA'19. The construction supports multiple optimizations and can be invoked using the nbadet
tool.
Added simulations for NBA: direct, delayed, fair and also some other variants like with multi-pebble and lookahead simulations. The tool nbasim
can be used to preprocess an automaton by quotienting states equivalent wrt. a suitable simulation.
Added support for external parity game solver Oink.
Added ltl2normalform
that rewrites LTL formulas into the restricted alternation normal form described in our LICS'20 submission.
Removed unused --worker
flag and OWL_{ANNOTATIONS,INPUT}
environment variables.
De-duplicate fixed-point guesses in the "symmetric" constructions.
Use extensions of the FG- and GF-advice functions (LICS'18) that use both guesses X and Y to rewrite the formula. Further, guesses are skipped that contain unused fixpoints.
Removed unmaintained fgx2dpa
translation. ltl2dpa
produces almost always (on the test sets) smaller automata compared to fgx2dpa
.
ltl2da
uses for the "safety-cosafety" and "cosafety-safety" fragment a optimised construction without invoking a fallback solution. This construction is based on our LICS'20 submission.
ltl2nba
, ltl2ngba
, ltl2ldba
, ltl2ldgba
, ltl2dra
, ltl2dgra
, and ltl2dpa
use a portfolio translator selecting simpler translations based on syntactic criteria, before applying the general purpose translation. This feature can be deactivated using --disable-portfolio
.
ltl2dpa
by default now uses a complement translation to obtain (possibly) smaller DPAs. This feature can be deactivated using --disable-complement
.
API:
Replace the hand-written C++ API by an automatically generated C API that embeds Owl into a C application as a native library.
Removed unused and unmaintained FrequencyG
class and forbid subclassing of GOperator
.
Addition of Negation
as a syntactic element for LTL formulas.
OmegaAcceptanceCast enables casting and conversion of different types of omega-acceptance.
EquivalenceClass always maintains the representative. This is made possible by major performance improvements in the EquivalenceClass implementation.
Addition of the BooleanOperations
utility class providing Boolean operations (complementation, union, and intersection) on automata.
Addition of utility classes for determinization of NCW and minimisation of DCW to good-for-games NCW.
Addition of disjunctiveNormalForm
and canonicalRepresentative
methods to the EquivalenceClass
interface for retrieving fixed and well-defined representatives of an equivalence class.
Various LTL rewrite rules.
Various API simplifications in the automata package.
Bugfixes:
Fixed several bugs affecting the LD(G)BA, D(G)RA, and DPA constructions. The translations based on the LICS'18 Master theorem and its predecessors have been affected. Thanks to Julian Brunner for reporting one of the issues.
Fixed a bug in the UpwardClosedSet
class: sets that were subsumed by other sets have not been removed in all circumstances.
Fixes for non-deterministic behaviour of code implementing constructions of non-deterministic automata (NonDeterministicConstructions
).
Bugfixes:
Bugfixes:
Bugfixes:
Modules:
Implemented all LICS'18 translations for LTL fragments. Including a symbolic successor / edge computation. The translations can be found in the canonical package and are exposed via ltl2da
and ltl2na
.
Removed TLSF support. Ensuring the correct implementation of the TLSF specification posed a too large maintenance burden. Users of the TLSF format can use Syfco (https://github.com/reactive-systems/syfco) to translate it to a basic LTL formula.
Warning: There are several specifications from Syntcomp in the TLSF (basic) format that have not been correctly parsed if they have not been properly parenthesised before.
Renamed minimize-aut to optimize-aut to highlight that automata are not necessarily minimal. Implemented optimizations for Büchi-like Rabin pairs.
Removed unmaintained and broken safra
module.
API:
Overhaul of the symbolic successor computation
In addition to providing a mapping from Edge<S>
to ValuationSet
(renamed from labelledEdges(S state)
to edgeMap(S state)
) some automata can provide a direct computation of a decision tree mapping from valuations to sets of edges (edgeTree(S state)
). This enable optimisation in the JNI-access.
This feature is mostly used by the direct translation of the safety and co-safety fragment of LTL to deterministic automata.
EquivalenceClass offers a trueness
value giving the percentage of satisfying assignments for an EquivalenceClass. This value is exposed via the JNI as the quality score.
Redesigned Formula classes offering substitution as part of the API instead of a separate visitor.
{M,R,U,W}Operator.of(...)
added the following simplification rules:
The LTL simplifier added the following simplification rules:
Overhaul of the C++-API. Most notably there is an API for approximative realisability checks for a state in the decomposed DPA.
Add basic support for ultimately periodic words and add language membership tests.
Bugfixes:
Throw an exception on malformed LTL input such as FF
, Fa!
and F+
. Thanks to Alexandre Duret-Lutz for reporting this issue.
The hoa
module now correctly parsed the -s
and --state-acceptance
options.
TBD (see gitlog)
Library:
xor
operator in the LTL input.Tools:
fgx2dga
(Preview): A translation of LTL-fairness formulas (FG
/GF
) to deterministic automata with a generic acceptance condition, meaning the acceptance condition is an arbitrary boolean combination of Inf
and Fin
sets. The tool supports all LTL operators using a fallback mechanism. This is a preview, thus functionality as well as the name is subject to change.Library:
Tools:
ltl2ldba
: A translator of LTL to limit-deterministic Büchi automata.ltl2dpa
: A translator of LTL to deterministic parity automata via LDBAs.ltl2da
: A translator of LTL to any deterministic automata. The tool is a wrapper for the before mentioned tools and returns the smallest automaton.nba2ldba
: A translator of non-deterministic Büchi to limit-deterministic Büchi automata.