diff --git a/ChangeLog b/ChangeLog index 060df3f70..e21ac3f57 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,13 @@ 2003-05-27 Alexandre Duret-Lutz + * src/tgba/bddprint.cc, src/tgba/bddprint.hh, + src/tgba/dictunion.hh, src/tgba/ltl2tgba.cc, src/tgba/ltl2tgba.hh, + src/tgba/tgbabddconcretefactory.hh, + src/tgba/tgbabddconcreteproduct.cc, + src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddfactory.hh, + src/tgba/tgbabddtranslatefactory.hh, src/tgbaalgos/dotty.cc: + Add Doxygen comments. + * src/tgba/bddfactory.hh, src/tgba/statebdd.hh, src/tgba/succiterconcrete.hh, src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.hh: Add diff --git a/src/tgba/bddprint.cc b/src/tgba/bddprint.cc index e8397ded6..6ae64c719 100644 --- a/src/tgba/bddprint.cc +++ b/src/tgba/bddprint.cc @@ -4,9 +4,10 @@ namespace spot { - + /// Global dictionary used by print_handler() to lookup variables. const tgba_bdd_dict* dict; + /// Stream handler used by Buddy to display BDD variables. static void print_handler(std::ostream& o, int var) { diff --git a/src/tgba/bddprint.hh b/src/tgba/bddprint.hh index 5d4f1c1d0..0469b2b34 100644 --- a/src/tgba/bddprint.hh +++ b/src/tgba/bddprint.hh @@ -9,13 +9,29 @@ namespace spot { + /// \brief Print a BDD as a set. + /// \param os The output stream. + /// \param dict The dictionary to use, to lookup variables. + /// \param b The BDD to print. std::ostream& bdd_print_set(std::ostream& os, const tgba_bdd_dict& dict, bdd b); + /// \brief Format a BDD as a set. + /// \param dict The dictionary to use, to lookup variables. + /// \param b The BDD to print. + /// \return The BDD formated as a string. std::string bdd_format_set(const tgba_bdd_dict& dict, bdd b); + /// \brief Print a BDD as a diagram in dotty format. + /// \param os The output stream. + /// \param dict The dictionary to use, to lookup variables. + /// \param b The BDD to print. std::ostream& bdd_print_dot(std::ostream& os, const tgba_bdd_dict& dict, bdd b); + /// \brief Print a BDD as a table. + /// \param os The output stream. + /// \param dict The dictionary to use, to lookup variables. + /// \param b The BDD to print. std::ostream& bdd_print_table(std::ostream& os, const tgba_bdd_dict& dict, bdd b); diff --git a/src/tgba/dictunion.hh b/src/tgba/dictunion.hh index 159db3d2d..cc03d1f34 100644 --- a/src/tgba/dictunion.hh +++ b/src/tgba/dictunion.hh @@ -5,6 +5,7 @@ namespace spot { + /// Build the union of two dictionaries. tgba_bdd_dict tgba_bdd_dict_union(const tgba_bdd_dict& l, const tgba_bdd_dict& r); } diff --git a/src/tgba/ltl2tgba.cc b/src/tgba/ltl2tgba.cc index 9bd46371f..865a505ce 100644 --- a/src/tgba/ltl2tgba.cc +++ b/src/tgba/ltl2tgba.cc @@ -3,11 +3,15 @@ #include "tgbabddconcretefactory.hh" #include "ltl2tgba.hh" -// FIXME: Add ref to Couvreur's paper. namespace spot { using namespace ltl; + + /// \brief Recursively translate a formula into a BDD. + /// + /// The algorithm used here is adapted from Jean-Michel Couvreur's + /// Probataf tool. class ltl_trad_visitor: public const_visitor { public: @@ -171,7 +175,7 @@ namespace spot }; tgba_bdd_concrete - ltl_to_tgba(const formula* f) + ltl_to_tgba(const ltl::formula* f) { tgba_bdd_concrete_factory fact; ltl_trad_visitor v(fact); diff --git a/src/tgba/ltl2tgba.hh b/src/tgba/ltl2tgba.hh index b2c25c8de..56a154054 100644 --- a/src/tgba/ltl2tgba.hh +++ b/src/tgba/ltl2tgba.hh @@ -6,8 +6,8 @@ namespace spot { + /// Build a spot::tgba_bdd_concrete from an LTL formula. tgba_bdd_concrete ltl_to_tgba(const ltl::formula* f); } #endif // SPOT_TGBA_LTL2TGBA_HH - diff --git a/src/tgba/tgbabddconcretefactory.hh b/src/tgba/tgbabddconcretefactory.hh index a47458f62..02e6b8703 100644 --- a/src/tgba/tgbabddconcretefactory.hh +++ b/src/tgba/tgbabddconcretefactory.hh @@ -5,26 +5,53 @@ #include "bddfactory.hh" #include "tgbabddfactory.hh" -namespace spot +namespace spot { - + /// Helper class to build a spot::tgba_bdd_concrete object. class tgba_bdd_concrete_factory: public bdd_factory, public tgba_bdd_factory { public: virtual ~tgba_bdd_concrete_factory(); - - int create_state(const ltl::formula* f); + + /// Create a state variable for formula \a f. + /// + /// \param f The formula to create a state for. + /// \return The variable number for this state. + /// + /// The state is not created if it already exists. Instead its + /// existing variable number is returned. Variable numbers + /// can be turned into BDD using ithvar(). + int create_state(const ltl::formula* f); + + /// Create an atomic proposition variable for formula \a f. + /// + /// \param f The formula to create an aotmic proposition for. + /// \return The variable number for this state. + /// + /// The atomic proposition is not created if it already exists. + /// Instead its existing variable number is returned. Variable numbers + /// can be turned into BDD using ithvar(). int create_atomic_prop(const ltl::formula* f); + + /// Create a promise variable for formula \a f. + /// + /// \param f The formula to create a promise for. + /// \return The variable number for this state. + /// + /// The promise is not created if it already exists. Instead its + /// existing variable number is returned. Variable numbers + /// can be turned into BDD using ithvar(). int create_promise(const ltl::formula* f); - + const tgba_bdd_core_data& get_core_data() const; const tgba_bdd_dict& get_dict() const; - + + /// Add a new constraint to the relation. void add_relation(bdd new_rel); - + private: - tgba_bdd_core_data data_; - tgba_bdd_dict dict_; + tgba_bdd_core_data data_; ///< Core data for the new automata. + tgba_bdd_dict dict_; ///< Dictionary for the new automata. }; } diff --git a/src/tgba/tgbabddconcreteproduct.cc b/src/tgba/tgbabddconcreteproduct.cc index 1c08b1e43..135a6bdc9 100644 --- a/src/tgba/tgbabddconcreteproduct.cc +++ b/src/tgba/tgbabddconcreteproduct.cc @@ -4,6 +4,11 @@ namespace spot { + /// \brief Helper class for product(). + /// + /// As both automata are encoded using BDD, we just have + /// to homogenize the variable numbers before ANDing the + /// relations and initial states. class tgba_bdd_product_factory: public tgba_bdd_factory { public: @@ -11,36 +16,36 @@ namespace spot const tgba_bdd_concrete& right) : dict_(tgba_bdd_dict_union(left.get_dict(), right.get_dict())), - fact_left_(left, dict_), - fact_right_(right, dict_), - data_(fact_left_.get_core_data(), fact_right_.get_core_data()), - init_(fact_left_.get_init_state() & fact_right_.get_init_state()) + fact_left_(left, dict_), + fact_right_(right, dict_), + data_(fact_left_.get_core_data(), fact_right_.get_core_data()), + init_(fact_left_.get_init_state() & fact_right_.get_init_state()) { } - + virtual ~tgba_bdd_product_factory() { } - + const tgba_bdd_core_data& get_core_data() const { return data_; } - + const tgba_bdd_dict& get_dict() const { return dict_; } - + bdd get_init_state() const { return init_; } - + private: tgba_bdd_dict dict_; tgba_bdd_translate_factory fact_left_; @@ -48,11 +53,11 @@ namespace spot tgba_bdd_core_data data_; bdd init_; }; - + tgba_bdd_concrete product(const tgba_bdd_concrete& left, const tgba_bdd_concrete& right) { - + tgba_bdd_product_factory p(left, right); return tgba_bdd_concrete(p, p.get_init_state()); } diff --git a/src/tgba/tgbabddconcreteproduct.hh b/src/tgba/tgbabddconcreteproduct.hh index 1d8625c11..78eabf250 100644 --- a/src/tgba/tgbabddconcreteproduct.hh +++ b/src/tgba/tgbabddconcreteproduct.hh @@ -5,6 +5,10 @@ namespace spot { + /// \brief Multiplies two tgba::tgba_bdd_concrete automata. + /// + /// This function build the resulting product, as another + /// tgba::tgba_bdd_concrete automaton. tgba_bdd_concrete product(const tgba_bdd_concrete& left, const tgba_bdd_concrete& right); } diff --git a/src/tgba/tgbabddfactory.hh b/src/tgba/tgbabddfactory.hh index 69239f0d7..d6e260b6f 100644 --- a/src/tgba/tgbabddfactory.hh +++ b/src/tgba/tgbabddfactory.hh @@ -6,10 +6,16 @@ namespace spot { + /// \brief Abstract class for spot::tgba_bdd_concrete factories. + /// + /// A spot::tgba_bdd_concrete can be constructed from anything that + /// supplies core data and their associated dictionary. class tgba_bdd_factory { public: + /// Get the core data for the new automata. virtual const tgba_bdd_core_data& get_core_data() const = 0; + /// Get the dictionary for the new automata. virtual const tgba_bdd_dict& get_dict() const = 0; }; } diff --git a/src/tgba/tgbabddtranslatefactory.hh b/src/tgba/tgbabddtranslatefactory.hh index f47627223..d1b41eb47 100644 --- a/src/tgba/tgbabddtranslatefactory.hh +++ b/src/tgba/tgbabddtranslatefactory.hh @@ -6,28 +6,37 @@ namespace spot { - + + /// A spot::tgba_bdd_factory than renumber BDD variables. class tgba_bdd_translate_factory: public tgba_bdd_factory { public: + ///\brief Construct a spot::tgba_bdd_translate_factory + /// + /// \param from The Automata to copy. + /// \param to The dictionary of variable number to use. tgba_bdd_translate_factory(const tgba_bdd_concrete& from, const tgba_bdd_dict& to); virtual ~tgba_bdd_translate_factory(); - bddPair* compute_pairs(const tgba_bdd_dict& from); - const tgba_bdd_core_data& get_core_data() const; const tgba_bdd_dict& get_dict() const; - + + /// Get the new initial state. bdd get_init_state() const; - + + protected: + /// Compute renaming pairs. + bddPair* compute_pairs(const tgba_bdd_dict& from); + private: tgba_bdd_core_data data_; tgba_bdd_dict dict_; - bdd init_; + bdd init_; }; - + + /// Reorder the variables of an automata. tgba_bdd_concrete defrag(const tgba_bdd_concrete& a); } diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index 9db0d06b2..5dbcb2cb4 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -7,6 +7,7 @@ namespace spot { typedef std::map seen_map; + /// Output and record a state. static bool dotty_state(std::ostream& os, const tgba& g, state* st, seen_map& m, int& node) @@ -28,6 +29,7 @@ namespace spot return true; } + /// Process successors. static void dotty_rec(std::ostream& os, const tgba& g, state* st, seen_map& m, int father)