From 799ab143000f524be4144089957437caf87d087b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 28 Nov 2011 13:37:14 +0100 Subject: [PATCH] Fix some Doxygen errors. * src/kripke/kripkeexplicit.hh: Reindent, and fix some comments. --- ChangeLog | 7 ++ src/kripke/kripkeexplicit.hh | 214 +++++++++++++++++------------------ 2 files changed, 112 insertions(+), 109 deletions(-) diff --git a/ChangeLog b/ChangeLog index 7059f134d..8be0d2539 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2011-11-28 Alexandre Duret-Lutz + + Fix some Doxygen errors. + + * src/kripke/kripkeexplicit.hh: Reindent, and fix + some comments. + 2011-11-13 Alexandre Duret-Lutz Add more nodes when resizing BDD table. diff --git a/src/kripke/kripkeexplicit.hh b/src/kripke/kripkeexplicit.hh index 1d9aefc8f..ba33f1b6f 100644 --- a/src/kripke/kripkeexplicit.hh +++ b/src/kripke/kripkeexplicit.hh @@ -35,60 +35,60 @@ namespace spot /// \brief Concrete class for kripke states. class state_kripke : public state { - friend class kripke_explicit; - friend class kripke_explicit_succ_iterator; - private: - state_kripke(); + friend class kripke_explicit; + friend class kripke_explicit_succ_iterator; + private: + state_kripke(); - /// \brief Compare two states. - /// - /// This method returns an integer less than, equal to, or greater - /// than zero if \a this is found, respectively, to be less than, equal - /// to, or greater than \a other according to some implicit total order. - /// - /// For moment, this method only compare the adress on the heap of the - /// twice pointers. - virtual int compare (const state* other) const; + /// \brief Compare two states. + /// + /// This method returns an integer less than, equal to, or greater + /// than zero if \a this is found, respectively, to be less than, equal + /// to, or greater than \a other according to some implicit total order. + /// + /// For moment, this method only compare the adress on the heap of the + /// twice pointers. + virtual int compare (const state* other) const; - /// \brief Hash a state - /// - /// \FIXME For moment : Only there to can instantiate state_kripke. - virtual size_t hash() const; + /// \brief Hash a state + virtual size_t hash() const; - /// \brief Duplicate a state. - virtual state_kripke* clone() const; + /// \brief Duplicate a state. + virtual state_kripke* clone() const; - /// \brief Add a condition to the conditions already in the state. - /// \param f The condition to add. - void add_conditions(bdd f); + /// \brief Add a condition to the conditions already in the state. + /// \param f The condition to add. + void add_conditions(bdd f); - /// \brief Add a new successor in the list. - /// \param add_me The state to add. - void add_succ(state_kripke*); + /// \brief Add a new successor in the list. + /// \param succ The successor state to add. + void add_succ(state_kripke* succ); - virtual bdd - as_bdd() const - { - return bdd_; - } + virtual bdd + as_bdd() const + { + return bdd_; + } - /// \brief Release a state. - /// - virtual void destroy() const - { - } + /// \brief Release a state. + /// + virtual void + destroy() const + { + } - virtual ~state_kripke () - { - } + virtual + ~state_kripke () + { + } - //////////////////////////////// - // Management for succ_iterator + //////////////////////////////// + // Management for succ_iterator - const std::list& get_succ() const; + const std::list& get_succ() const; - bdd bdd_; - std::list succ_; + bdd bdd_; + std::list succ_; }; @@ -96,21 +96,20 @@ namespace spot /// \brief Implement iterator pattern on successor of a state_kripke. class kripke_explicit_succ_iterator : public kripke_succ_iterator { - public: - kripke_explicit_succ_iterator(const state_kripke*, - bdd); + public: + kripke_explicit_succ_iterator(const state_kripke*, bdd); - ~kripke_explicit_succ_iterator(); + ~kripke_explicit_succ_iterator(); - virtual void first(); - virtual void next(); - virtual bool done() const; + virtual void first(); + virtual void next(); + virtual bool done() const; - virtual state_kripke* current_state() const; + virtual state_kripke* current_state() const; private: - const state_kripke* s_; - std::list::const_iterator it_; + const state_kripke* s_; + std::list::const_iterator it_; }; @@ -118,77 +117,74 @@ namespace spot /// \brief Kripke Structure. class kripke_explicit : public kripke { - public: - kripke_explicit(bdd_dict*); - kripke_explicit(bdd_dict*, state_kripke*); - ~kripke_explicit(); + public: + kripke_explicit(bdd_dict*); + kripke_explicit(bdd_dict*, state_kripke*); + ~kripke_explicit(); - bdd_dict* get_dict() const; - state_kripke* get_init_state() const; + bdd_dict* get_dict() const; + state_kripke* get_init_state() const; - /// \brief Allow to get an iterator on the state we passed in parameter. - kripke_explicit_succ_iterator* succ_iter(const spot::state* local_state, - const spot::state* global_state = 0, - const tgba* global_automaton = 0) const; + /// \brief Allow to get an iterator on the state we passed in + /// parameter. + kripke_explicit_succ_iterator* + succ_iter(const spot::state* local_state, + const spot::state* global_state = 0, + const tgba* global_automaton = 0) const; - /// \function state_condition - /// \brief Get the condition on the state, designed by the adress, - /// or by his name. - bdd state_condition(const state* s) const; - bdd state_condition(const std::string) const; + /// \brief Get the condition on the state + bdd state_condition(const state* s) const; + /// \brief Get the condition on the state + bdd state_condition(const std::string) const; - /// \brief Return the name of the state. - std::string format_state(const state*) const; + /// \brief Return the name of the state. + std::string format_state(const state*) const; + /// \brief Create state, if it does not already exists. + /// + /// Used by the parser. + void add_state(std::string); - /// \brief Check if the state already exist, and create it if not. - /// used by the parser for more simplicity. - void add_state(std::string); + /// \brief Add a transition between two states. + void add_transition(std::string source, + std::string dest); - /// \function add_transition - /// \brief Add a transition between two state. - /// Allow to do this with the two adress, or just the source adress, - void add_transition(std::string source, - std::string dest); + /// \brief Add a BDD condition to the state + /// + /// \param add the condition. + /// \param on_me where add the condition. + void add_conditions(bdd add, + std::string on_me); - /// \function add_conditions - /// \brief Add a condition in bdd format to the state, - /// name by his name or his address. - /// \param add the condition. - /// \param on_me where add the condition. - void add_conditions(bdd add, - std::string on_me); + /// \brief Add a formula to the state corresponding to the name. + /// + /// \param f the formula to add. + /// \param on_me the state where to add. + void add_condition(const ltl::formula* f, + std::string on_me); - /// \brief Add a formula to the state corresponding to the name. - /// \param on_me The state where add. - /// \param f the formula to add. - void add_condition(const ltl::formula* f, - std::string on_me); + /// \brief Return map between states and their names. + const std::map& + sn_get() const; - const std::map& - sn_get() const; + private: + /// \brief Add a state in the two maps. + void add_state(std::string, state_kripke*); - private: - /// \brief Add a state in the two map. - void add_state(std::string, state_kripke*); + void add_conditions(bdd add, + state_kripke* on_me); - void add_conditions(bdd add, - state_kripke* on_me); + void add_transition(std::string source, + const state_kripke* dest); - /// or with the two name. - void add_transition(state_kripke* source, - const state_kripke* dest); - void add_transition(std::string source, - const state_kripke* dest); + void add_transition(state_kripke* source, + const state_kripke* dest); - - - - bdd_dict* dict_; - state_kripke* init_; - std::map ns_nodes_; - std::map sn_nodes_; + bdd_dict* dict_; + state_kripke* init_; + std::map ns_nodes_; + std::map sn_nodes_; }; } #endif /* !SPOT_KRIPKEEXPLICIT_HH_ */