remove_fin: fix incorrect state-based output
* spot/twaalgos/remfin.cc: If no Inf set is used, set sbacc early so that it is used in the algorithm. * tests/core/remfin.test: Add more tests. * NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz
parent
30a68d288b
commit
df04c715cf
3 changed files with 204 additions and 5 deletions
7
NEWS
7
NEWS
|
|
@ -194,6 +194,13 @@ New in spot 2.3.5.dev (not yet released)
|
|||
- The 'spot.gen' package exports the functions from libspotgen.
|
||||
See https://spot.lrde.epita.fr/ipynb/gen.html for examples.
|
||||
|
||||
Bugs fixed:
|
||||
|
||||
- When the remove_fin() function was called on some automaton with
|
||||
Inf-less acceptance involving at least one disjunction (e.g.,
|
||||
generalized co-Büchi), it would sometime output an automaton with
|
||||
transition-based acceptance but marked as state-based.
|
||||
|
||||
Backward-incompatible changes:
|
||||
|
||||
- spot::acc_cond::mark_t::operator bool() has been marked as
|
||||
|
|
|
|||
|
|
@ -672,7 +672,11 @@ namespace spot
|
|||
res->set_acceptance(aut->num_sets() + extra_sets, new_code);
|
||||
res->set_init_state(aut->get_init_state_number());
|
||||
|
||||
bool sbacc = aut->prop_state_acc().is_true();
|
||||
// If the input had no Inf, the output is a state-based automaton.
|
||||
if (allinf == 0U)
|
||||
res->prop_state_acc(true);
|
||||
|
||||
bool sbacc = res->prop_state_acc().is_true();
|
||||
scc_info si(aut);
|
||||
unsigned nscc = si.scc_count();
|
||||
std::vector<unsigned> state_map(nst);
|
||||
|
|
@ -749,9 +753,6 @@ namespace spot
|
|||
}
|
||||
}
|
||||
|
||||
// If the input had no Inf, the output is a state-based automaton.
|
||||
if (allinf == 0U)
|
||||
res->prop_state_acc(true);
|
||||
|
||||
res->purge_dead_states();
|
||||
trace << "before cleanup: " << res->get_acceptance() << '\n';
|
||||
|
|
|
|||
|
|
@ -250,6 +250,20 @@ State: 1 {2}
|
|||
[0] 1
|
||||
[!0] 0
|
||||
--END--
|
||||
/*
|
||||
** This random automaton caused remove_fin() to output
|
||||
** an automaton with transition-based acceptance incorrectly marked as
|
||||
** state-based.
|
||||
*/
|
||||
HOA: v1 States: 10 Start: 0 AP: 2 "p0" "p1" Acceptance: 4 Fin(1) |
|
||||
(Fin(2) & Fin(3) & Fin(0)) properties: trans-labels explicit-labels
|
||||
trans-acc --BODY-- State: 0 [!0&1] 5 [!0&1] 7 State: 1 [0&!1] 2 {2}
|
||||
[0&1] 9 {1} [!0&1] 1 [0&!1] 6 {1 3} State: 2 [!0&1] 8 {0 1} [!0&!1]
|
||||
1 {1} State: 3 [!0&1] 5 {1} [0&1] 2 State: 4 [0&!1] 4 {1} [0&1] 6 {0}
|
||||
[0&1] 5 {1} State: 5 [0&1] 9 {1} State: 6 [0&1] 5 {2 3} [!0&1] 9 {2}
|
||||
[!0&1] 4 State: 7 [0&!1] 8 {3} [!0&!1] 7 {2} [0&!1] 3 {2} [!0&1] 5 {1}
|
||||
State: 8 [!0&1] 8 {2} [!0&!1] 3 {1} [!0&1] 4 State: 9 [0&!1] 6 {0 3}
|
||||
[!0&1] 2 --END--
|
||||
EOF
|
||||
|
||||
acctwelve='Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4)&Inf(5)'
|
||||
|
|
@ -715,6 +729,91 @@ State: 1 {0}
|
|||
[!0] 0
|
||||
[0] 1
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 21
|
||||
Start: 0
|
||||
AP: 2 "p0" "p1"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels state-acc
|
||||
--BODY--
|
||||
State: 0 {0}
|
||||
[!0&1] 5
|
||||
[!0&1] 7
|
||||
State: 1
|
||||
[!0&1] 1
|
||||
[0&!1] 2
|
||||
[0&!1] 6
|
||||
[0&1] 9
|
||||
[!0&1] 14
|
||||
[!0&1] 20
|
||||
State: 2
|
||||
[!0&!1] 1
|
||||
[!0&1] 8
|
||||
[!0&!1] 20
|
||||
State: 3
|
||||
[0&1] 2
|
||||
[!0&1] 5
|
||||
[0&1] 18
|
||||
State: 4
|
||||
[0&!1] 4
|
||||
[0&1] 5
|
||||
[0&1] 6
|
||||
[0&!1] 17
|
||||
State: 5
|
||||
[0&1] 9
|
||||
State: 6
|
||||
[!0&1] 4
|
||||
[0&1] 5
|
||||
[!0&1] 9
|
||||
[!0&1] 12
|
||||
[!0&1] 17
|
||||
State: 7 {0}
|
||||
[0&!1] 3
|
||||
[!0&1] 5
|
||||
[!0&!1] 7
|
||||
[0&!1] 8
|
||||
State: 8
|
||||
[!0&!1] 3
|
||||
[!0&1] 4
|
||||
[!0&1] 8
|
||||
[!0&1] 12
|
||||
[!0&1] 13
|
||||
[!0&1] 17
|
||||
[!0&!1] 19
|
||||
State: 9
|
||||
[!0&1] 2
|
||||
[0&!1] 6
|
||||
[0&!1] 11
|
||||
[!0&1] 18
|
||||
State: 10 {0}
|
||||
[0&!1] 11
|
||||
State: 11 {0}
|
||||
[!0&1] 10
|
||||
[!0&1] 12
|
||||
State: 12 {0}
|
||||
[0&1] 11
|
||||
State: 13 {0}
|
||||
[!0&1] 12
|
||||
[!0&1] 13
|
||||
State: 14 {0}
|
||||
[!0&1] 14
|
||||
State: 15 {0}
|
||||
[0&1] 16
|
||||
State: 16 {0}
|
||||
[!0&1] 18
|
||||
State: 17 {0}
|
||||
[0&1] 15
|
||||
[0&!1] 17
|
||||
State: 18 {0}
|
||||
[!0&!1] 20
|
||||
State: 19 {0}
|
||||
[!0&1] 15
|
||||
[0&1] 18
|
||||
State: 20 {0}
|
||||
[0&1] 16
|
||||
[!0&1] 20
|
||||
--END--
|
||||
EOF
|
||||
|
||||
cat >expected-tgba <<EOF
|
||||
|
|
@ -1174,6 +1273,91 @@ State: 1 {0}
|
|||
[!0] 0
|
||||
[0] 1
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 21
|
||||
Start: 0
|
||||
AP: 2 "p0" "p1"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels trans-acc
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0&1] 5
|
||||
[!0&1] 7
|
||||
State: 1
|
||||
[!0&1] 1
|
||||
[0&!1] 2
|
||||
[0&!1] 6
|
||||
[0&1] 9
|
||||
[!0&1] 14
|
||||
[!0&1] 20
|
||||
State: 2
|
||||
[!0&!1] 1
|
||||
[!0&1] 8
|
||||
[!0&!1] 20
|
||||
State: 3
|
||||
[0&1] 2
|
||||
[!0&1] 5
|
||||
[0&1] 18
|
||||
State: 4
|
||||
[0&!1] 4
|
||||
[0&1] 5
|
||||
[0&1] 6
|
||||
[0&!1] 17
|
||||
State: 5
|
||||
[0&1] 9
|
||||
State: 6
|
||||
[!0&1] 4
|
||||
[0&1] 5
|
||||
[!0&1] 9
|
||||
[!0&1] 12
|
||||
[!0&1] 17
|
||||
State: 7
|
||||
[0&!1] 3
|
||||
[!0&1] 5
|
||||
[!0&!1] 7 {0}
|
||||
[0&!1] 8
|
||||
State: 8
|
||||
[!0&!1] 3
|
||||
[!0&1] 4
|
||||
[!0&1] 8
|
||||
[!0&1] 12
|
||||
[!0&1] 13
|
||||
[!0&1] 17
|
||||
[!0&!1] 19
|
||||
State: 9
|
||||
[!0&1] 2
|
||||
[0&!1] 6
|
||||
[0&!1] 11
|
||||
[!0&1] 18
|
||||
State: 10
|
||||
[0&!1] 11 {0}
|
||||
State: 11
|
||||
[!0&1] 10 {0}
|
||||
[!0&1] 12 {0}
|
||||
State: 12
|
||||
[0&1] 11 {0}
|
||||
State: 13
|
||||
[!0&1] 12
|
||||
[!0&1] 13 {0}
|
||||
State: 14
|
||||
[!0&1] 14 {0}
|
||||
State: 15
|
||||
[0&1] 16
|
||||
State: 16
|
||||
[!0&1] 18 {0}
|
||||
State: 17
|
||||
[0&1] 15
|
||||
[0&!1] 17 {0}
|
||||
State: 18
|
||||
[!0&!1] 20 {0}
|
||||
State: 19
|
||||
[!0&1] 15
|
||||
[0&1] 18
|
||||
State: 20
|
||||
[0&1] 16 {0}
|
||||
[!0&1] 20 {0}
|
||||
--END--
|
||||
EOF
|
||||
|
||||
run 0 $autfilt -H --remove-fin test1 > output
|
||||
|
|
@ -1183,3 +1367,10 @@ diff -u output expected
|
|||
run 0 $autfilt -H --tgba test1 > output
|
||||
cat output
|
||||
diff -u output expected-tgba
|
||||
|
||||
# make sure the above expected automata are correct
|
||||
autcross --language-preserved 'autfilt --remove-fin' 'autfilt --tgba' -Ftest1
|
||||
|
||||
# try 10 small random automata just in case
|
||||
randaut -A'random 6' -Q10 -n10 3 |
|
||||
autcross --verbose --language-preserved 'autfilt --remove-fin' 'autfilt --tgba'
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue