succiter.hh 2.26 KB
Newer Older
1
2
3
#ifndef SPOT_TGBA_SUCCITER_H
# define SPOT_TGBA_SUCCITER_H

4
#include "state.hh"
5
6
7
8

namespace spot
{

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.
16
17
18
  class tgba_succ_iterator
  {
  public:
19
20
    virtual
    ~tgba_succ_iterator()
21
22
    {
    }
23

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.
36
    virtual void first() = 0;
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.
42
    virtual void next() = 0;
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
54
    virtual bool done() = 0;
55

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.
68
    virtual state* current_state() = 0;
69
    /// \brief Get the condition on the transition leading to this successor.
70
    virtual bdd current_condition() = 0;
71
    /// \brief Get the promise on the transition leading to this successor.
72
    virtual bdd current_promise() = 0;
73
74

    //@}
75
76
77
78
79
80
  };

}


#endif // SPOT_TGBA_SUCCITER_H