succiter.hh 2.26 KB
Newer Older
 Alexandre Duret-Lutz committed May 26, 2003 1 2 3 ``````#ifndef SPOT_TGBA_SUCCITER_H # define SPOT_TGBA_SUCCITER_H `````` Alexandre Duret-Lutz committed May 27, 2003 4 ``````#include "state.hh" `````` Alexandre Duret-Lutz committed May 26, 2003 5 6 7 8 `````` namespace spot { `````` Alexandre Duret-Lutz committed May 27, 2003 9 10 11 12 13 14 15 `````` /// \brief Iterate over the successors of a state. /// /// This class provides the basic functionalities required to /// iterate over the successors of a state, as well as querying /// transition labels. Because transitions are never explicitely /// encoded, labels (conditions and promises) can only be queried /// while iterating over the successors. `````` Alexandre Duret-Lutz committed May 26, 2003 16 17 18 `````` class tgba_succ_iterator { public: `````` Alexandre Duret-Lutz committed May 27, 2003 19 20 `````` virtual ~tgba_succ_iterator() `````` Alexandre Duret-Lutz committed May 26, 2003 21 22 `````` { } `````` Alexandre Duret-Lutz committed May 27, 2003 23 `````` `````` Alexandre Duret-Lutz committed May 27, 2003 24 25 26 27 28 29 30 31 32 33 34 35 `````` /// \name Iteration //@{ /// \brief Position the iterator on the first successor (if any). /// /// This method can be called several times to make multiple /// passes over successors. /// /// \warning One should always call \c done() to /// ensure there is a successor, even after \c first(). A /// common trap is to assume that there is at least one /// successor: this is wrong. `````` Alexandre Duret-Lutz committed May 26, 2003 36 `````` virtual void first() = 0; `````` Alexandre Duret-Lutz committed May 27, 2003 37 38 39 40 41 `````` /// \brief Jump to the next successor (if any). /// /// \warning Again, one should always call \c done() to ensure /// there is a successor. `````` Alexandre Duret-Lutz committed May 26, 2003 42 `````` virtual void next() = 0; `````` Alexandre Duret-Lutz committed May 27, 2003 43 44 45 46 47 48 49 50 51 52 53 `````` /// \brief Check whether the iteration is finished. /// /// This function should be called after any call to \c first() /// or \c next() and before any enquiry about the current state. /// /// The usual way to do this is with a \c for loop. /// \code /// for (s->first(); !s->done(); s->next()) /// ... /// \endcode `````` Alexandre Duret-Lutz committed May 26, 2003 54 `````` virtual bool done() = 0; `````` Alexandre Duret-Lutz committed May 27, 2003 55 `````` `````` Alexandre Duret-Lutz committed May 27, 2003 56 57 58 59 60 61 62 63 64 65 66 67 `````` //@} /// \name Inspection //@{ /// \brief Get the state of the current successor. /// /// Note that the same state may occur at different points /// in the iteration. These actually correspond to the same /// destination. It just means there were several transitions, /// with different conditions or promises, leading to the /// same state. `````` Alexandre Duret-Lutz committed May 27, 2003 68 `````` virtual state* current_state() = 0; `````` Alexandre Duret-Lutz committed May 27, 2003 69 `````` /// \brief Get the condition on the transition leading to this successor. `````` Alexandre Duret-Lutz committed May 26, 2003 70 `````` virtual bdd current_condition() = 0; `````` Alexandre Duret-Lutz committed May 27, 2003 71 `````` /// \brief Get the promise on the transition leading to this successor. `````` Alexandre Duret-Lutz committed May 26, 2003 72 `````` virtual bdd current_promise() = 0; `````` Alexandre Duret-Lutz committed May 27, 2003 73 74 `````` //@} `````` Alexandre Duret-Lutz committed May 26, 2003 75 76 77 78 79 80 `````` }; } #endif // SPOT_TGBA_SUCCITER_H``````