Commit f1b8d5f1 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

postproc: preliminary support for alternating automata

* spot/twaalgos/ Call remove_alternation().
* tests/core/alternating.test: Additional test.
parent 9f6924cc
......@@ -5,6 +5,12 @@ New in spot (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.
* A twa is required to have at least one state, the initial state.
......@@ -41,6 +47,13 @@ New in spot (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
......@@ -34,6 +34,7 @@
#include <spot/twaalgos/sbacc.hh>
#include <spot/twaalgos/sepsets.hh>
#include <spot/twaalgos/determinize.hh>
#include <spot/twaalgos/alternation.hh>
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);
......@@ -133,3 +133,27 @@ properties: univ-branch trans-labels explicit-labels state-acc
properties: very-weak
diff output expected
cat >out.hoa <<EOF
HOA: v1
tool: "ltl3dra" "0.2.2"
name: "VWAA for GFa"
States: 3
Start: 0
acc-name: co-Buchi
Acceptance: 1 Fin(0)
AP: 1 "a"
properties: trans-labels explicit-labels state-acc univ-branch very-weak
State: 0 "GF(a)"
[t] 1&0
State: 1 "F(a)" {0}
[(0)] 2
[t] 1
State: 2 "t"
[t] 2
test 3 = `autfilt --stats=%s out.hoa`
test 2 = `autfilt --tgba --stats=%s out.hoa`
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment