to_dca/to_nca: fix handling of co-Büchi input
* spot/twaalgos/cobuchi.cc (to_dca, to_nca): Do not process the input if it is already co-Büchi. * tests/core/dca.test: Test this. * NEWS: Mention the bug.
This commit is contained in:
parent
a9bf4dfa58
commit
5e2a8a581a
3 changed files with 35 additions and 3 deletions
5
NEWS
5
NEWS
|
|
@ -1,6 +1,9 @@
|
|||
New in spot 2.5.2.dev (not yet released)
|
||||
|
||||
Nothing yet.
|
||||
Bugs fixed:
|
||||
|
||||
- "autfilt --cobuchi --small/--det" would turn a transition-based
|
||||
co-Büchi automaton into a state-based co-Büchi.
|
||||
|
||||
New in spot 2.5.2 (2018-03-25)
|
||||
|
||||
|
|
|
|||
|
|
@ -337,6 +337,9 @@ namespace spot
|
|||
twa_graph_ptr
|
||||
to_nca(const_twa_graph_ptr aut, bool named_states)
|
||||
{
|
||||
if (aut->acc().is_co_buchi())
|
||||
return make_twa_graph(aut, twa::prop_set::all());
|
||||
|
||||
if (auto weak = weak_to_cobuchi(aut))
|
||||
return weak;
|
||||
|
||||
|
|
@ -683,8 +686,12 @@ namespace spot
|
|||
to_dca(const_twa_graph_ptr aut, bool named_states)
|
||||
{
|
||||
if (is_deterministic(aut))
|
||||
if (auto weak = weak_to_cobuchi(aut))
|
||||
return weak;
|
||||
{
|
||||
if (aut->acc().is_co_buchi())
|
||||
return make_twa_graph(aut, twa::prop_set::all());
|
||||
if (auto weak = weak_to_cobuchi(aut))
|
||||
return weak;
|
||||
}
|
||||
|
||||
const acc_cond::acc_code& code = aut->get_acceptance();
|
||||
|
||||
|
|
|
|||
|
|
@ -369,3 +369,25 @@ State: 1 [!1] 1 {0 2} [!0&!1] 2 [1] 3 [!0&1] 4 State: 2 [!0&!1] 2 {0 3}
|
|||
[1] 7 {2} [!1] 8 {2} State: 9 [1] 3 {2} [!0] 4 [!1] 9 {2} State: 10 [1]
|
||||
7 [!1] 10 {0 2} --END--
|
||||
EOF
|
||||
|
||||
cat >in.hoa <<EOF
|
||||
HOA: v1
|
||||
name: "FGa"
|
||||
States: 1
|
||||
Start: 0
|
||||
AP: 1 "a"
|
||||
acc-name: co-Buchi
|
||||
Acceptance: 1 Fin(0)
|
||||
properties: trans-labels explicit-labels trans-acc complete
|
||||
properties: deterministic stutter-invariant
|
||||
--BODY--
|
||||
State: 0
|
||||
[0] 0
|
||||
[!0] 0 {0}
|
||||
--END--
|
||||
EOF
|
||||
# We had a problem that to_nca()/to_dca() would call sbacc()
|
||||
# even if the input was already of the good shape. Make sure
|
||||
# this is not the case anymore.
|
||||
test '1,co-Buchi' = "`autfilt --cobuchi --small --stats='%s,%[]g' in.hoa`"
|
||||
test '1,co-Buchi' = "`autfilt --cobuchi --det --stats='%s,%[]g' in.hoa`"
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue