tgba.hh 3.99 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

    /// \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;
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101

    /// \brief Return the set of all accepting conditions used
    /// by this automaton.
    ///
    /// The goal of the emptiness check is to ensure that
    /// a strongly connected component walks through each
    /// of these acceptiong conditions.  I.e., the union
    /// of the acceptiong conditions of all transition in
    /// the SCC should be equal to the result of this function.
    virtual bdd all_accepting_conditions() const = 0;

    /// \brief Return the conjuction of all negated accepting
    /// variables. 
    ///
    /// For instance if the automaton uses variables \c Acc[a],
    /// \c Acc[b] and \c Acc[c] to describe accepting sets,
    /// this function should return \c !Acc[a]\&!Acc[b]\&!Acc[c].
    ///
    /// This is useful when making products: each operand conditions
    /// set should be augmented with the neg_accepting_conditions() of
    /// the other operand.
    virtual bdd neg_accepting_conditions() const = 0;
102
  };
103
104

}
105
106

#endif // SPOT_TGBA_TGBA_HH