diff --git a/spot/twaalgos/product.hh b/spot/twaalgos/product.hh index 7ca09ee39..ef8d47374 100644 --- a/spot/twaalgos/product.hh +++ b/spot/twaalgos/product.hh @@ -26,24 +26,80 @@ namespace spot { - // The tgba constructed by product() below contain property named - // "product-states" with type product_states. + /// \brief Automata constructed by product() contain a property + /// named "product-states" with this type typedef std::vector> product_states; + /// \ingroup twa_algorithms + /// \brief Intersect two automata using a synchronous product + /// + /// The resulting automaton will accept the intersection of both + /// languages and have an acceptance condition that is the + /// conjunction of the acceptance conditions of the two input + /// automata. + /// + /// The algorithm also defines a named property called + /// "product-states" with type spot::product_states. This stores + /// the pair of original state numbers associated to each state of + /// the product. SPOT_API twa_graph_ptr product(const const_twa_graph_ptr& left, const const_twa_graph_ptr& right); + /// \ingroup twa_algorithms + /// \brief Intersect two automata using a synchronous product + /// + /// These variant allow changing the initial state of both automata + /// in case you want to start the product at a different place. + /// + /// The resulting automaton will accept the intersection of the + /// languages recognized by each input automaton (with its initial + /// state changed) and have an acceptance condition that is the + /// conjunction of the acceptance conditions of the two input + /// automata. + /// + /// The algorithm also defines a named property called + /// "product-states" with type spot::product_states. This stores + /// the pair of original state numbers associated to each state of + /// the product. SPOT_API twa_graph_ptr product(const const_twa_graph_ptr& left, const const_twa_graph_ptr& right, unsigned left_state, unsigned right_state); + /// \ingroup twa_algorithms + /// \brief Sum two automata using a synchronous product + /// + /// The resulting automaton will accept the union of both + /// languages and have an acceptance condition that is the + /// disjunction of the acceptance conditions of the two input + /// automata. + /// + /// The algorithm also defines a named property called + /// "product-states" with type spot::product_states. This stores + /// the pair of original state numbers associated to each state of + /// the product. SPOT_API twa_graph_ptr product_or(const const_twa_graph_ptr& left, const const_twa_graph_ptr& right); + /// \ingroup twa_algorithms + /// \brief Sum two automata using a synchronous product + /// + /// These variant allow changing the initial state of both automata + /// in case you want to start the product at a different place. + /// + /// The resulting automaton will accept the sum of the languages + /// recognized by each input automaton (with its initial state + /// changed) and have an acceptance condition that is the + /// disjunction of the acceptance conditions of the two input + /// automata. + /// + /// The algorithm also defines a named property called + /// "product-states" with type spot::product_states. This stores + /// the pair of original state numbers associated to each state of + /// the product. SPOT_API twa_graph_ptr product_or(const const_twa_graph_ptr& left, const const_twa_graph_ptr& right, diff --git a/spot/twaalgos/remfin.hh b/spot/twaalgos/remfin.hh index 4908c3705..f53dee551 100644 --- a/spot/twaalgos/remfin.hh +++ b/spot/twaalgos/remfin.hh @@ -23,11 +23,12 @@ namespace spot { - /// \brief Convert a state-based Rabin automaton to Büchi automaton, - /// preserving determinism when possible. + /// \ingroup twa_algorithms + /// \brief Convert a Rabin automaton to Büchi automaton, preserving + /// determinism when possible. /// - /// Return nullptr if the input is not a Rabin automaton, or is not - /// state-based. + /// Return nullptr if the input is not a Rabin (or Rabin-like) + /// automaton. /// /// This essentially applies the algorithm from "Deterministic /// ω-automata vis-a-vis Deterministic Büchi Automata", S. Krishnan, @@ -39,7 +40,13 @@ namespace spot SPOT_API twa_graph_ptr rabin_to_buchi_maybe(const const_twa_graph_ptr& aut); + /// \ingroup twa_algorithms /// \brief Rewrite an automaton without Fin acceptance. + /// + /// This algorithm dispatches between many strategies. It has + /// dedicated algorithms for weak automata, automata with Rabin-like + /// acceptance, automata with Streett-like acceptance, and some + /// generic code that will work on any kind of acceptance condition. SPOT_API twa_graph_ptr remove_fin(const const_twa_graph_ptr& aut); } diff --git a/spot/twaalgos/sum.hh b/spot/twaalgos/sum.hh index 651035ab6..2ad5a2e1b 100644 --- a/spot/twaalgos/sum.hh +++ b/spot/twaalgos/sum.hh @@ -24,6 +24,7 @@ namespace spot { + /// \ingroup twa_algorithms /// \brief Sum two twa into a new twa, performing the union of the two input /// automata. /// @@ -34,6 +35,7 @@ namespace spot twa_graph_ptr sum(const const_twa_graph_ptr& left, const const_twa_graph_ptr& right); + /// \ingroup twa_algorithms /// \brief Sum two twa into a new twa, performing the union of the two input /// automata. /// @@ -48,6 +50,7 @@ namespace spot unsigned left_state, unsigned right_state); + /// \ingroup twa_algorithms /// \brief Sum two twa into a new twa, using a universal initial transition, /// performing the intersection of the two languages of the input automata. /// @@ -58,6 +61,7 @@ namespace spot twa_graph_ptr sum_and(const const_twa_graph_ptr& left, const const_twa_graph_ptr& right); + /// \ingroup twa_algorithms /// \brief Sum two twa into a new twa, using a universal initial transition, /// performing the intersection of the two languages of the input automata. /// diff --git a/spot/twaalgos/totgba.hh b/spot/twaalgos/totgba.hh index c68f10184..f43f52fa2 100644 --- a/spot/twaalgos/totgba.hh +++ b/spot/twaalgos/totgba.hh @@ -25,22 +25,35 @@ namespace spot { + /// \ingroup twa_algorithms /// \brief Take an automaton with any acceptance condition and return /// an equivalent Generalized Büchi automaton. + /// + /// This dispatch between many algorithms. If the input has Streett + /// (or Streett-like) acceptance, + /// spot::streett_to_generalized_buchi() is called right away and + /// produces a TGBA. Otherwise, it calls spot::remove_in() which + /// returns a TBA. SPOT_API twa_graph_ptr to_generalized_buchi(const const_twa_graph_ptr& aut); + /// \ingroup twa_algorithms /// \brief Convert Streett acceptance into generalized Büchi /// acceptance. SPOT_API twa_graph_ptr streett_to_generalized_buchi(const const_twa_graph_ptr& in); + /// \ingroup twa_algorithms /// \brief Convert Streett acceptance into generalized Büchi - /// only if SPOT_STREET_CONF_MIN is set to a number of pairs - /// less than the number of pairs used by IN. + /// + /// This version only works SPOT_STREET_CONF_MIN is set to a number + /// of pairs less than the number of pairs used by \a in. The + /// default is 3. It returns nullptr of that condition is not met, + /// or if the input automaton does not have Streett-like acceptance. SPOT_API twa_graph_ptr streett_to_generalized_buchi_maybe(const const_twa_graph_ptr& in); + /// \ingroup twa_algorithms /// \brief Take an automaton with any acceptance condition and return /// an equivalent Generalized Rabin automaton. /// @@ -55,6 +68,7 @@ namespace spot to_generalized_rabin(const const_twa_graph_ptr& aut, bool share_inf = false); + /// \ingroup twa_algorithms /// \brief Take an automaton with any acceptance condition and return /// an equivalent Generalized Streett automaton. ///