94 lines
3.5 KiB
Text
94 lines
3.5 KiB
Text
New in spot 0.0s:
|
||
|
||
New in spot 0.0r (2004-03-08):
|
||
|
||
* In ltl_to_tgba_fm:
|
||
- New option `exprop' to optimize determinism.
|
||
- Make the `symbolic indentification' from 0.0p optional.
|
||
* `nonacceptant_lbtt_reachable' new function to help getting
|
||
accurate statistics from LBTT.
|
||
* Revamp the cgi script's user interface.
|
||
* Upgrade to lbtt 1.0.3, swig 1.3.21, automake 1.8.3
|
||
|
||
New in spot 0.0p (2004-02-03):
|
||
|
||
* In ltl_to_tgba_fm:
|
||
- identify states with identical symbolic expansions
|
||
(i.e., identical continuations)
|
||
- use Acc[b] as acceptance condition for Fb, not Acc[Fb].
|
||
* Update and speed-up the cgi script.
|
||
* Improve degeneralization.
|
||
|
||
New in spot 0.0n (2004-01-13):
|
||
|
||
* emptiness_check::check2() is a variant of Couvreur's emptiness check that
|
||
explores visited states first.
|
||
* Build the EESRG supporting code condinally, as the associated
|
||
GreatSPN changes have not yet been contributed to GreatSPN.
|
||
* Add a powerset algorithm (determinize TGBA ignoring acceptance
|
||
conditions, i.e., as if they were used to recognize finite languages).
|
||
* tgba_explicit::merge_transitions: merge transitions with same source,
|
||
destination, and acceptance condition.
|
||
* Run test cases within valgrind.
|
||
* Various bug fixes.
|
||
|
||
New in spot 0.0l (2003-12-01):
|
||
|
||
* Computation of prime implicants. This simplify the output of
|
||
ltl_to_tgba_fm, and allows conditions to be output as some of
|
||
product in dot output.
|
||
* Optimize translation of GFy in ltl_to_tgba_fm.
|
||
* tgba_explicit supports arbitrary binary formulae on transitions
|
||
(only conjunctions were allowed).
|
||
|
||
New in spot 0.0j (2003-11-03):
|
||
|
||
* Use hash_map's instead of map's almost everywhere.
|
||
* New emptiness check, based on Couvreur's algorithm.
|
||
* LTL propositions can be put inside doublequotes to disambiguate
|
||
some constructions.
|
||
* Preliminary support for GreatSPN's EESRG.
|
||
* Various bug fixes.
|
||
|
||
New in spot 0.0h (2003-08-18):
|
||
|
||
* More python bindings:
|
||
- "import buddy" works (see wrap/python/tests/bddnqueen.py for an example),
|
||
- almost all the Spot API is now available via "import spot".
|
||
* wrap/python/cgi/ltl2tgba.py is an LTL-to-B<>chi translator that
|
||
work as as a cgi script.
|
||
* Couvreur's FM'99 ltl-to-tgba translation.
|
||
|
||
New in spot 0.0f (2003-08-01):
|
||
|
||
* More python bindings, still only for the spot::ltl:: namespace.
|
||
* Functional GSPN interface. (Enable with --with-gspn=directory.)
|
||
* The LTL scanner recognizes /\, \/, and xor.
|
||
* Upgrade to lbtt 1.0.2.
|
||
* tgba_tba_proxy is an on-the-fly degeneralizer.
|
||
* Implements the "magic search" algorithm.
|
||
(Works only on a tgba_tba_proxy.)
|
||
* Tgba's output algorithms (save(), dotty()) now non-recursive.
|
||
* During products, succ_iter will optimize its set of successors
|
||
using information computed from the current product state.
|
||
* BDD dictionnaries are now shared between automata and. This
|
||
gets rid of all the BDD-variable translating machinery.
|
||
|
||
New in spot 0.0d (2003-07-13):
|
||
|
||
* Optimize translation of G operators occurring at the root
|
||
of a formula (or its immediate children when the root is a
|
||
conjunction). This saves two BDD variables per G operator.
|
||
* Distribute lbtt, and run it during `make check'.
|
||
* First sketch of GSPN interface.
|
||
* succ_iter_concreate::next() completely rewritten.
|
||
* Transitions are now labelled by boolean formulae (not only
|
||
conjunctions).
|
||
* Documentation:
|
||
- Output collaboration diagrams.
|
||
- Build and distribute PDF manual.
|
||
* Many bug fixes.
|
||
|
||
New in spot 0.0b (2003-06-26):
|
||
|
||
* Everything.
|