tgba.hh 3.7 KB
 Alexandre Duret-Lutz committed May 26, 2003 1 2 3 ``````#ifndef SPOT_TGBA_TGBA_HH # define SPOT_TGBA_TGBA_HH `````` Alexandre Duret-Lutz committed May 27, 2003 4 ``````#include "state.hh" `````` Alexandre Duret-Lutz committed May 26, 2003 5 6 7 8 9 ``````#include "succiter.hh" #include "tgbabdddict.hh" namespace spot { `````` Alexandre Duret-Lutz committed May 27, 2003 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 `````` /// \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. /// /// 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. `````` Alexandre Duret-Lutz committed May 26, 2003 32 33 34 35 36 37 38 39 `````` class tgba { public: virtual ~tgba() { } `````` Alexandre Duret-Lutz committed May 27, 2003 40 41 42 43 44 45 `````` /// \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; `````` Alexandre Duret-Lutz committed May 26, 2003 46 `````` `````` Alexandre Duret-Lutz committed May 27, 2003 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 `````` /// \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. `````` Alexandre Duret-Lutz committed May 26, 2003 67 `````` virtual const tgba_bdd_dict& get_dict() const = 0; `````` Alexandre Duret-Lutz committed May 27, 2003 68 69 70 71 72 73 `````` /// \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; `````` Alexandre Duret-Lutz committed Jun 23, 2003 74 75 76 77 78 79 80 81 82 83 84 85 `````` /// \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 `````` Alexandre Duret-Lutz committed Jun 26, 2003 86 `````` /// variables. `````` Alexandre Duret-Lutz committed Jun 23, 2003 87 `````` /// `````` Alexandre Duret-Lutz committed Jun 26, 2003 88 89 90 `````` /// For instance if the automaton uses variables Acc[a], /// Acc[b] and Acc[c] to describe accepting sets, /// this function should return !Acc[a]\&!Acc[b]\&!Acc[c]. `````` Alexandre Duret-Lutz committed Jun 23, 2003 91 92 93 94 95 `````` /// /// 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; `````` Alexandre Duret-Lutz committed May 28, 2003 96 `````` }; `````` Alexandre Duret-Lutz committed May 26, 2003 97 98 `````` } `````` Alexandre Duret-Lutz committed May 26, 2003 99 100 `````` #endif // SPOT_TGBA_TGBA_HH``````