tgba.hh 3.05 KB
Newer Older
1
2
3
#ifndef SPOT_TGBA_TGBA_HH
# define SPOT_TGBA_TGBA_HH

4
#include "state.hh"
5
6
7
8
9
#include "succiter.hh"
#include "tgbabdddict.hh"

namespace spot
{
10
11
12
13
14
15
16
17
18
19
20
21
22
  /// \brief A Transition-based Generalized Büchi Automaton.
  ///
  /// The acronym TGBA (Transition-based Generalized Büchi Automaton)
  /// was coined by Dimitra Giannakopoulou and Flavio Lerda
  /// in "From States to Transitions: Improving Translation of LTL
  /// Formulae to Büchi Automata".  (FORTE'02)
  ///
  /// TGBAs are transition-based, meanings their labels are put
  /// on arcs, not on nodes.  They use Generalized Büchi acceptance
  /// conditions: there are several accepting sets (of
  /// transitions), and a path can be accepted only if it traverse
  /// at least one transition of each set infinitely often.
  ///
23
24
25
26
27
28
  /// Actually we do not really encode accepting sets but their
  /// complement: promise sets.  Formulae such as 'a U b' and
  /// 'F b' make the promise to fulfil 'b' enventually.  A path can
  /// be accepted if for each promise it traverse infinitely often
  /// a transition that does not make this promise.
  ///
29
30
31
32
33
34
35
36
37
  /// Browsing such automaton can be achieved using two functions.
  /// \c get_init_state, and \c succ_iter.  The former returns
  /// the initial state while the latter allows to explore the
  /// successor states of any state.
  ///
  /// Note that although this is a transition-based automata,
  /// we never represent transitions!  Transition informations are
  /// obtained by querying the iterator over the successors of
  /// a state.
38
39
40
41
42
43
44
45
  class tgba
  {
  public:
    virtual
    ~tgba()
    {
    }

46
47
48
49
50
51
    /// \brief Get the initial state of the automaton.
    ///
    /// The state has been allocated with \c new.  It is the
    /// responsability of the caller to \c delete it when no
    /// longer needed.
    virtual state* get_init_state() const = 0;
52

53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
    /// \brief Get an iterator over the successors of \a state.
    ///
    /// The iterator has been allocated with \c new.  It is the
    /// responsability of the caller to \c delete it when no
    /// longer needed.
    ///
    /// \param state is the state whose successors are to be explored.
    /// This pointer is not adopted in any way by \c succ_iter, and
    /// it is still the caller's responsability to delete it when
    /// appropriate (this can be done during the lifetime of
    /// the iterator).
    virtual tgba_succ_iterator* succ_iter(const state* state) const = 0;

    /// \brief Get the dictionary associated to the automaton.
    ///
    /// State are represented as BDDs.  The dictionary allows
    /// to map BDD variables back to formulae, and vice versa.
    /// This is useful when dealing with several automata (which
    /// may use the same BDD variable for different formula),
    /// or simply when printing.
73
    virtual const tgba_bdd_dict& get_dict() const = 0;
74
75
76
77
78
79
80

    /// \brief Format the state as a string for printing.
    ///
    /// This formating is the responsability of the automata
    /// who owns the state.
    virtual std::string format_state(const state* state) const = 0;
  }; 
81
82

}
83
84

#endif // SPOT_TGBA_TGBA_HH