From 2cd298e4b0e852c0d898b20c4162e4a9a3986c42 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 16 Nov 2004 23:47:50 +0000 Subject: [PATCH] * src/tgba/bdddict.hh, src/tgba/state.hh, src/tgba/statebdd.hh, src/tgba/succiter.hh, src/tgba/succiterconcrete.hh, src/tgba/tgba.hh, src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbaexplicit.hh, src/tgba/tgbaproduct.hh, src/tgba/tgbareduc.hh, src/tgba/tgbatba.hh, src/tgbaalgos/emptiness.hh, src/tgbaalgos/magic.hh, src/tgbaalgos/replayrun.hh, src/tgbaalgos/gtec/gtec.hh, iface/gspn/ssp.hh: Introduce Doxygen groups in the documentation. Presently this only covers the tgba/ directory, and the emptiness-check algorithms. * doc/Doxyfile.in (EXCLUDE_PATTERNS): Skip Bison-generated files in src/evtgbaparse/. --- ChangeLog | 15 ++++ doc/Doxyfile.in | 6 +- iface/gspn/ssp.hh | 4 ++ src/tgba/bdddict.hh | 1 + src/tgba/state.hh | 4 ++ src/tgba/statebdd.hh | 3 +- src/tgba/succiter.hh | 5 +- src/tgba/succiterconcrete.hh | 3 +- src/tgba/tgba.hh | 22 ++++++ src/tgba/tgbabddconcrete.hh | 4 +- src/tgba/tgbabddconcreteproduct.hh | 9 +-- src/tgba/tgbaexplicit.hh | 3 + src/tgba/tgbaproduct.hh | 1 + src/tgba/tgbareduc.hh | 6 +- src/tgba/tgbatba.hh | 2 + src/tgbaalgos/emptiness.hh | 111 ++++++++++++++++++++--------- src/tgbaalgos/gtec/gtec.hh | 4 ++ src/tgbaalgos/magic.hh | 47 ++++++------ src/tgbaalgos/replayrun.hh | 2 + 19 files changed, 182 insertions(+), 70 deletions(-) diff --git a/ChangeLog b/ChangeLog index bea4e50e4..92c36e4f6 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,18 @@ +2004-11-17 Alexandre Duret-Lutz + + * src/tgba/bdddict.hh, src/tgba/state.hh, src/tgba/statebdd.hh, + src/tgba/succiter.hh, src/tgba/succiterconcrete.hh, + src/tgba/tgba.hh, src/tgba/tgbabddconcrete.hh, + src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbaexplicit.hh, + src/tgba/tgbaproduct.hh, src/tgba/tgbareduc.hh, + src/tgba/tgbatba.hh, src/tgbaalgos/emptiness.hh, + src/tgbaalgos/magic.hh, src/tgbaalgos/replayrun.hh, + src/tgbaalgos/gtec/gtec.hh, iface/gspn/ssp.hh: Introduce Doxygen + groups in the documentation. Presently this only covers the + tgba/ directory, and the emptiness-check algorithms. + * doc/Doxyfile.in (EXCLUDE_PATTERNS): Skip Bison-generated files + in src/evtgbaparse/. + 2004-11-16 Alexandre Duret-Lutz * src/tgba/tgbatba.hh (tgba_sba_proxy): New class, with the diff --git a/doc/Doxyfile.in b/doc/Doxyfile.in index 755f9ddf3..4a50e3e65 100644 --- a/doc/Doxyfile.in +++ b/doc/Doxyfile.in @@ -461,9 +461,9 @@ EXCLUDE_SYMLINKS = NO # EXCLUDE_PATTERNS tag to specify one or more wildcard patterns to exclude # certain files from those directories. -EXCLUDE_PATTERNS = */tgbaparse/location.hh \ - */tgbaparse/stack.hh \ - */tgbaparse/position.hh \ +EXCLUDE_PATTERNS = */*tgbaparse/location.hh \ + */*tgbaparse/stack.hh \ + */*tgbaparse/position.hh \ */*parse/*parse*.hh \ *test/* diff --git a/iface/gspn/ssp.hh b/iface/gspn/ssp.hh index ff6b6f731..3973cc0e1 100644 --- a/iface/gspn/ssp.hh +++ b/iface/gspn/ssp.hh @@ -48,12 +48,16 @@ namespace spot const ltl::declarative_environment& env_; }; + /// \defgroup emptiness_check_ssp Emptiness-check algorithms for SSP + /// \ingroup emptiness_check + /// @{ couvreur99_check* couvreur99_check_ssp_semi(const tgba* ssp_automata); couvreur99_check* couvreur99_check_ssp_shy_semi(const tgba* ssp_automata); couvreur99_check* couvreur99_check_ssp_shy(const tgba* ssp_automata); couvreur99_check_result* counter_example_ssp(const couvreur99_check_status* status); + /// @} } #endif // SPOT_IFACE_GSPN_SSP_GSPN_SSP_HH diff --git a/src/tgba/bdddict.hh b/src/tgba/bdddict.hh index 26332a9de..01ca7b891 100644 --- a/src/tgba/bdddict.hh +++ b/src/tgba/bdddict.hh @@ -34,6 +34,7 @@ namespace spot { /// Map BDD variables to formulae. + /// \ingroup tgba_essentials class bdd_dict: public bdd_allocator { public: diff --git a/src/tgba/state.hh b/src/tgba/state.hh index d5af79424..49bf5b068 100644 --- a/src/tgba/state.hh +++ b/src/tgba/state.hh @@ -31,6 +31,7 @@ namespace spot { /// \brief Abstract class for states. + /// \ingroup tgba_essentials class state { public: @@ -76,6 +77,7 @@ namespace spot }; /// \brief Strict Weak Ordering for \c state*. + /// \ingroup tgba_essentials /// /// This is meant to be used as a comparison functor for /// STL \c map whose key are of type \c state*. @@ -98,6 +100,7 @@ namespace spot }; /// \brief An Equivalence Relation for \c state*. + /// \ingroup tgba_essentials /// /// This is meant to be used as a comparison functor for /// Sgi \c hash_map whose key are of type \c state*. @@ -121,6 +124,7 @@ namespace spot }; /// \brief Hash Function for \c state*. + /// \ingroup tgba_essentials /// /// This is meant to be used as a hash functor for /// Sgi's \c hash_map whose key are of type \c state*. diff --git a/src/tgba/statebdd.hh b/src/tgba/statebdd.hh index af7440c1b..c045af996 100644 --- a/src/tgba/statebdd.hh +++ b/src/tgba/statebdd.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. // @@ -28,6 +28,7 @@ namespace spot { /// A state whose representation is a BDD. + /// \ingroup tgba_representation class state_bdd: public state { public: diff --git a/src/tgba/succiter.hh b/src/tgba/succiter.hh index 1fe286159..fe7a49239 100644 --- a/src/tgba/succiter.hh +++ b/src/tgba/succiter.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,8 +26,8 @@ namespace spot { - /// \brief Iterate over the successors of a state. + /// \ingroup tgba_essentials /// /// This class provides the basic functionalities required to /// iterate over the successors of a state, as well as querying @@ -96,7 +96,6 @@ namespace spot //@} }; - } diff --git a/src/tgba/succiterconcrete.hh b/src/tgba/succiterconcrete.hh index c68132cef..7e95e185a 100644 --- a/src/tgba/succiterconcrete.hh +++ b/src/tgba/succiterconcrete.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. // @@ -29,6 +29,7 @@ namespace spot { /// A concrete iterator over successors of a TGBA state. + /// \ingroup tgba_representation class tgba_succ_iterator_concrete: public tgba_succ_iterator { public: diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh index ddb9e78ef..b3391a582 100644 --- a/src/tgba/tgba.hh +++ b/src/tgba/tgba.hh @@ -28,7 +28,21 @@ namespace spot { + /// \defgroup tgba TGBA (Transition-based Genealized Büchi Automaton) + /// + /// Spot is centered around the spot::tgba type. This type and its + /// cousins are listed \ref tgba_essentials "here". This is an + /// abstract interface. Its implementations are either \ref + /// tgba_representation "concrete representations", or \ref + /// tgba_on_the_fly_algorithms "on-the-fly algorithms". Other + /// algorithms that work on spot::tgba are \ref tgba_algorithms + /// "listed separately". + + /// \addtogroup tgba_essentials Essential TGBA types + /// \ingroup tgba + /// \brief A Transition-based Generalized Büchi Automaton. + /// \ingroup tgba_essentials /// /// The acronym TGBA (Transition-based Generalized Büchi Automaton) /// was coined by Dimitra Giannakopoulou and Flavio Lerda @@ -201,6 +215,14 @@ namespace spot mutable int num_acc_; }; + /// \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 } #endif // SPOT_TGBA_TGBA_HH diff --git a/src/tgba/tgbabddconcrete.hh b/src/tgba/tgbabddconcrete.hh index ea64f6afb..fec3b72e4 100644 --- a/src/tgba/tgbabddconcrete.hh +++ b/src/tgba/tgbabddconcrete.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. // @@ -30,7 +30,7 @@ namespace spot { /// \brief A concrete spot::tgba implemented using BDDs. - /// + /// \ingroup tgba_representation class tgba_bdd_concrete: public tgba { public: diff --git a/src/tgba/tgbabddconcreteproduct.hh b/src/tgba/tgbabddconcreteproduct.hh index 512f8cbfa..8d22ec083 100644 --- a/src/tgba/tgbabddconcreteproduct.hh +++ b/src/tgba/tgbabddconcreteproduct.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,10 +26,11 @@ namespace spot { - /// \brief Multiplies two tgba::tgba_bdd_concrete automata. + /// \brief Multiplies two spot::tgba_bdd_concrete automata. + /// \ingroup tgba_algorithms /// - /// This function build the resulting product, as another - /// tgba::tgba_bdd_concrete automaton. + /// This function builds the resulting product as another + /// spot::tgba_bdd_concrete automaton. tgba_bdd_concrete* product(const tgba_bdd_concrete* left, const tgba_bdd_concrete* right); } diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index b87e6be60..ed55d141a 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -34,6 +34,7 @@ namespace spot class tgba_explicit_succ_iterator; /// Explicit representation of a spot::tgba. + /// \ingroup tgba_representation class tgba_explicit: public tgba { public: @@ -116,6 +117,7 @@ namespace spot /// States used by spot::tgba_explicit. + /// \ingroup tgba_representation class state_explicit : public spot::state { public: @@ -139,6 +141,7 @@ namespace spot /// Successor iterators used by spot::tgba_explicit. + /// \ingroup tgba_representation class tgba_explicit_succ_iterator: public tgba_succ_iterator { public: diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh index a24c3b2d6..182b325f2 100644 --- a/src/tgba/tgbaproduct.hh +++ b/src/tgba/tgbaproduct.hh @@ -29,6 +29,7 @@ namespace spot { /// \brief A state for spot::tgba_product. + /// \ingroup tgba_on_the_fly_algorithms /// /// This state is in fact a pair of state: the state from the left /// automaton and that of the right. diff --git a/src/tgba/tgbareduc.hh b/src/tgba/tgbareduc.hh index e27f424db..7992a5805 100644 --- a/src/tgba/tgbareduc.hh +++ b/src/tgba/tgbareduc.hh @@ -47,8 +47,10 @@ namespace spot }; - class tgba_reduc: public tgba_explicit, - public tgba_reachable_iterator_breadth_first + /// Explicit automata used in reductions. + /// \ingroup tgba_representation + class tgba_reduc: + public tgba_explicit, public tgba_reachable_iterator_breadth_first { public: tgba_reduc(const tgba* a, diff --git a/src/tgba/tgbatba.hh b/src/tgba/tgbatba.hh index cd3131569..3e6053f6f 100644 --- a/src/tgba/tgbatba.hh +++ b/src/tgba/tgbatba.hh @@ -30,6 +30,7 @@ namespace spot { /// \brief Degeneralize a spot::tgba on the fly, producing a TBA. + /// \ingroup tgba_on_the_fly_algorithms /// /// This class acts as a proxy in front of a spot::tgba, that should /// be degeneralized on the fly. The result is still a spot::tgba, @@ -87,6 +88,7 @@ namespace spot }; /// \brief Degeneralize a spot::tgba on the fly, producing an SBA. + /// \ingroup tgba_on_the_fly_algorithms /// /// This class acts as a proxy in front of a spot::tgba, that should /// be degeneralized on the fly. diff --git a/src/tgbaalgos/emptiness.hh b/src/tgbaalgos/emptiness.hh index 7dcdd4bd8..2e730de81 100644 --- a/src/tgbaalgos/emptiness.hh +++ b/src/tgbaalgos/emptiness.hh @@ -29,43 +29,41 @@ namespace spot { - - /// An accepted run, for a tgba. - struct tgba_run - { - struct step { - const state* s; - bdd label; - bdd acc; - }; - - typedef std::list steps; - - steps prefix; - steps cycle; - - ~tgba_run(); - tgba_run() - { - }; - tgba_run(const tgba_run& run); - tgba_run& operator=(const tgba_run& run); - }; - class tgba; + struct tgba_run; - /// \brief Display a tgba_run. + /// \addtogroup emptiness_check Emptiness-check + /// \ingroup tgba_algorithms /// - /// Output the prefix and cycle of the tgba_run \a run, even if it - /// does not corresponds to an actual run of the automaton \a a. - /// This is unlike replay_tgba_run(), which will ensure the run - /// actually exist in the automaton (and will display any transition - /// annotation). + /// All emptiness-check algorithms follow the same interface. + /// Basically once you have constructed an instance of + /// spot::emptiness_check (by instantiating a subclass, or calling a + /// functions construct such instance; see \ref + /// emptiness_check_algorithms "this list"), you should call + /// spot::emptiness_check::check() to check the automaton. /// - /// (\a a is used here only to format states and transitions.) - std::ostream& print_tgba_run(std::ostream& os, - const tgba* a, - const tgba_run* run); + /// If spot::emptiness_check::check() returns 0, then the automaton + /// was found empty. Otherwise the automaton accepts some run. + /// (Beware that some algorithms---those using bit-state + /// hashing---may found the automaton to be empty even if it is not + /// actually empty.) + /// + /// When spot::emptiness_check::check() does not return 0, it + /// returns an instance of spot::emptiness_check_result. You can + /// try to call spot::emptiness_check_result::accepting_run() to + /// obtain an accepting run. For some emptiness-check algorithms, + /// spot::emptiness_check_result::accepting_run() will require some + /// extra computation. Most emptiness-check algorithms are able to + /// return such an accepting run, however this is not mandatory and + /// spot::emptiness_check_result::accepting_run() can return 0 (this + /// does not means by anyway that no accepting run exist). + /// + /// The acceptance run returned by + /// spot::emptiness_check_result::accepting_run(), if any, is of + /// type spot::tgba_run. \ref tgba_run "This page" gathers existing + /// operations on these objects. + /// + /// @{ /// \brief The result of an emptiness check. /// @@ -112,6 +110,53 @@ namespace spot virtual std::ostream& print_stats(std::ostream& os) const; }; + /// @} + + /// \addtogroup emptiness_check_algorithms Emptiness-check algorithms + /// \ingroup emptiness_check + + + /// \addtogroup tgba_run TGBA runs and supporting functions + /// \ingroup emptiness_check + /// @{ + + /// An accepted run, for a tgba. + struct tgba_run + { + struct step { + const state* s; + bdd label; + bdd acc; + }; + + typedef std::list steps; + + steps prefix; + steps cycle; + + ~tgba_run(); + tgba_run() + { + }; + tgba_run(const tgba_run& run); + tgba_run& operator=(const tgba_run& run); + }; + + /// \brief Display a tgba_run. + /// + /// Output the prefix and cycle of the tgba_run \a run, even if it + /// does not corresponds to an actual run of the automaton \a a. + /// This is unlike replay_tgba_run(), which will ensure the run + /// actually exist in the automaton (and will display any transition + /// annotation). + /// + /// (\a a is used here only to format states and transitions.) + std::ostream& print_tgba_run(std::ostream& os, + const tgba* a, + const tgba_run* run); + /// @} + + } #endif // SPOT_TGBAALGOS_EMPTINESS_HH diff --git a/src/tgbaalgos/gtec/gtec.hh b/src/tgbaalgos/gtec/gtec.hh index f3fdbe720..fb0541fa2 100644 --- a/src/tgbaalgos/gtec/gtec.hh +++ b/src/tgbaalgos/gtec/gtec.hh @@ -27,6 +27,9 @@ namespace spot { + /// \addtogroup emptiness_check_algorithms + /// @{ + /// \brief Check whether the language of an automate is empty. /// /// This is based on the following paper. @@ -149,6 +152,7 @@ namespace spot virtual int* find_state(const state* s); }; + /// @} } #endif // SPOT_TGBAALGOS_GTEC_GTEC_HH diff --git a/src/tgbaalgos/magic.hh b/src/tgbaalgos/magic.hh index 40770bd10..8eb799dce 100644 --- a/src/tgbaalgos/magic.hh +++ b/src/tgbaalgos/magic.hh @@ -27,16 +27,20 @@ namespace spot { - /// \brief Returns an emptiness checker on the spot::tgba automaton \a a. - /// During the visit of \a a, the returned checker stores explicitely all + + /// \addtogroup emptiness_check_algorithms + /// @{ + + /// \brief Returns an emptiness checker on the spot::tgba automaton \a a. + /// During the visit of \a a, the returned checker stores explicitely all /// the traversed states. /// /// \pre The automaton \a a must have at most one accepting condition (i.e. /// it is a TBA). /// - /// The method \a check() of the returned checker can be called several times - /// (until it returns a null pointer) to enumerate all the visited accepting - /// paths. The implemented algorithm is the following. + /// The method \a check() of the returned checker can be called several times + /// (until it returns a null pointer) to enumerate all the visited accepting + /// paths. The implemented algorithm is the following. /// /// \verbatim /// procedure check () @@ -77,7 +81,7 @@ namespace spot /// /// \verbatim /// Article{ courcoubertis.92.fmsd, - /// author = {Costas Courcoubetis and Moshe Y. Vardi and Pierre + /// author = {Costas Courcoubetis and Moshe Y. Vardi and Pierre /// Wolper and Mihalis Yannakakis}, /// title = {Memory-Efficient Algorithm for the Verification of /// Temporal Properties}, @@ -90,7 +94,7 @@ namespace spot /// emptiness_check* explicit_magic_search(const tgba *a); - /// \brief Returns an emptiness checker on the spot::tgba automaton \a a. + /// \brief Returns an emptiness checker on the spot::tgba automaton \a a. /// During the visit of \a a, the returned checker does not store explicitely /// the traversed states but uses the bit state hashing technic. However, the /// implemented algorithm is the same as the one of @@ -103,24 +107,24 @@ namespace spot /// emptiness_check* bit_state_hashing_magic_search(const tgba *a, size_t size); - /// \brief Returns an emptiness check on the spot::tgba automaton \a a. - /// During the visit of \a a, the returned checker stores explicitely all + /// \brief Returns an emptiness check on the spot::tgba automaton \a a. + /// During the visit of \a a, the returned checker stores explicitely all /// the traversed states. /// /// \pre The automaton \a a must have at most one accepting condition (i.e. /// it is a TBA). - /// - /// The method \a check() of the returned checker can be called several times - /// (until it returns a null pointer) to enumerate all the visited accepting - /// paths. The implemented algorithm is the following: - /// + /// + /// The method \a check() of the returned checker can be called several times + /// (until it returns a null pointer) to enumerate all the visited accepting + /// paths. The implemented algorithm is the following: + /// /// \verbatim /// procedure check () /// begin /// weight = 0; /// call dfs_blue(s0); /// end; - /// + /// /// procedure dfs_blue (s) /// begin /// s.color = cyan; @@ -134,8 +138,8 @@ namespace spot /// if the edge (s,t) is accepting then /// weight = weight - 1; /// end if; - /// else if t.color == cyan and - /// (the edge (s,t) is accepting or + /// else if t.color == cyan and + /// (the edge (s,t) is accepting or /// weight > t.weight) then /// report cycle; /// end if; @@ -145,7 +149,7 @@ namespace spot /// end for; /// s.color = blue; /// end; - /// + /// /// procedure dfs_red(s) /// begin /// if s.color == cyan then @@ -159,8 +163,8 @@ namespace spot /// end for; /// end; /// \endverbatim - /// - /// It is an adaptation to TBA (and a slight extension) of the one + /// + /// It is an adaptation to TBA (and a slight extension) of the one /// presented in /// \verbatim /// InProceedings{ schwoon.05.tacas, @@ -183,7 +187,7 @@ namespace spot /// emptiness_check* explicit_se05_search(const tgba *a); - /// \brief Returns an emptiness checker on the spot::tgba automaton \a a. + /// \brief Returns an emptiness checker on the spot::tgba automaton \a a. /// During the visit of \a a, the returned checker does not store explicitely /// the traversed states but uses the bit state hashing technic. However, the /// implemented algorithm is the same as the one of @@ -196,6 +200,7 @@ namespace spot /// emptiness_check* bit_state_hashing_se05_search(const tgba *a, size_t size); + /// @} } #endif // SPOT_TGBAALGOS_MAGIC_HH diff --git a/src/tgbaalgos/replayrun.hh b/src/tgbaalgos/replayrun.hh index f8c375055..2c5fc9889 100644 --- a/src/tgbaalgos/replayrun.hh +++ b/src/tgbaalgos/replayrun.hh @@ -43,6 +43,8 @@ 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); }