From e48506f5484c216a085ea9108ed8d35685e166e5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 4 Jul 2024 12:11:10 +0200 Subject: [PATCH] improve some comments * spot/twaalgos/complement.hh, spot/twaalgos/complement.cc: Here. --- spot/twaalgos/complement.cc | 7 ++++--- spot/twaalgos/complement.hh | 3 ++- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/spot/twaalgos/complement.cc b/spot/twaalgos/complement.cc index 00e9cb0ce..9fad4eac4 100644 --- a/spot/twaalgos/complement.cc +++ b/spot/twaalgos/complement.cc @@ -515,7 +515,7 @@ namespace spot twa_graph_ptr res = dualize(aut); // There are cases with "t" acceptance that get converted to // Büchi during completion, then dualized to co-Büchi, but the - // acceptance is still not used. To try to clean it up in this + // acceptance is still not used. Try to clean it up in this // case. if (aut->num_sets() == 0 || // Also dualize removes sink states, but doesn't simplify @@ -525,8 +525,9 @@ namespace spot return res; } if (is_very_weak_automaton(aut)) - // removing alternation may need more acceptance sets than we support. - // in this case res==nullptr and we try the other determinization. + // Removing alternation may need more acceptance sets than Spot + // supports. When this happens res==nullptr and we fall back to + // determinization-based complementation. if (twa_graph_ptr res = remove_alternation(dualize(aut), false, aborter, false)) return res; diff --git a/spot/twaalgos/complement.hh b/spot/twaalgos/complement.hh index 4b74f27b8..6bb8ff1d9 100644 --- a/spot/twaalgos/complement.hh +++ b/spot/twaalgos/complement.hh @@ -73,7 +73,8 @@ namespace spot /// If an output_aborter is supplied, it is used to /// abort the construction of larger automata. /// - /// complement_semidet() is not yet used. + /// complement_semidet() is not yet used, as it is not always better + /// when the input is semi-deterministic. SPOT_API twa_graph_ptr complement(const const_twa_graph_ptr& aut, const output_aborter* aborter = nullptr);