parseaut: handle alternating automata with many universal init states
* spot/parseaut/parseaut.yy (fix_initial_state): Use spot::internal::outgoing_edge_group to reduce all initial states to a single one. * tests/core/parseaut.test: Add more tests.
This commit is contained in:
Alexandre Duret-Lutz
parent
27ab631cdc
commit
d2f471da06
2 changed files with 164 additions and 27 deletions
|
|
@ -40,6 +40,7 @@
|
|||
#include <spot/parseaut/public.hh>
|
||||
#include "spot/priv/accmap.hh"
|
||||
#include <spot/tl/parse.hh>
|
||||
#include <spot/twaalgos/alternation.hh>
|
||||
|
||||
#ifndef HAVE_STRVERSCMP
|
||||
// If the libc does not have this, a version is compiled in lib/.
|
||||
|
|
@ -2128,6 +2129,24 @@ static void fix_acceptance(result_& r)
|
|||
}
|
||||
}
|
||||
|
||||
// Spot only supports a single initial state.
|
||||
//
|
||||
// If the input file does not declare any initial state (this is valid
|
||||
// in the HOA format) add one nonetheless.
|
||||
//
|
||||
// If the input file has multiple initial states we have to merge
|
||||
// them.
|
||||
//
|
||||
// 1) In the non-alternating case, this is as simple as making a new
|
||||
// initial state using the union of all the outgoing transitions of
|
||||
// the declared initial states. Note that if one of the original
|
||||
// initial state has no incoming transition, then we can use it as
|
||||
// initial state, avoiding the creation of a new state.
|
||||
//
|
||||
// 2) In the alternating case, the input may have several initial
|
||||
// states that are conjuncts. We have to reduce the conjuncts to a
|
||||
// single state first.
|
||||
|
||||
static void fix_initial_state(result_& r)
|
||||
{
|
||||
std::vector<std::vector<unsigned>> start;
|
||||
|
|
@ -2139,16 +2158,16 @@ static void fix_initial_state(result_& r)
|
|||
v.reserve(p.second.size());
|
||||
for (unsigned s: p.second)
|
||||
// Ignore initial states without declaration
|
||||
// (They have been diagnosed already.)
|
||||
if (s < ssz && r.info_states[s].declared)
|
||||
v.emplace_back(s);
|
||||
if (!v.empty())
|
||||
start.push_back(v);
|
||||
}
|
||||
|
||||
// If no initial state has been declared, add one.
|
||||
if (start.empty())
|
||||
{
|
||||
// If no initial state has been declared, add one, because
|
||||
// Spot will not work without one.
|
||||
if (r.opts.want_kripke)
|
||||
r.h->ks->set_init_state(r.h->ks->new_state(bddfalse));
|
||||
else
|
||||
|
|
@ -2189,32 +2208,58 @@ static void fix_initial_state(result_& r)
|
|||
|
||||
bool found = false;
|
||||
unsigned init = 0;
|
||||
bool init_alternation = false;
|
||||
for (auto& pp: start)
|
||||
{
|
||||
if (pp.size() != 1)
|
||||
{
|
||||
r.h->errors.emplace_front(r.start.front().first,
|
||||
"alternating automata only support "
|
||||
"a single initial state");
|
||||
return;
|
||||
}
|
||||
unsigned p = pp.front();
|
||||
if (!has_incoming[p])
|
||||
{
|
||||
init = p;
|
||||
found = true;
|
||||
}
|
||||
}
|
||||
if (!found)
|
||||
if (pp.size() == 1)
|
||||
{
|
||||
unsigned p = pp.front();
|
||||
if (!has_incoming[p])
|
||||
{
|
||||
init = p;
|
||||
found = true;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
init_alternation = true;
|
||||
break;
|
||||
}
|
||||
|
||||
if (!found || init_alternation)
|
||||
// We do need a fake initial state
|
||||
init = aut->new_state();
|
||||
aut->set_init_state(init);
|
||||
for (auto& pp: start)
|
||||
|
||||
// The non-alternating case is the easiest, we simply declare
|
||||
// the outgoing transitions of all "original initial states"
|
||||
// into the only one initial state.
|
||||
if (!init_alternation)
|
||||
{
|
||||
unsigned p = pp.front();
|
||||
if (p != init)
|
||||
for (auto& t: aut->out(p))
|
||||
aut->new_edge(init, t.dst, t.cond);
|
||||
for (auto& pp: start)
|
||||
{
|
||||
unsigned p = pp.front();
|
||||
if (p != init)
|
||||
for (auto& t: aut->out(p))
|
||||
aut->new_edge(init, t.dst, t.cond);
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
// In the alternating case, we merge outgoing transition of
|
||||
// the universal destination of conjunct initial states.
|
||||
// (Note that this loop would work for the non-alternating
|
||||
// case too, but it is more expansive, so we avoid it if we
|
||||
// can.)
|
||||
spot::outedge_combiner combiner(aut);
|
||||
bdd comb_or = bddfalse;
|
||||
for (auto& pp: start)
|
||||
{
|
||||
bdd comb_and = bddtrue;
|
||||
for (unsigned d: pp)
|
||||
comb_and &= combiner(d);
|
||||
comb_or |= comb_and;
|
||||
}
|
||||
combiner.new_dests(init, comb_or);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1867,8 +1867,8 @@ input:45.13-28: ... 'properties: !inherently-weak' given here
|
|||
EOF
|
||||
|
||||
|
||||
# This input caused a segfault at some point.
|
||||
# Not supporting alternation is not an excuse for segfaulting.
|
||||
# This input caused a segfault at some point (before Spot's support
|
||||
# for alternating automaton).
|
||||
cat >input <<EOF
|
||||
HOA: v1
|
||||
tool: "ltl3ba" "1.1.2"
|
||||
|
|
@ -1920,8 +1920,84 @@ State: 11 "t"
|
|||
--END--
|
||||
EOF
|
||||
|
||||
expecterr input <<EOF
|
||||
input:4.1-12: alternating automata only support a single initial state
|
||||
expectok input <<EOF
|
||||
HOA: v1
|
||||
States: 13
|
||||
Start: 12
|
||||
AP: 4 "p2" "c1" "p1" "c2"
|
||||
acc-name: co-Buchi
|
||||
Acceptance: 1 Fin(0)
|
||||
properties: univ-branch trans-labels explicit-labels state-acc
|
||||
--BODY--
|
||||
State: 0 "X (G(c2))"
|
||||
[t] 1
|
||||
State: 1 "G(c2)"
|
||||
[3] 1
|
||||
State: 2 "FG(c1)" {0}
|
||||
[1] 3
|
||||
[t] 2
|
||||
State: 3 "G(c1)"
|
||||
[1] 3
|
||||
State: 4 "X (F!((c2)))"
|
||||
[t] 5
|
||||
State: 5 "F!((c2))" {0}
|
||||
[!3] 11
|
||||
[t] 5
|
||||
State: 6 "GF!((c1))"
|
||||
[!1] 6
|
||||
[t] 7&6
|
||||
State: 7 "F!((c1))" {0}
|
||||
[!1] 11
|
||||
[t] 7
|
||||
State: 8 "((!((c1)) U (!((c1)) && !((p1)))) R F!((p2)))"
|
||||
[!0&!1&!2] 11
|
||||
[!1&!2] 10
|
||||
[!0&!1] 9
|
||||
[!1] 10&9
|
||||
[!0] 8
|
||||
[t] 10&8
|
||||
State: 9 "(!((c1)) U (!((c1)) && !((p1))))" {0}
|
||||
[!1&!2] 11
|
||||
[!1] 9
|
||||
State: 10 "F!((p2))" {0}
|
||||
[!0] 11
|
||||
[t] 10
|
||||
State: 11 "t"
|
||||
[t] 11
|
||||
State: 12
|
||||
[!0&!1&!2] 1&5&11
|
||||
[!0&!1&!2] 2&5&11
|
||||
[!0&!1&!2] 1&6&11
|
||||
[!0&!1&!2] 2&6&11
|
||||
[!0&!1] 1&5&9
|
||||
[!0&!1] 2&5&9
|
||||
[!0&!1] 1&6&9
|
||||
[!0&!1] 2&6&9
|
||||
[!0&!1] 1&6&8
|
||||
[!0&!1] 2&6&8
|
||||
[!0&1] 3&5&8
|
||||
[!0&1] 3&6&7&8
|
||||
[!0] 1&5&8
|
||||
[!0] 2&5&8
|
||||
[!0] 1&6&7&8
|
||||
[!0] 2&6&7&8
|
||||
[!1&!2] 1&5&10
|
||||
[!1&!2] 2&5&10
|
||||
[!1&!2] 1&6&10
|
||||
[!1&!2] 2&6&10
|
||||
[!1] 1&5&9&10
|
||||
[!1] 2&5&9&10
|
||||
[!1] 1&6&9&10
|
||||
[!1] 2&6&9&10
|
||||
[!1] 1&6&8&10
|
||||
[!1] 2&6&8&10
|
||||
[1] 3&5&8&10
|
||||
[1] 3&6&7&8&10
|
||||
[t] 1&5&8&10
|
||||
[t] 2&5&8&10
|
||||
[t] 1&6&7&8&10
|
||||
[t] 2&6&7&8&10
|
||||
--END--
|
||||
EOF
|
||||
|
||||
# Some alternation errors
|
||||
|
|
@ -1956,6 +2032,20 @@ State: 0
|
|||
[!0&1] 2
|
||||
[0&1] 0&1
|
||||
--END--
|
||||
HOA: v1
|
||||
Start: 0&1
|
||||
AP: 2 "a" "b"
|
||||
acc-name: co-Buchi
|
||||
Acceptance: 1 Fin(0)
|
||||
properties: univ-branch trans-labels explicit-labels state-acc
|
||||
properties: complete deterministic
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0&!1] 0&1
|
||||
[0&!1] 1
|
||||
[!0&1] 2
|
||||
[0&1] 0&1
|
||||
--END--
|
||||
EOF
|
||||
|
||||
err1="this might cause the following errors"
|
||||
|
|
@ -1973,6 +2063,8 @@ input:29.7-9: universal branch used despite previous declaration...
|
|||
input:22.13-24: ... here
|
||||
input:26.11: state 1 has no definition
|
||||
input:28.8: state 2 has no definition
|
||||
input:32.1-10: initial state 1 has no definition
|
||||
input:42.8: state 2 has no definition
|
||||
EOF
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue