diff --git a/NEWS b/NEWS index 958ea1645..7a15bd1ac 100644 --- a/NEWS +++ b/NEWS @@ -126,6 +126,10 @@ New in spot 2.11.6.dev (not yet released) weak automata as input, but the documentation did not reflect this. + - spot::remove_alternation() has a new argument to decide whether it + should raise an exception of return nullptr if it requires more + acceptance sets than supported. + Python: - The spot.automata() and spot.automaton() functions now accept a @@ -200,6 +204,9 @@ New in spot 2.11.6.dev (not yet released) purge_dead_state(), did not update the highlight-edges property. (Issue #555.) + - spot::minimize_obligation will skip attempts to complement very + weak automata when those would require too many acceptance sets. + New in spot 2.11.6 (2023-08-01) Bug fixes: diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc index 88ca240eb..1de366b66 100644 --- a/spot/twaalgos/alternation.cc +++ b/spot/twaalgos/alternation.cc @@ -347,7 +347,8 @@ namespace spot } - twa_graph_ptr run(bool named_states, const output_aborter* aborter) + twa_graph_ptr run(bool named_states, const output_aborter* aborter, + bool raise_if_too_many_sets) { // First, we classify each SCC into three possible classes: // @@ -356,6 +357,10 @@ namespace spot // 3) rejecting of size >1 classify_each_scc(); + if (!raise_if_too_many_sets && + (has_reject_more_ + reject_1_count_) > SPOT_MAX_ACCSETS) + return nullptr; + // Rejecting SCCs of size 1 can be handled using genralized // Büchi acceptance, using one set per SCC, as in Gastin & // Oddoux CAV'01. See also Boker & et al. ICALP'10. Larger @@ -367,6 +372,7 @@ namespace spot // We preserve deterministic-like properties, and // stutter-invariance. res->prop_copy(aut_, {false, false, false, true, true, true}); + // This will raise an exception if we request too many sets. res->set_generalized_buchi(has_reject_more_ + reject_1_count_); // We for easier computation of outgoing sets, we will @@ -502,14 +508,15 @@ namespace spot twa_graph_ptr remove_alternation(const const_twa_graph_ptr& aut, bool named_states, - const output_aborter* aborter) + const output_aborter* aborter, + bool raise_if_too_many_sets) { if (aut->is_existential()) // Nothing to do, why was this function called at all? return std::const_pointer_cast(aut); alternation_remover ar(aut); - return ar.run(named_states, aborter); + return ar.run(named_states, aborter, raise_if_too_many_sets); } diff --git a/spot/twaalgos/alternation.hh b/spot/twaalgos/alternation.hh index e782856af..1e0ba87ed 100644 --- a/spot/twaalgos/alternation.hh +++ b/spot/twaalgos/alternation.hh @@ -100,12 +100,17 @@ namespace spot /// \param named_states name each state for easier debugging /// /// \param aborter Return nullptr if the built automaton would - /// be larger than the size specified by the \a aborter. + /// be larger than the size specified by the \a aborter, or + /// if it would require too many acceptance sets. + /// + /// \param raise_if_too_many_sets when set to false, return + /// nullptr in cases where we would need too many colors /// @} SPOT_API twa_graph_ptr remove_alternation(const const_twa_graph_ptr& aut, bool named_states = false, - const output_aborter* aborter = nullptr); + const output_aborter* aborter = nullptr, + bool raise_if_too_many_sets = true); // Remove universal edges on the fly. diff --git a/spot/twaalgos/complement.cc b/spot/twaalgos/complement.cc index 0a7f0cc16..7e38e519a 100644 --- a/spot/twaalgos/complement.cc +++ b/spot/twaalgos/complement.cc @@ -512,7 +512,11 @@ namespace spot if (!aut->is_existential() || is_universal(aut)) return dualize(aut); if (is_very_weak_automaton(aut)) - return remove_alternation(dualize(aut), aborter); + // removing alternation may need more acceptance sets than we support. + // in this case res==nullptr and we try the other determinization. + if (twa_graph_ptr res = remove_alternation(dualize(aut), false, + aborter, false)) + return res; // Determinize spot::option_map m; if (aborter) diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc index faaca1cae..40e176d2e 100644 --- a/spot/twaalgos/minimize.cc +++ b/spot/twaalgos/minimize.cc @@ -681,7 +681,10 @@ namespace spot else if (is_very_weak_automaton(aut_f)) { // Very weak automata are easy to complement. - aut_neg_f = remove_alternation(dualize(aut_f)); + aut_neg_f = remove_alternation(dualize(aut_f), false, + nullptr, false); + if (!aut_neg_f) // this required too many colors + return nullptr; } else { diff --git a/tests/core/optba.test b/tests/core/optba.test index 916794e66..c31d7081f 100755 --- a/tests/core/optba.test +++ b/tests/core/optba.test @@ -170,3 +170,827 @@ State: 1 "T2" [0&1] 1 [0&1] 2 [!0&!1] 2 [0&1] 3 [!0&!1] 1 State: 2 "T1" {0} [0&1] 2 State: 3 "all" {0} [t] 3 --END-- EOF test '3,6' = `autfilt --small in --stats=%s,%e` + + + +# The following TGBA was supplied by Yann Thierry-Mieg +# and caused minimize_obligation to call remove_alternation +# for complementation, but it required too many colors. + +cat >in.hoa <