Bump version to 1.99b to celebrate support for generic acceptance
* configure.ac: Bump version. * NEWS: Update description of HOA support.
This commit is contained in:
parent
b321a410d5
commit
7bac775ad4
2 changed files with 13 additions and 13 deletions
24
NEWS
24
NEWS
|
|
@ -1,4 +1,4 @@
|
|||
New in spot 1.99a (not yet released)
|
||||
New in spot 1.99b (not yet released)
|
||||
|
||||
* Major changes (including backward incompatible changes):
|
||||
|
||||
|
|
@ -70,17 +70,17 @@ New in spot 1.99a (not yet released)
|
|||
order to do batch processing. This format can be output by all
|
||||
tools (since Spot 1.2.5) using the --hoa option, and it can be
|
||||
read by autfilt (by default) and ltlcross (using the %H
|
||||
specifier). The current implementation does not support:
|
||||
- acceptance specifications involving "Fin(x)", "|", or "f".
|
||||
- alternation
|
||||
but the rest is expected to work. Those restrictions cause the
|
||||
automaton to be interpretable as a TGBA. In particular,
|
||||
multiple initial states are converted into an extra initial
|
||||
state; complemented acceptance sets Inf(!x) are converted to
|
||||
Inf(x); negated (maybe after duplication); explicit or implicit
|
||||
labels can be used; aliases are supported; "--ABORT--" can be
|
||||
used in a stream. The parser currently ignore all optional
|
||||
headers (starting with a lowercase letter).
|
||||
specifier). The current implementation does not support
|
||||
alternation. Multiple initial states are converted into an
|
||||
extra initial state; complemented acceptance sets Inf(!x) are
|
||||
converted to Inf(x); negated (maybe after duplication); explicit
|
||||
or implicit labels can be used; aliases are supported;
|
||||
"--ABORT--" can be used in a stream.
|
||||
|
||||
Note that not all algorithms in the library will work with any
|
||||
acceptance conditions. Automata with acceptance conditions that
|
||||
involve Fin acceptance can be couverted to not use Fin when that
|
||||
is a problem.
|
||||
|
||||
- The above HOA parser can also parse never claims, and LBTT
|
||||
automata, so the never claim parser and the LBTT parser have
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue