tgba.hh 6.22 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 ``````#include "succiter.hh" `````` Alexandre Duret-Lutz committed Jul 14, 2003 6 ``````#include "bdddict.hh" `````` Alexandre Duret-Lutz committed May 26, 2003 7 8 9 `````` 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 `````` class tgba { `````` Alexandre Duret-Lutz committed Jul 17, 2003 34 35 36 `````` protected: tgba(); virtual ~tgba(); `````` Alexandre Duret-Lutz committed May 26, 2003 37 `````` `````` Alexandre Duret-Lutz committed Jul 17, 2003 38 `````` public: `````` Alexandre Duret-Lutz committed May 27, 2003 39 40 41 42 43 44 `````` /// \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 45 `````` `````` Alexandre Duret-Lutz committed Jul 17, 2003 46 `````` /// \brief Get an iterator over the successors of \a local_state. `````` Alexandre Duret-Lutz committed May 27, 2003 47 48 49 50 51 `````` /// /// The iterator has been allocated with \c new. It is the /// responsability of the caller to \c delete it when no /// longer needed. /// `````` Alexandre Duret-Lutz committed Jul 17, 2003 52 53 54 55 56 57 58 59 60 `````` /// During synchornized products, additional informations are /// passed about the entire product and its state. Recall that /// products can be nested, forming a tree of spot::tgba where /// most values are computed on demand. \a global_automaton /// designate the root spot::tgba, and \a global_state its /// state. This two objects can be used by succ_iter() to /// restrict the set of successors to compute. /// /// \param local_state The state whose successors are to be explored. `````` Alexandre Duret-Lutz committed May 27, 2003 61 62 63 64 `````` /// 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). `````` Alexandre Duret-Lutz committed Jul 17, 2003 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 `````` /// \param global_state In a product, the state of the global /// product automaton. Otherwise, 0. Like \a locale_state, /// \a global_state is not adopted by \c succ_iter. /// \param global_automaton In a product, the state of the global /// product automaton. Otherwise, 0. virtual tgba_succ_iterator* succ_iter(const state* local_state, const state* global_state = 0, const tgba* global_automaton = 0) const = 0; /// \brief Get a formula that must hold whatever successor is taken. /// /// \return A formula which must be verified for all successors /// of \a state. /// /// This can be as simple as \c bddtrue, or more completely /// the disjunction of the condition of all successors. This /// is used as an hint by \c succ_iter() to reduce the number /// of successor to compute in a product. /// /// Sub classes should implement compute_support_conditions(), /// this function is just a wrapper that will cache the /// last return value for efficiency. bdd support_conditions(const state* state) const; /// \brief Get the conjunctions of variables tested by /// the outgoing transitions of \a state. /// /// All variables tested by outgoing transitions must be /// returned. This is mandatory. /// /// This is used as an hint by some \c succ_iter() to reduce the /// number of successor to compute in a product. /// /// Sub classes should implement compute_support_variables(), /// this function is just a wrapper that will cache the /// last return value for efficiency. bdd support_variables(const state* state) const; `````` Alexandre Duret-Lutz committed May 27, 2003 103 104 105 106 107 108 109 110 `````` /// \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 Jul 14, 2003 111 `````` virtual bdd_dict* get_dict() const = 0; `````` Alexandre Duret-Lutz committed May 27, 2003 112 113 114 115 116 117 `````` /// \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 118 119 120 121 122 123 124 125 126 127 128 129 `````` /// \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 130 `````` /// variables. `````` Alexandre Duret-Lutz committed Jun 23, 2003 131 `````` /// `````` Alexandre Duret-Lutz committed Jun 26, 2003 132 133 134 `````` /// 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 135 `````` /// `````` Alexandre Duret-Lutz committed Jul 17, 2003 136 `````` /// This is useful when making products: each operand's condition `````` Alexandre Duret-Lutz committed Jun 23, 2003 137 138 139 `````` /// set should be augmented with the neg_accepting_conditions() of /// the other operand. virtual bdd neg_accepting_conditions() const = 0; `````` Alexandre Duret-Lutz committed Jul 17, 2003 140 141 142 143 144 145 146 147 148 149 150 `````` protected: /// Do the actual computation of tgba::support_conditions(). virtual bdd compute_support_conditions(const state* state) const = 0; /// Do the actual computation of tgba::support_variables(). virtual bdd compute_support_variables(const state* state) const = 0; private: mutable const state* last_support_conditions_input_; mutable bdd last_support_conditions_output_; mutable const state* last_support_variables_input_; mutable bdd last_support_variables_output_; `````` Alexandre Duret-Lutz committed May 28, 2003 151 `````` }; `````` Alexandre Duret-Lutz committed May 26, 2003 152 153 `````` } `````` Alexandre Duret-Lutz committed May 26, 2003 154 155 `````` #endif // SPOT_TGBA_TGBA_HH``````