complete: add support for alternating autamata
* spot/twaalgos/complete.cc: Do not use the initial state as a sink if it is universal. * tests/core/complete.test: Add a test case.
This commit is contained in:
parent
f1b8d5f1d4
commit
071d819c49
2 changed files with 56 additions and 4 deletions
|
|
@ -49,7 +49,7 @@ namespace spot
|
||||||
{
|
{
|
||||||
bool sinkable = true;
|
bool sinkable = true;
|
||||||
bool first = true;
|
bool first = true;
|
||||||
acc_cond::mark_t commonacc = 0U;
|
acc_cond::mark_t commonacc = um.second;
|
||||||
for (auto& t: aut->out(i))
|
for (auto& t: aut->out(i))
|
||||||
{
|
{
|
||||||
if (t.dst != i) // Not a self-loop
|
if (t.dst != i) // Not a self-loop
|
||||||
|
|
@ -80,11 +80,12 @@ namespace spot
|
||||||
|
|
||||||
unsigned t = aut->num_edges();
|
unsigned t = aut->num_edges();
|
||||||
|
|
||||||
// If the automaton is empty, pretend that state 0 is a sink.
|
// If the automaton is empty, and the initial state is not
|
||||||
if (t == 0)
|
// universal, pretend this is the sink.
|
||||||
|
if (t == 0 && !aut->is_univ_dest(aut->get_init_state_number()))
|
||||||
sink = aut->get_init_state_number();
|
sink = aut->get_init_state_number();
|
||||||
|
|
||||||
// Now complete all states (excluding any newly added the sink).
|
// Now complete all states (excluding any newly added sink).
|
||||||
for (unsigned i = 0; i < n; ++i)
|
for (unsigned i = 0; i < n; ++i)
|
||||||
{
|
{
|
||||||
bdd missingcond = bddtrue;
|
bdd missingcond = bddtrue;
|
||||||
|
|
|
||||||
|
|
@ -82,6 +82,27 @@ State: 1
|
||||||
[0] 1 {0}
|
[0] 1 {0}
|
||||||
[!0] 1 {0}
|
[!0] 1 {0}
|
||||||
--END--
|
--END--
|
||||||
|
HOA: v1
|
||||||
|
States: 2
|
||||||
|
Start: 0
|
||||||
|
AP: 2 "a" "b"
|
||||||
|
Acceptance: 1 Fin(0)
|
||||||
|
properties: very-weak
|
||||||
|
--BODY--
|
||||||
|
State: 0
|
||||||
|
[!0 | 1] 0
|
||||||
|
[0&!1] 1&0
|
||||||
|
State: 1 {0}
|
||||||
|
[0&!1] 1
|
||||||
|
--END--
|
||||||
|
HOA: v1
|
||||||
|
States: 2
|
||||||
|
Start: 0&1
|
||||||
|
Acceptance: 1 Fin(0)
|
||||||
|
--BODY--
|
||||||
|
State: 0
|
||||||
|
State: 1 {0}
|
||||||
|
--END--
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
cat >expected <<EOF
|
cat >expected <<EOF
|
||||||
|
|
@ -171,6 +192,36 @@ State: 1 {0}
|
||||||
[0] 1
|
[0] 1
|
||||||
[!0] 1
|
[!0] 1
|
||||||
--END--
|
--END--
|
||||||
|
HOA: v1
|
||||||
|
States: 2
|
||||||
|
Start: 0
|
||||||
|
AP: 2 "a" "b"
|
||||||
|
acc-name: co-Buchi
|
||||||
|
Acceptance: 1 Fin(0)
|
||||||
|
properties: univ-branch trans-labels explicit-labels state-acc complete
|
||||||
|
properties: deterministic very-weak
|
||||||
|
--BODY--
|
||||||
|
State: 0
|
||||||
|
[!0 | 1] 0
|
||||||
|
[0&!1] 1&0
|
||||||
|
State: 1 {0}
|
||||||
|
[0&!1] 1
|
||||||
|
[!0 | 1] 1
|
||||||
|
--END--
|
||||||
|
HOA: v1
|
||||||
|
States: 2
|
||||||
|
Start: 0&1
|
||||||
|
AP: 0
|
||||||
|
acc-name: co-Buchi
|
||||||
|
Acceptance: 1 Fin(0)
|
||||||
|
properties: univ-branch trans-labels explicit-labels state-acc complete
|
||||||
|
properties: deterministic
|
||||||
|
--BODY--
|
||||||
|
State: 0
|
||||||
|
[t] 0
|
||||||
|
State: 1
|
||||||
|
[t] 0
|
||||||
|
--END--
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
run 0 autfilt -CH automaton >out
|
run 0 autfilt -CH automaton >out
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue