diff --git a/src/dstarparse/public.hh b/src/dstarparse/public.hh index 18440120c..4e461f896 100644 --- a/src/dstarparse/public.hh +++ b/src/dstarparse/public.hh @@ -30,7 +30,7 @@ namespace spot { - /// \addtogroup tgba_io + /// \addtogroup twa_io /// @{ /// \brief A parse diagnostic with its location. diff --git a/src/hoaparse/public.hh b/src/hoaparse/public.hh index cf5d56ded..4029ce516 100644 --- a/src/hoaparse/public.hh +++ b/src/hoaparse/public.hh @@ -30,7 +30,7 @@ namespace spot { - /// \addtogroup tgba_io + /// \addtogroup twa_io /// @{ #ifndef SWIG diff --git a/src/kripke/fairkripke.hh b/src/kripke/fairkripke.hh index 4c6b0a920..9ef7587c3 100644 --- a/src/kripke/fairkripke.hh +++ b/src/kripke/fairkripke.hh @@ -23,7 +23,7 @@ #include "fwd.hh" /// \addtogroup kripke Kripke Structures -/// \ingroup tgba +/// \ingroup twa namespace spot { diff --git a/src/kripke/kripkeprint.hh b/src/kripke/kripkeprint.hh index 0761ceb9c..733192944 100644 --- a/src/kripke/kripkeprint.hh +++ b/src/kripke/kripkeprint.hh @@ -26,7 +26,7 @@ namespace spot { - /// \ingroup tgba_io + /// \ingroup twa_io /// \brief Save the reachable part of Kripke structure in text format. /// /// The states will be named with the value returned by the @@ -38,7 +38,7 @@ namespace spot SPOT_API std::ostream& kripke_save_reachable(std::ostream& os, const const_kripke_ptr& k); - /// \ingroup tgba_io + /// \ingroup twa_io /// \brief Save the reachable part of Kripke structure in text format. /// /// States will be renumbered with sequential number. This is much diff --git a/src/tgba/bdddict.hh b/src/tgba/bdddict.hh index eea37dfd9..61f28d817 100644 --- a/src/tgba/bdddict.hh +++ b/src/tgba/bdddict.hh @@ -36,7 +36,7 @@ namespace spot /// \brief Private data for bdd_dict. class bdd_dict_priv; - /// \ingroup tgba_essentials + /// \ingroup twa_essentials /// \brief Map BDD variables to formulae. /// /// The BDD library uses integers to designate Boolean variables in diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index d5869706f..54d752fd6 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -35,7 +35,7 @@ namespace spot { - /// \ingroup tgba_essentials + /// \ingroup twa_essentials /// \brief Abstract class for states. class SPOT_API state { @@ -100,7 +100,7 @@ namespace spot } }; - /// \ingroup tgba_essentials + /// \ingroup twa_essentials /// \brief Strict Weak Ordering for \c state*. /// /// This is meant to be used as a comparison functor for @@ -122,7 +122,7 @@ namespace spot } }; - /// \ingroup tgba_essentials + /// \ingroup twa_essentials /// \brief An Equivalence Relation for \c state*. /// /// This is meant to be used as a comparison functor for @@ -145,7 +145,7 @@ namespace spot } }; - /// \ingroup tgba_essentials + /// \ingroup twa_essentials /// \ingroup hash_funcs /// \brief Hash Function for \c state*. /// @@ -173,7 +173,7 @@ namespace spot state_ptr_hash, state_ptr_equal> state_set; - /// \ingroup tgba_essentials + /// \ingroup twa_essentials /// \brief Render state pointers unique via a hash table. class SPOT_API state_unicity_table { @@ -238,7 +238,7 @@ namespace spot inline void shared_state_deleter(state* s) { s->destroy(); } - /// \ingroup tgba_essentials + /// \ingroup twa_essentials /// \brief Strict Weak Ordering for \c shared_state /// (shared_ptr). /// @@ -262,7 +262,7 @@ namespace spot } }; - /// \ingroup tgba_essentials + /// \ingroup twa_essentials /// \brief An Equivalence Relation for \c shared_state /// (shared_ptr). /// @@ -288,7 +288,7 @@ namespace spot } }; - /// \ingroup tgba_essentials + /// \ingroup twa_essentials /// \ingroup hash_funcs /// \brief Hash Function for \c shared_state (shared_ptr). /// @@ -318,7 +318,7 @@ namespace spot state_shared_ptr_hash, state_shared_ptr_equal> shared_state_set; - /// \ingroup tgba_essentials + /// \ingroup twa_essentials /// \brief Iterate over the successors of a state. /// /// This class provides the basic functionalities required to @@ -441,10 +441,10 @@ namespace spot /// algorithms that work on spot::twa are \ref tgba_algorithms /// "listed separately". - /// \addtogroup tgba_essentials Essential TωA types + /// \addtogroup twa_essentials Essential TωA types /// \ingroup twa - /// \ingroup tgba_essentials + /// \ingroup twa_essentials /// \brief A Transition-based ω-Automaton. /// /// The acronym TωA stands for Transition-based ω-automaton. @@ -845,27 +845,27 @@ namespace spot }; - /// \addtogroup tgba_representation TGBA representations + /// \addtogroup twa_representation TGBA representations /// \ingroup twa - /// \addtogroup tgba_algorithms TGBA algorithms + /// \addtogroup twa_algorithms TGBA algorithms /// \ingroup twa - /// \addtogroup tgba_on_the_fly_algorithms TGBA on-the-fly algorithms - /// \ingroup tgba_algorithms + /// \addtogroup twa_on_the_fly_algorithms TGBA on-the-fly algorithms + /// \ingroup twa_algorithms - /// \addtogroup tgba_io Input/Output of TGBA - /// \ingroup tgba_algorithms + /// \addtogroup twa_io Input/Output of TGBA + /// \ingroup twa_algorithms - /// \addtogroup tgba_ltl Translating LTL formulae into TGBA - /// \ingroup tgba_algorithms + /// \addtogroup twa_ltl Translating LTL formulae into TGBA + /// \ingroup twa_algorithms - /// \addtogroup tgba_generic Algorithm patterns - /// \ingroup tgba_algorithms + /// \addtogroup twa_generic Algorithm patterns + /// \ingroup twa_algorithms - /// \addtogroup tgba_reduction TGBA simplifications - /// \ingroup tgba_algorithms + /// \addtogroup twa_reduction TGBA simplifications + /// \ingroup twa_algorithms - /// \addtogroup tgba_misc Miscellaneous algorithms on TGBA - /// \ingroup tgba_algorithms + /// \addtogroup twa_misc Miscellaneous algorithms on TGBA + /// \ingroup twa_algorithms } diff --git a/src/tgba/tgbamask.cc b/src/tgba/tgbamask.cc index c3082a5ca..575994038 100644 --- a/src/tgba/tgbamask.cc +++ b/src/tgba/tgbamask.cc @@ -76,7 +76,7 @@ namespace spot transitions::const_iterator it_; }; - /// \ingroup tgba_on_the_fly_algorithms + /// \ingroup twa_on_the_fly_algorithms /// \brief A masked TGBA (abstract). /// /// Ignores some states from a TGBA. What state are preserved or diff --git a/src/tgba/tgbamask.hh b/src/tgba/tgbamask.hh index 94ca2803f..ef58f5159 100644 --- a/src/tgba/tgbamask.hh +++ b/src/tgba/tgbamask.hh @@ -25,7 +25,7 @@ namespace spot { - /// \ingroup tgba_on_the_fly_algorithms + /// \ingroup twa_on_the_fly_algorithms /// \brief Mask a TGBA, keeping a given set of states. /// /// Mask the TGBA \a to_mask, keeping only the @@ -36,7 +36,7 @@ namespace spot const state_set& to_keep, const state* init = 0); - /// \ingroup tgba_on_the_fly_algorithms + /// \ingroup twa_on_the_fly_algorithms /// \brief Mask a TGBA, rejecting a given set of states. /// /// Mask the TGBA \a to_mask, keeping only the states that are not @@ -48,7 +48,7 @@ namespace spot const state* init = 0); - /// \ingroup tgba_on_the_fly_algorithms + /// \ingroup twa_on_the_fly_algorithms /// \brief Mask a TGBA, rejecting some acceptance set of transitions. /// /// This will ignore all transitions that have the TO_IGNORE diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh index a2537242f..954744907 100644 --- a/src/tgba/tgbaproduct.hh +++ b/src/tgba/tgbaproduct.hh @@ -28,7 +28,7 @@ namespace spot { - /// \ingroup tgba_on_the_fly_algorithms + /// \ingroup twa_on_the_fly_algorithms /// \brief A state for spot::twa_product. /// /// This state is in fact a pair of state: the state from the left diff --git a/src/tgba/tgbaproxy.hh b/src/tgba/tgbaproxy.hh index 857e639a1..f028593b1 100644 --- a/src/tgba/tgbaproxy.hh +++ b/src/tgba/tgbaproxy.hh @@ -23,7 +23,7 @@ namespace spot { - /// \ingroup tgba_on_the_fly_algorithms + /// \ingroup twa_on_the_fly_algorithms /// \brief A TGBA proxy. /// /// This implements a simple proxy to an existing diff --git a/src/tgba/tgbasafracomplement.cc b/src/tgba/tgbasafracomplement.cc index e5a5fad8e..373c77c6e 100644 --- a/src/tgba/tgbasafracomplement.cc +++ b/src/tgba/tgbasafracomplement.cc @@ -827,7 +827,7 @@ namespace spot // state_complement /// States used by spot::tgba_safra_complement. - /// \ingroup tgba_representation + /// \ingroup twa_representation class state_complement : public state { public: @@ -954,7 +954,7 @@ namespace spot } /// Successor iterators used by spot::tgba_safra_complement. - /// \ingroup tgba_representation + /// \ingroup twa_representation class tgba_safra_complement_succ_iterator: public twa_succ_iterator { public: diff --git a/src/tgba/tgbasafracomplement.hh b/src/tgba/tgbasafracomplement.hh index 1078bdd1f..b325efcfd 100644 --- a/src/tgba/tgbasafracomplement.hh +++ b/src/tgba/tgbasafracomplement.hh @@ -29,7 +29,7 @@ namespace spot { - /// \ingroup tgba_on_the_fly_algorithms + /// \ingroup twa_on_the_fly_algorithms /// \brief Build a complemented automaton. /// /// It creates an automaton that recognizes the diff --git a/src/tgbaalgos/are_isomorphic.hh b/src/tgbaalgos/are_isomorphic.hh index 67dedcb0f..0c2845dc2 100644 --- a/src/tgbaalgos/are_isomorphic.hh +++ b/src/tgbaalgos/are_isomorphic.hh @@ -30,7 +30,7 @@ namespace spot public: isomorphism_checker(const const_twa_graph_ptr ref); - /// \ingroup tgba_misc + /// \ingroup twa_misc /// \brief Check whether an automaton is isomorphic to the one passed to /// the constructor. /// diff --git a/src/tgbaalgos/bfssteps.hh b/src/tgbaalgos/bfssteps.hh index eef653ac7..f6df574cd 100644 --- a/src/tgbaalgos/bfssteps.hh +++ b/src/tgbaalgos/bfssteps.hh @@ -27,7 +27,7 @@ namespace spot { - /// \ingroup tgba_misc + /// \ingroup twa_misc /// \brief Make a BFS in a spot::tgba to compute a tgba_run::steps. /// /// This class should be used to compute the shortest path diff --git a/src/tgbaalgos/canonicalize.hh b/src/tgbaalgos/canonicalize.hh index b1ab59176..fbb80a0d3 100644 --- a/src/tgbaalgos/canonicalize.hh +++ b/src/tgbaalgos/canonicalize.hh @@ -23,7 +23,7 @@ namespace spot { - /// \ingroup tgba_misc + /// \ingroup twa_misc /// \brief Reorder the states and transitions of aut in a way that will be the /// same for every isomorphic automata. SPOT_API twa_graph_ptr canonicalize(twa_graph_ptr aut); diff --git a/src/tgbaalgos/degen.hh b/src/tgbaalgos/degen.hh index c0c1541d3..58f6f0c68 100644 --- a/src/tgbaalgos/degen.hh +++ b/src/tgbaalgos/degen.hh @@ -23,7 +23,7 @@ namespace spot { - /// \ingroup tgba_misc + /// \ingroup twa_misc /// \brief Degeneralize a spot::tgba into an equivalent sba with /// only one acceptance condition. /// diff --git a/src/tgbaalgos/dotty.hh b/src/tgbaalgos/dotty.hh index e5c502cf3..b14948a28 100644 --- a/src/tgbaalgos/dotty.hh +++ b/src/tgbaalgos/dotty.hh @@ -28,7 +28,7 @@ namespace spot { - /// \ingroup tgba_io + /// \ingroup twa_io /// \brief Print reachable states in dot format. /// /// If \a assume_sba is set, this assumes that the automaton diff --git a/src/tgbaalgos/dupexp.hh b/src/tgbaalgos/dupexp.hh index cea32cba0..b12a1977b 100644 --- a/src/tgbaalgos/dupexp.hh +++ b/src/tgbaalgos/dupexp.hh @@ -29,12 +29,12 @@ namespace spot { - /// \ingroup tgba_misc + /// \ingroup twa_misc /// \brief Build an explicit automaton from all states of \a aut, /// numbering states in bread first order as they are processed. SPOT_API twa_graph_ptr tgba_dupexp_bfs(const const_twa_ptr& aut, twa::prop_set p); - /// \ingroup tgba_misc + /// \ingroup twa_misc /// \brief Build an explicit automaton from all states of \a aut, /// numbering states in depth first order as they are processed. SPOT_API twa_graph_ptr diff --git a/src/tgbaalgos/emptiness.hh b/src/tgbaalgos/emptiness.hh index 104592cca..3254f8342 100644 --- a/src/tgbaalgos/emptiness.hh +++ b/src/tgbaalgos/emptiness.hh @@ -37,7 +37,7 @@ namespace spot typedef std::shared_ptr const_tgba_run_ptr; /// \addtogroup emptiness_check Emptiness-checks - /// \ingroup tgba_algorithms + /// \ingroup twa_algorithms /// /// All emptiness-check algorithms follow the same interface. /// Basically once you have constructed an instance of @@ -258,7 +258,7 @@ namespace spot /// \ingroup emptiness_check - /// \addtogroup tgba_run TGBA runs and supporting functions + /// \addtogroup twa_run TGBA runs and supporting functions /// \ingroup emptiness_check /// @{ diff --git a/src/tgbaalgos/hoa.hh b/src/tgbaalgos/hoa.hh index 6b82cd637..a75a2d413 100644 --- a/src/tgbaalgos/hoa.hh +++ b/src/tgbaalgos/hoa.hh @@ -25,7 +25,7 @@ namespace spot { - /// \ingroup tgba_io + /// \ingroup twa_io /// \brief Print reachable states in Hanoi Omega Automata format. /// /// \param os The output stream to print on. diff --git a/src/tgbaalgos/isdet.hh b/src/tgbaalgos/isdet.hh index 04b428395..b062d09d9 100644 --- a/src/tgbaalgos/isdet.hh +++ b/src/tgbaalgos/isdet.hh @@ -23,7 +23,7 @@ namespace spot { - /// \addtogroup tgba_misc + /// \addtogroup twa_misc /// @{ /// \brief Count the number of non-deterministic states in \a aut. diff --git a/src/tgbaalgos/isweakscc.hh b/src/tgbaalgos/isweakscc.hh index 33cfb7b6e..8102039ea 100644 --- a/src/tgbaalgos/isweakscc.hh +++ b/src/tgbaalgos/isweakscc.hh @@ -23,7 +23,7 @@ namespace spot { - /// \addtogroup tgba_misc + /// \addtogroup twa_misc /// @{ /// \brief Whether the SCC number \a scc in \a map is inherently diff --git a/src/tgbaalgos/lbtt.hh b/src/tgbaalgos/lbtt.hh index b4c3edffe..4262c5f6f 100644 --- a/src/tgbaalgos/lbtt.hh +++ b/src/tgbaalgos/lbtt.hh @@ -27,7 +27,7 @@ namespace spot { - /// \ingroup tgba_io + /// \ingroup twa_io /// \brief Print reachable states in LBTT's format. /// /// \param g The automata to print. diff --git a/src/tgbaalgos/ltl2taa.hh b/src/tgbaalgos/ltl2taa.hh index 28832d301..4f1a64f1b 100644 --- a/src/tgbaalgos/ltl2taa.hh +++ b/src/tgbaalgos/ltl2taa.hh @@ -24,7 +24,7 @@ namespace spot { - /// \ingroup tgba_ltl + /// \ingroup twa_ltl /// \brief Build a spot::taa* from an LTL formula. /// /// This is based on the following. diff --git a/src/tgbaalgos/ltl2tgba_fm.hh b/src/tgbaalgos/ltl2tgba_fm.hh index c9449dcf7..ddf0a0019 100644 --- a/src/tgbaalgos/ltl2tgba_fm.hh +++ b/src/tgbaalgos/ltl2tgba_fm.hh @@ -29,7 +29,7 @@ namespace spot { - /// \ingroup tgba_ltl + /// \ingroup twa_ltl /// \brief Build a spot::twa_graph_ptr from an LTL formula. /// /// This is based on the following paper. diff --git a/src/tgbaalgos/minimize.hh b/src/tgbaalgos/minimize.hh index 3ffc3334b..f3c30bd6e 100644 --- a/src/tgbaalgos/minimize.hh +++ b/src/tgbaalgos/minimize.hh @@ -24,7 +24,7 @@ namespace spot { - /// \addtogroup tgba_reduction + /// \addtogroup twa_reduction /// @{ /// \brief Construct a minimal deterministic monitor. diff --git a/src/tgbaalgos/neverclaim.hh b/src/tgbaalgos/neverclaim.hh index 7cbc8e71b..10c44b7bd 100644 --- a/src/tgbaalgos/neverclaim.hh +++ b/src/tgbaalgos/neverclaim.hh @@ -28,7 +28,7 @@ namespace spot { - /// \ingroup tgba_io + /// \ingroup twa_io /// \brief Print reachable states in Spin never claim format. /// /// \param os The output stream to print on. diff --git a/src/tgbaalgos/postproc.hh b/src/tgbaalgos/postproc.hh index 7efb0461c..45e483ddf 100644 --- a/src/tgbaalgos/postproc.hh +++ b/src/tgbaalgos/postproc.hh @@ -25,7 +25,7 @@ namespace spot { class option_map; - /// \addtogroup tgba_reduction + /// \addtogroup twa_reduction /// @{ /// \brief Wrap TGBA/BA/Monitor post-processing algorithms in an diff --git a/src/tgbaalgos/powerset.hh b/src/tgbaalgos/powerset.hh index a27c4926e..fa14cd782 100644 --- a/src/tgbaalgos/powerset.hh +++ b/src/tgbaalgos/powerset.hh @@ -42,7 +42,7 @@ namespace spot }; - /// \ingroup tgba_misc + /// \ingroup twa_misc /// \brief Build a deterministic automaton, ignoring acceptance conditions. /// /// This create a deterministic automaton that recognizes the diff --git a/src/tgbaalgos/projrun.hh b/src/tgbaalgos/projrun.hh index 6afa2ddf2..7cc422f28 100644 --- a/src/tgbaalgos/projrun.hh +++ b/src/tgbaalgos/projrun.hh @@ -31,7 +31,7 @@ namespace spot { struct tgba_run; - /// \ingroup tgba_run + /// \ingroup twa_run /// \brief Project a tgba_run on a tgba. /// /// If a tgba_run has been generated on a product, or any other diff --git a/src/tgbaalgos/randomgraph.hh b/src/tgbaalgos/randomgraph.hh index 386a241b8..78abd8265 100644 --- a/src/tgbaalgos/randomgraph.hh +++ b/src/tgbaalgos/randomgraph.hh @@ -29,7 +29,7 @@ namespace spot { - /// \ingroup tgba_misc + /// \ingroup twa_misc /// \brief Construct a tgba randomly. /// /// \param n The number of states wanted in the automata (>0). All states diff --git a/src/tgbaalgos/reachiter.hh b/src/tgbaalgos/reachiter.hh index 7bde6d9e9..3054ec1cb 100644 --- a/src/tgbaalgos/reachiter.hh +++ b/src/tgbaalgos/reachiter.hh @@ -29,7 +29,7 @@ namespace spot { - /// \ingroup tgba_generic + /// \ingroup twa_generic /// \brief Iterate over all reachable states of a spot::tgba. class SPOT_API tgba_reachable_iterator { @@ -95,7 +95,7 @@ namespace spot seen_map seen; ///< States already seen. }; - /// \ingroup tgba_generic + /// \ingroup twa_generic /// \brief An implementation of spot::tgba_reachable_iterator that browses /// states breadth first. class SPOT_API tgba_reachable_iterator_breadth_first : @@ -111,7 +111,7 @@ namespace spot std::deque todo; ///< A queue of states yet to explore. }; - /// \ingroup tgba_generic + /// \ingroup twa_generic /// \brief Iterate over all states of an automaton using a DFS. class SPOT_API tgba_reachable_iterator_depth_first { @@ -177,7 +177,7 @@ namespace spot virtual void pop(); }; - /// \ingroup tgba_generic + /// \ingroup twa_generic /// \brief Iterate over all states of an automaton using a DFS. /// /// This variant also maintains a set of states that are on the DFS diff --git a/src/tgbaalgos/reducerun.hh b/src/tgbaalgos/reducerun.hh index 62dacfa45..c6b862a10 100644 --- a/src/tgbaalgos/reducerun.hh +++ b/src/tgbaalgos/reducerun.hh @@ -28,7 +28,7 @@ namespace spot { - /// \ingroup tgba_run + /// \ingroup twa_run /// \brief Reduce an accepting run. /// /// Return a run which is accepting for \a a and that is no longer diff --git a/src/tgbaalgos/replayrun.hh b/src/tgbaalgos/replayrun.hh index 44feee936..018595276 100644 --- a/src/tgbaalgos/replayrun.hh +++ b/src/tgbaalgos/replayrun.hh @@ -31,7 +31,7 @@ namespace spot { struct tgba_run; - /// \ingroup tgba_run + /// \ingroup twa_run /// \brief Replay a tgba_run on a tgba. /// /// This is similar to print_tgba_run(), except that the run is diff --git a/src/tgbaalgos/simulation.hh b/src/tgbaalgos/simulation.hh index 8e41c2c62..b716e15d9 100644 --- a/src/tgbaalgos/simulation.hh +++ b/src/tgbaalgos/simulation.hh @@ -24,7 +24,7 @@ namespace spot { - /// \addtogroup tgba_reduction + /// \addtogroup twa_reduction /// @{ /// @{ diff --git a/src/tgbaalgos/stats.hh b/src/tgbaalgos/stats.hh index dbee7f097..b7a8079c6 100644 --- a/src/tgbaalgos/stats.hh +++ b/src/tgbaalgos/stats.hh @@ -29,7 +29,7 @@ namespace spot { - /// \addtogroup tgba_misc + /// \addtogroup twa_misc /// @{ struct SPOT_API tgba_statistics diff --git a/src/tgbaalgos/stripacc.hh b/src/tgbaalgos/stripacc.hh index 67286a8a1..17714eef2 100644 --- a/src/tgbaalgos/stripacc.hh +++ b/src/tgbaalgos/stripacc.hh @@ -23,7 +23,7 @@ namespace spot { - /// \ingroup tgba_misc + /// \ingroup twa_misc /// \brief Remove all acceptance sets from a twa_graph. /// /// This is equivalent to marking all states/transitions as accepting. diff --git a/src/tgbaalgos/translate.hh b/src/tgbaalgos/translate.hh index 061c99e24..f23bfa280 100644 --- a/src/tgbaalgos/translate.hh +++ b/src/tgbaalgos/translate.hh @@ -24,7 +24,7 @@ namespace spot { - /// \ingroup tgba_ltl + /// \ingroup twa_ltl /// \brief Translate an LTL formula into an optimized spot::tgba. /// /// This class implements a three-step translation: