ltl2dstar NEWS
(C) 2005-2018 Joachim Klein

   Permission is granted to anyone to make or distribute verbatim copies
   of this document as received, in any medium, provided that the
   copyright notice and this permission notice are preserved.

   Permission is granted to distribute modified versions
   of this document, or of portions of it, under the above conditions,
   provided also that they carry prominent notices stating who last
   changed them.


Version 0.5.4 (improvements, bugfixes)
 * New option --dba-direct, defaults to yes:
   If the input NBA is already deterministic, skip Safra's determinization.
   Stutter (if applicable) and bisimulation quotienting are applied nonetheless.
   (suggested by Alexandre Duret-Lutz)
 * New option 'nbareject' for --safra (on by default):
   Preprocess NBA and remove surely rejecting states.
 * New option --extra-output for additional output beyond the main output.
 * Generate 'name' and 'tool' header for HOA output.
 * Fix: (reported by Alexandre Duret-Lutz)
    The HOA property for stutter-insensitiveness is called
    "stutter-invariant", was not properly recognized.
 * Fix: update to cpphoafparser 0.99.2
    Fixes non-deterministic validation errors when parsing larger
    HOA automata, hang when 't' or 'f' occur in acc-name extra info.
 * Promela/LBTT lexers refreshed with flex 2.6.4 (less compiler warnings)
 * Update bundled Boost library fragment to 1.66.0

Version 0.5.3 (more HOA support)
 * Fix HOA output for empty set of atomic propositions
 * Flexible --ltl2nba translator specification, can read HOA NBA
 * --input=nba option for determinizing directly from HOA NBA
 * --complement-input=yes/no and --trust-hoa-properties=yes/no
 * export stutter-insensitiveness property in HOA
 * parsing for HOA via cpphoafparser 0.99.1
 * Now requires C++11 compiler
 * Parse Promela neverclaims generated by Spin 6.2.4 and later
 * Refresh of generated parsers

Version 0.5.2 (Bugfix and maintenance release, add HOA support)
 * Fix computation of stutter-insensitive symbols, i.e., when
   --partial-stutter=yes is used (not activated by default).
   Could lead to incorrect automata.

 * Support for Hanoi Omega Automata Format (output).
   New command-line option --output-format can be used to generate
   automata in
    - ltl2dstar-format (--output-format=native)
    - HOAF             (--output-format=hoa)
    - DOT              (--output-format=dot)
   The old option --output=dot still works, but is only a legacy
   short-hand for
     --output=automaton --output-format=dot

 * Update included Boost C++ Libraries version to 1.57.0

 * Some code-cleanup:
   - (Named) temporary files are created with mkstemp()
   - Refactor handling of non-existing bitset index
   - Switch from unsigned int to std::size_t to reduce some 64bit
     warnings.
   - Fix compilation issues on Cygwin and newer GCC compilers.
   - Update hash map class to support various implementations
     (TR1, STD, Boost, ...), see common/hash_map.hpp
  
 * Fix some small issues in the documentation
 * Now actually support ^ (xor)
 * Search for external tool in the path (see documentation)
 * Correctly quote " in output of --detailed-states=yes
 
 * Optional infrastructure for building ltl2dstar with cmake (see README)

Version 0.5.1 (Bugfix release)
 * Fix bug in SafraTree.operator<
 * Add Plugin infrastructure

Version 0.5.0

 * Add stuttering, with command line options (see documentation):
    --stutter            Use stutter construction
    --partial-stutter    Use partial stutter

    --stutter=yes is new default.

 * Add option --automata=original-nba to output the NBA generated for
   the LTL formula

 * Several bugfixes
 
 * Update included Boost C++ Libraries version to 1.33.1


Version 0.4.2 (Bugfix release)

 * Fix compilation errors on SUN Solaris (variable name clashes)


Version 0.4.1 (Bugfix release)
 
 * Fix memory access problems in DRAOptimizations (bisimulation)