diff --git a/NEWS b/NEWS index 18caa0615..4c0f4b439 100644 --- a/NEWS +++ b/NEWS @@ -5,6 +5,12 @@ New in spot 2.2.2.dev (Not yet released) * ltlcross supports translators that output weak alternating automata in the HOA format (not necessarily *very* weak). + * autfilt can read alternating automata. This is still experimental + (see below). Some of the algorithms proposed by autfilt will + refuse to work because they have not yet been updated to work with + alternating automata, but in any case they should display a + diagnostic: if you see a crash, please report it. + Library: * A twa is required to have at least one state, the initial state. @@ -41,6 +47,13 @@ New in spot 2.2.2.dev (Not yet released) were existential edges. As a consequence, acceptance information is not accurate. + - postprocessor will call remove_alternation() right away, so + it can be used as a way to transform alternating automata + into different sub-types of (generalized) Büchi automata. + Note that although prostprocessor optimize the resulting + automata, it still has no simplification algorithms that work + at the alternating automaton level. + * twa objects have a new property, very-weak, that can be set or retrieved via twa::prop_very_weak(), and that can be tested by is_very_weak_automaton(). diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index d1181c2cf..b119663a8 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -34,6 +34,7 @@ #include #include #include +#include namespace spot { @@ -173,6 +174,14 @@ namespace spot if (type_ == BA || SBACC_) state_based_ = true; + if (a->is_alternating() && + // We will probably have to revisit this condition later. + // Currently, the intent is that postprocessor should never + // return an alternating automaton, unless it is called with + // its laxest settings. + !(type_ == Generic && PREF_ == Any && level_ == Low)) + a = remove_alternation(a); + if (type_ != Generic && !a->acc().is_generalized_buchi()) { a = to_generalized_buchi(a); diff --git a/tests/core/alternating.test b/tests/core/alternating.test index a09c8f0d2..158cb99eb 100644 --- a/tests/core/alternating.test +++ b/tests/core/alternating.test @@ -133,3 +133,27 @@ properties: univ-branch trans-labels explicit-labels state-acc properties: very-weak EOF diff output expected + + +cat >out.hoa <