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

hoa: do not add a fake initial state when possible

* src/hoaparse/hoaparse.yy: If we have multiple initial states, but
one of them has no incoming edge, use this state instead of the fake
initial state we normally add.
* src/tgbatest/hoaparse.test: Add test case.
parent 58b08812
......@@ -1357,13 +1357,29 @@ static void fix_initial_state(result_& r)
}
else
{
// Multiple initial states. Add a fake one.
// Multiple initial states. We might need to add a fake one,
// unless one of the actual initial state has no incoming edge.
auto& aut = r.h->aut;
unsigned i = aut->new_state();
aut->set_init_state(i);
for (auto p : start)
for (auto& t: aut->out(p))
aut->new_transition(i, t.dst, t.cond);
std::vector<unsigned> has_incoming(aut->num_states(), 0);
for (auto& t: aut->transitions())
has_incoming[t.dst] = true;
bool found = false;
unsigned init = 0;
for (auto p: start)
if (!has_incoming[p])
{
init = p;
found = true;
}
if (!found)
// We do need a fake initial state
init = aut->new_state();
aut->set_init_state(init);
for (auto p: start)
if (p != init)
for (auto& t: aut->out(p))
aut->new_transition(init, t.dst, t.cond);
}
}
......
......@@ -1218,3 +1218,68 @@ State: 5 {0}
[t] 5
--END--
EOF
# Another example from ltl3ba
# Here we make sure that we do not always need to create a fake
# initial state when multiple initial states are used.
cat >input <<EOF
HOA: v1
tool: "ltl3ba" "1.1.0 - working copy"
name: "TGBA for GFa && GF(b&&c) && GF(d||e) || x"
States: 3
Start: 0
Start: 2
acc-name: generalized-Buchi 3
Acceptance: 3 Inf(0) & Inf(1) & Inf(2)
AP: 6 "a" "b" "c" "d" "e" "x"
properties: trans-labels explicit-labels trans-acc no-univ-branch
--BODY--
State: 0 "(x)"
[(5)] 1 {0 1 2}
State: 1 "t"
[t] 1 {0 1 2}
State: 2 "G((F(a) && F((b) && (c))) && F((d) || (e)))"
[t] 2
[(0)] 2 {0}
[(1 & 2)] 2 {1}
[(0 & 1 & 2)] 2 {0 1}
[(!3 & 4) | (3)] 2 {2}
[(0 & !3 & 4) | (0 & 3)] 2 {0 2}
[(1 & 2 & !3 & 4) | (1 & 2 & 3)] 2 {1 2}
[(0 & 1 & 2 & !3 & 4) | (0 & 1 & 2 & 3)] 2 {0 1 2}
--END--
EOF
expectok input <<EOF
HOA: v1
name: "TGBA for GFa && GF(b&&c) && GF(d||e) || x"
States: 3
Start: 0
AP: 6 "a" "b" "c" "d" "e" "x"
acc-name: generalized-Buchi 3
Acceptance: 3 Inf(0)&Inf(1)&Inf(2)
properties: trans-labels explicit-labels trans-acc complete
--BODY--
State: 0
[5] 1 {0 1 2}
[t] 2
[0] 2
[1&2] 2
[0&1&2] 2
[3 | 4] 2
[0&3 | 0&4] 2
[1&2&3 | 1&2&4] 2
[0&1&2&3 | 0&1&2&4] 2
State: 1
[t] 1 {0 1 2}
State: 2
[t] 2
[0] 2 {0}
[1&2] 2 {1}
[0&1&2] 2 {0 1}
[3 | 4] 2 {2}
[0&3 | 0&4] 2 {0 2}
[1&2&3 | 1&2&4] 2 {1 2}
[0&1&2&3 | 0&1&2&4] 2 {0 1 2}
--END--
EOF
Markdown is supported
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