succiter.hh 476 Bytes
Newer Older
1
2
3
#ifndef SPOT_TGBA_SUCCITER_H
# define SPOT_TGBA_SUCCITER_H

4
#include "state.hh"
5
6
7
8
9
10
11

namespace spot
{

  class tgba_succ_iterator
  {
  public:
12
13
    virtual
    ~tgba_succ_iterator()
14
15
    {
    }
16

17
18
19
20
    // iteration
    virtual void first() = 0;
    virtual void next() = 0;
    virtual bool done() = 0;
21

22
    // inspection
23
    virtual state* current_state() = 0;
24
25
26
27
28
29
30
31
    virtual bdd current_condition() = 0;
    virtual bdd current_promise() = 0;
  };

}


#endif // SPOT_TGBA_SUCCITER_H