diff --git a/ChangeLog b/ChangeLog index 78395aa98..01b2e94c1 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,16 @@ 2004-11-17 Alexandre Duret-Lutz + * src/tgba/tgba.hh, src/tgbaalgos/dotty.hh, + src/tgbaalgos/dottydec.hh, src/tgbaalgos/dupexp.hh, + src/tgbaalgos/emptiness.hh, src/tgbaalgos/lbtt.hh, + src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.hh, + src/tgbaalgos/neverclaim.hh, src/tgbaalgos/powerset.hh, + src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.hh, + src/tgbaalgos/reachiter.hh, src/tgbaalgos/reductgba_sim.hh, + src/tgbaalgos/replayrun.hh, src/tgbaalgos/rundotdec.hh + src/tgbaalgos/save.hh, src/tgbaalgos/stats.hh, + src/tgbaparse/public.hh: Add Doxygen groups for TGBA algorithms. + * src/ltlast/atomic_prop.hh, src/ltlast/binop.hh, src/ltlast/constant.hh, src/ltlast/formula.hh, src/ltlast/multop.hh, src/ltlast/refformula.hh, @@ -13,7 +24,6 @@ groups for LTL algorithms and types. * doc/Makefile.am (fast-doc): New target. - * src/misc/hashfunc.hh: Include cstddef to define size_t, and guard the file for multiple inclusions. diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index b3391a582..02c107342 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -218,11 +218,26 @@ namespace spot /// \addtogroup tgba_representation TGBA representations /// \ingroup tgba - /// \addtogroup tgba_on_the_fly_algorithms TGBA on-the-fly algorithms - /// \ingroup tgba - /// \addtogroup tgba_algorithms TGBA algorithms /// \ingroup tgba + + /// \addtogroup tgba_on_the_fly_algorithms TGBA on-the-fly algorithms + /// \ingroup tgba_algorithms + + /// \addtogroup tgba_io Input/Output of TGBA + /// \ingroup tgba_algorithms + + /// \addtogroup tgba_ltl Translating LTL formulae into TGBA + /// \ingroup tgba_algorithms + + /// \addtogroup tgba_generic Algorithm patterns + /// \ingroup tgba_algorithms + + /// \addtogroup tgba_reduction TGBA simplifications + /// \ingroup tgba_algorithms + + /// \addtogroup tgba_misc Miscellaneous algorithms on TGBA + /// \ingroup tgba_algorithms } #endif // SPOT_TGBA_TGBA_HH diff --git a/src/tgbaalgos/dotty.hh b/src/tgbaalgos/dotty.hh index f1c05ed40..28df1d03c 100644 --- a/src/tgbaalgos/dotty.hh +++ b/src/tgbaalgos/dotty.hh @@ -30,6 +30,10 @@ namespace spot class tgba; /// \brief Print reachable states in dot format. + /// \ingroup tgba_io + /// The \a dd argument allows to customize the output in various + /// ways. See \ref tgba_dotty "this page" for a list of available + /// decorators. std::ostream& dotty_reachable(std::ostream& os, const tgba* g, diff --git a/src/tgbaalgos/dottydec.hh b/src/tgbaalgos/dottydec.hh index fb7fb08b0..bf7a0fd17 100644 --- a/src/tgbaalgos/dottydec.hh +++ b/src/tgbaalgos/dottydec.hh @@ -30,7 +30,11 @@ namespace spot class tgba; class tgba_succ_iterator; - /// Choose state and link styles for spot::dotty_reachable. + /// \addtogroup tgba_dotty Decorating the dot output + /// \ingroup tgba_io + + /// \brief Choose state and link styles for spot::dotty_reachable. + /// \ingroup tgba_dotty class dotty_decorator { public: diff --git a/src/tgbaalgos/dupexp.hh b/src/tgbaalgos/dupexp.hh index d84145f70..0196f8e92 100644 --- a/src/tgbaalgos/dupexp.hh +++ b/src/tgbaalgos/dupexp.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -26,11 +26,13 @@ namespace spot { - /// Build an explicit automata from all states of \a aut, numbering - /// states in bread first order as they are processed. + /// \brief Build an explicit automata from all states of \a aut, + /// numbering states in bread first order as they are processed. + /// \ingroup tgba_misc tgba_explicit* tgba_dupexp_bfs(const tgba* aut); - /// Build an explicit automata from all states of \a aut, numbering - /// states in depth first order as they are processed. + /// \brief Build an explicit automata from all states of \a aut, + /// numbering states in depth first order as they are processed. + /// \ingroup tgba_misc tgba_explicit* tgba_dupexp_dfs(const tgba* aut); } diff --git a/src/tgbaalgos/emptiness.hh b/src/tgbaalgos/emptiness.hh index 2e730de81..ccf481b3f 100644 --- a/src/tgbaalgos/emptiness.hh +++ b/src/tgbaalgos/emptiness.hh @@ -32,7 +32,7 @@ namespace spot class tgba; struct tgba_run; - /// \addtogroup emptiness_check Emptiness-check + /// \addtogroup emptiness_check Emptiness-checks /// \ingroup tgba_algorithms /// /// All emptiness-check algorithms follow the same interface. diff --git a/src/tgbaalgos/lbtt.hh b/src/tgbaalgos/lbtt.hh index 5c6527368..d47a46946 100644 --- a/src/tgbaalgos/lbtt.hh +++ b/src/tgbaalgos/lbtt.hh @@ -28,6 +28,7 @@ namespace spot { /// \brief Print reachable states in LBTT format. + /// \ingroup tgba_io /// /// \param g The automata to print. /// \param os Where to print. diff --git a/src/tgbaalgos/ltl2tgba_fm.hh b/src/tgbaalgos/ltl2tgba_fm.hh index ef36d0522..f326ebc53 100644 --- a/src/tgbaalgos/ltl2tgba_fm.hh +++ b/src/tgbaalgos/ltl2tgba_fm.hh @@ -29,6 +29,7 @@ namespace spot { /// \brief Build a spot::tgba_explicit* from an LTL formula. + /// \ingroup tgba_ltl /// /// This is based on the following paper. /// \verbatim diff --git a/src/tgbaalgos/ltl2tgba_lacim.hh b/src/tgbaalgos/ltl2tgba_lacim.hh index 038348abe..d4b3b755d 100644 --- a/src/tgbaalgos/ltl2tgba_lacim.hh +++ b/src/tgbaalgos/ltl2tgba_lacim.hh @@ -27,7 +27,8 @@ namespace spot { - /// Build a spot::tgba_bdd_concrete from an LTL formula. + /// \brief Build a spot::tgba_bdd_concrete from an LTL formula. + /// \ingroup tgba_ltl /// /// This is based on the following paper. /// \verbatim diff --git a/src/tgbaalgos/neverclaim.hh b/src/tgbaalgos/neverclaim.hh index 3804dd263..2d2eb562b 100644 --- a/src/tgbaalgos/neverclaim.hh +++ b/src/tgbaalgos/neverclaim.hh @@ -29,6 +29,7 @@ namespace spot { /// \brief Print reachable states in Spin never claim format. + /// \ingroup tgba_io /// /// \param os The output stream to print on. /// \param g The degeneralized automaton to output. diff --git a/src/tgbaalgos/powerset.hh b/src/tgbaalgos/powerset.hh index 57ca22925..cc329ff9c 100644 --- a/src/tgbaalgos/powerset.hh +++ b/src/tgbaalgos/powerset.hh @@ -27,6 +27,7 @@ namespace spot { /// \brief Build a deterministic automaton, ignoring acceptance conditions. + /// \ingroup tgba_misc /// /// This create a deterministic automaton that recognize the /// same language as \a aut would if its acceptance conditions diff --git a/src/tgbaalgos/projrun.hh b/src/tgbaalgos/projrun.hh index 0f2140142..80dbc014d 100644 --- a/src/tgbaalgos/projrun.hh +++ b/src/tgbaalgos/projrun.hh @@ -30,6 +30,7 @@ namespace spot class tgba; /// \brief Project a tgba_run on a tgba. + /// \ingroup tgba_run /// /// If a tgba_run has been generated on a product, or any other /// on-the-fly algorithm with tgba operands, diff --git a/src/tgbaalgos/randomgraph.hh b/src/tgbaalgos/randomgraph.hh index 9a711058f..e4afe40dd 100644 --- a/src/tgbaalgos/randomgraph.hh +++ b/src/tgbaalgos/randomgraph.hh @@ -31,6 +31,7 @@ namespace spot class tgba; /// \brief Construct a tgba randomly. + /// \ingroup tgba_misc /// /// \param n The number of states wanted in the automata. All states /// will be connected, and there will be no dead state. diff --git a/src/tgbaalgos/reachiter.hh b/src/tgbaalgos/reachiter.hh index cb94879ae..1bfdd0823 100644 --- a/src/tgbaalgos/reachiter.hh +++ b/src/tgbaalgos/reachiter.hh @@ -30,6 +30,7 @@ namespace spot { /// \brief Iterate over all reachable states of a spot::tgba. + /// \ingroup tgba_generic class tgba_reachable_iterator { public: @@ -92,6 +93,7 @@ namespace spot /// \brief An implementation of spot::tgba_reachable_iterator that browses /// states depth first. + /// \ingroup tgba_generic class tgba_reachable_iterator_depth_first : public tgba_reachable_iterator { public: @@ -106,6 +108,7 @@ namespace spot /// \brief An implementation of spot::tgba_reachable_iterator that browses /// states breadth first. + /// \ingroup tgba_generic class tgba_reachable_iterator_breadth_first : public tgba_reachable_iterator { public: diff --git a/src/tgbaalgos/reductgba_sim.hh b/src/tgbaalgos/reductgba_sim.hh index f073b030f..d86fea2aa 100644 --- a/src/tgbaalgos/reductgba_sim.hh +++ b/src/tgbaalgos/reductgba_sim.hh @@ -32,6 +32,9 @@ namespace spot { + /// \addtogroup tgba_reduction + /// @{ + /// Options for reduce. enum reduce_tgba_options { @@ -327,6 +330,7 @@ namespace spot }; + /// @} } #endif diff --git a/src/tgbaalgos/replayrun.hh b/src/tgbaalgos/replayrun.hh index 2c5fc9889..da78ab414 100644 --- a/src/tgbaalgos/replayrun.hh +++ b/src/tgbaalgos/replayrun.hh @@ -30,6 +30,7 @@ namespace spot class tgba; /// \brief Replay a tgba_run on a tgba. + /// \ingroup tgba_run /// /// This is similar to print_tgba_run(), except that the run is /// actually replayed on the automaton while it is printed. Doing @@ -43,8 +44,6 @@ namespace spot /// \param debug if set the output will be more verbose and extra /// debugging informations will be output on failure /// \return true iff the run could be completed - /// - /// \ingroup tgba_run bool replay_tgba_run(std::ostream& os, const tgba* a, const tgba_run* run, bool debug = false); } diff --git a/src/tgbaalgos/rundotdec.hh b/src/tgbaalgos/rundotdec.hh index fb0237231..008d5bd71 100644 --- a/src/tgbaalgos/rundotdec.hh +++ b/src/tgbaalgos/rundotdec.hh @@ -31,6 +31,7 @@ namespace spot { /// \brief Highlight a spot::tgba_run on a spot::tgba. + /// \ingroup tgba_dotty /// /// An instance of this class can be passed to spot::dotty_reachable. class tgba_run_dotty_decorator: public dotty_decorator diff --git a/src/tgbaalgos/save.hh b/src/tgbaalgos/save.hh index 88483bec2..98b796063 100644 --- a/src/tgbaalgos/save.hh +++ b/src/tgbaalgos/save.hh @@ -28,6 +28,7 @@ namespace spot { /// \brief Save reachable states in text format. + /// \ingroup tgba_io std::ostream& tgba_save_reachable(std::ostream& os, const tgba* g); } diff --git a/src/tgbaalgos/stats.hh b/src/tgbaalgos/stats.hh index b5f7bc020..fada59667 100644 --- a/src/tgbaalgos/stats.hh +++ b/src/tgbaalgos/stats.hh @@ -26,6 +26,10 @@ namespace spot { + + /// \addtogroup tgba_misc + /// @{ + struct tgba_statistics { unsigned transitions; @@ -34,6 +38,8 @@ namespace spot /// \brief Compute statistics for an automata. tgba_statistics stats_reachable(const tgba* g); + + /// @} } #endif // SPOT_TGBAALGOS_STATS_HH diff --git a/src/tgbaparse/public.hh b/src/tgbaparse/public.hh index eb2379118..1dc63aed6 100644 --- a/src/tgbaparse/public.hh +++ b/src/tgbaparse/public.hh @@ -32,6 +32,9 @@ namespace spot { + /// \addtogroup tgba_io + /// @{ + /// \brief A parse diagnostic with its location. typedef std::pair tgba_parse_error; /// \brief A list of parser diagnostics, as filled by parse. @@ -67,6 +70,8 @@ namespace spot /// \return \c true iff any diagnostic was output. bool format_tgba_parse_errors(std::ostream& os, tgba_parse_error_list& error_list); + + /// @} } #endif // SPOT_TGBAPARSE_PUBLIC_HH