diff --git a/NEWS b/NEWS index 57690f32b..a07a0d449 100644 --- a/NEWS +++ b/NEWS @@ -5,8 +5,13 @@ New in spot 2.1.2.dev (not yet released) * is_unambiguous() was rewritten in a more efficient way. * scc_info learned to determine the acceptance of simple SCCs made - of a single self-loop without ressorting to remove_fin() for complex - acceptance conditions. + of a single self-loop without ressorting to remove_fin() for complex + acceptance conditions. + + * remove_fin() has been improved to better deal with automata with + "unclean" acceptance, i.e., acceptance sets that are declared but + not used. In particular, this helps scc_info to be more efficient + at deciding the acceptance of SCCs in presence of Fin acceptance. New in spot 2.1.2 (2016-10-14) diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 136ad3936..848f9f189 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -979,7 +979,7 @@ namespace spot::strip_acceptance_here(aut); if (opt_merge) aut->merge_edges(); - if (opt_clean_acc || opt_rem_fin) + if (opt_clean_acc) cleanup_acceptance_here(aut); if (opt_sep_sets) separate_sets_here(aut); diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 1525fba41..acabd545d 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -517,6 +517,20 @@ namespace spot if (auto maybe = rabin_to_buchi_maybe(aut)) return maybe; + { + // We want a clean acceptance condition, i.e., one where all + // sets are useful. If that is not the case, clean it first. + acc_cond::mark_t unused = aut->acc().all_sets(); + for (auto& t: aut->edges()) + { + unused -= t.acc; + if (!unused) + break; + } + if (unused) + return remove_fin(cleanup_acceptance(aut)); + } + std::vector code; std::vector rem; std::vector keep; diff --git a/tests/core/remfin.test b/tests/core/remfin.test index 0b27f7dde..16d2fb978 100755 --- a/tests/core/remfin.test +++ b/tests/core/remfin.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015 Laboratoire de Recherche et Développement +# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -206,8 +206,40 @@ deterministic complete stutter-insensitive comment: "Safra[NBA=3]" acc-name: Rabin 2 Acceptance: 4 (Fin(0)&Inf(1))|(Fin(2)&Inf(3)) Start: 1 AP: 2 "p0" "p1" --BODY-- State: 0 {2} 2 0 2 3 State: 1 {0 2} 2 1 2 2 State: 2 {1 2} 2 0 2 2 State: 3 {3} 2 0 2 3 --END-- +/* This is the square of smaller.hoa from #188. */ +HOA: v1 States: 37 Start: 0 AP: 2 "a" "b" Acceptance: 24 (Inf(11) | +Fin(5)) & (Inf(10) | Fin(4)) & (Inf(9) | Fin(3)) & (Inf(8) | Fin(2)) & +(Inf(7) | Fin(1)) & (Inf(6) | Fin(0)) & (Inf(23) | Fin(17)) & (Inf(22) +| Fin(16)) & (Inf(21) | Fin(15)) & (Inf(20) | Fin(14)) & (Inf(19) | +Fin(13)) & (Inf(18) | Fin(12)) properties: trans-labels explicit-labels +trans-acc complete --BODY-- State: 0 [!0] 0 {0 12} [0] 1 [0&1] 2 [0&1] +3 [0&1] 4 State: 1 [t] 1 {1 13} [1] 2 {1} [1] 3 {13} [1] 4 State: 2 +[t] 2 {1 14} [!1] 5 {1} [1] 4 {14} State: 3 [t] 3 {2 13} [1] 4 {2} [!1] +6 {13} State: 4 [t] 4 {2 14} [!1] 7 {2} [!1] 8 {14} [!1] 9 State: 5 [t] +5 {1 15} [1] 10 {1} [1] 7 {15} [1] 11 State: 6 [t] 6 {3 13} [1] 8 {3} +[1] 12 {13} [1] 13 State: 7 [t] 7 {2 15} [1] 11 {2} [!1] 9 {15} State: +8 [t] 8 {3 14} [!1] 9 {3} [1] 13 {14} State: 9 [t] 9 {3 15} [1] 14 {3} +[1] 15 {15} [1] 16 State: 10 [t] 10 {1 16} [!1] 17 {1} [1] 11 {16} +State: 11 [t] 11 {2 16} [!1] 18 {2} [!1] 14 {16} [!1] 19 State: 12 [t] +12 {4 13} [1] 13 {4} [!1] 20 {13} State: 13 [t] 13 {4 14} [!1] 15 {4} +[!1] 21 {14} [!1] 22 State: 14 [t] 14 {3 16} [!1] 19 {3} [1] 16 {16} +State: 15 [t] 15 {4 15} [1] 16 {4} [!1] 22 {15} State: 16 [t] 16 {4 16} +[!1] 23 {4} [!1] 24 {16} [!1] 25 State: 17 [1] 26 {1 23} [!1] 17 {1 17} +[1] 27 {23} State: 18 [1] 27 {2 23} [!1] 18 {2 17} [!1] 19 {17} State: +19 [1] 28 {3 23} [!1] 19 {3 17} [1] 29 {23} State: 20 [1] 30 {11 13} +[1] 31 {11} [!1] 20 {5 13} State: 21 [1] 31 {11 14} [!1] 21 {5 14} [!1] +22 {5} State: 22 [1] 32 {11 15} [1] 33 {11} [!1] 22 {5 15} State: 23 +[1] 29 {4 23} [!1] 23 {4 17} [!1] 25 {17} State: 24 [1] 33 {11 16} [!1] +24 {5 16} [!1] 25 {5} State: 25 [1] 34 {11 23} [!1] 25 {5 17} State: 26 +[t] 26 {1} [1] 27 State: 27 [t] 27 {2} [!1] 28 State: 28 [t] 28 {3} [1] +29 State: 29 [t] 29 {4} [!1] 35 State: 30 [t] 30 {13} [1] 31 State: 31 +[t] 31 {14} [!1] 32 State: 32 [t] 32 {15} [1] 33 State: 33 [t] 33 {16} +[!1] 36 State: 34 [t] 34 State: 35 [1] 34 {11} [!1] 35 {5} State: 36 +[1] 34 {23} [!1] 36 {17} --END-- EOF +acctwelve='Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4)&Inf(5)' +acctwelve=$acctwelve'&Inf(6)&Inf(7)&Inf(8)&Inf(9)&Inf(10)&Inf(11)' cat >expected <expected-tgba < output