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:
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.