ICTAC 2019 journal version release

• SLAA transition reductions are now implemented
• flags cleanup

ICTAC 2019 release

• LTL3TELA now uses substantially less acceptance marks with -G0.
• Two bugs in pattern-based reduction (Spotela) which could cause production of incorrect automata or an unhandled exception have been fixed.
• Multiple minor bugs are now fixed.

ATVA 2019 release

We are happy to announce new major release of LTL3TELA. Compared to previous versions, the sizes of produced automata decreased for a lot of formulae. The most notable new features are:

• ability to produce deterministic automata using -D1 option
• new reduction techniques in construction of SLAA and NA
• larger employment of Spot during the translation

For the entire list of changes, please see the ChangeLog.

Maintenance release

• Fixed segfault with -p1.
• Support for -m2 (detection of mergeable G for experimental purposes) added.

Integrate ltl2tgba into translation process

The version is now 1.2.0.

• LTL3TELA now tries to translate the formula with Spot and outputs the smaller automaton.
• When both the original automaton and the complemented automaton for !f have the same number of states, the latter is preferred. This should produce deterministic automata in more cases.
• -v now outputs the used version of Spot.

Compatibility with Spot 2.6

• Incorrect usage of spot::acc_cond::mark_t::value_t has been replaced with an alias of unsigned.

Maintenance release

• update version to 1.1.1
• fix segfault in make_nondeterministic if a fresh initial state is created
• catch Too many acceptance sets used. from Spot and exit with code 32
• LTL3TELA now compiles with -std=c++14

Rename to LTL3TELA; translation of both f and !f

• The tool is now named LTL3TELA
• LTL3TELA now also translates the negation of formula; if the resulting automaton is deterministic and smaller than the original automaton, its complement is used as an output
• Spot 2.4+ is now required to compile LTL3TELA

Small improvements

Thanks to Alexandre Duret-Lutz for suggesting all the improvements.

• hide "Garbage collection" messages from BuDDy
• set the name of produced nondeterministic automaton
• remove unnecessary call to purge_unreachable_states
• catch exception thrown by parse_formula

initial version

v1.0.0

add -v flag that prints version