tgba.hh 10 KB
 Alexandre Duret-Lutz committed Jun 09, 2013 1 2 // Copyright (C) 2009, 2011, 2013 Laboratoire de Recherche et // Développement de l'Epita (LRDE).  Guillaume Sadegh committed Jan 24, 2010 3 // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de  Alexandre Duret-Lutz committed May 28, 2009 4 5 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie.  Alexandre Duret-Lutz committed Nov 21, 2003 6 7 8 9 10 // // This file is part of Spot, a model checking library. // // Spot is free software; you can redistribute it and/or modify it // under the terms of the GNU General Public License as published by  Alexandre Duret-Lutz committed Oct 12, 2012 11 // the Free Software Foundation; either version 3 of the License, or  Alexandre Duret-Lutz committed Nov 21, 2003 12 13 14 15 16 17 18 19 // (at your option) any later version. // // Spot is distributed in the hope that it will be useful, but WITHOUT // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public // License for more details. // // You should have received a copy of the GNU General Public License  Alexandre Duret-Lutz committed Oct 12, 2012 20 // along with this program. If not, see .  Alexandre Duret-Lutz committed Nov 21, 2003 21   Alexandre Duret-Lutz committed May 26, 2003 22 23 24 #ifndef SPOT_TGBA_TGBA_HH # define SPOT_TGBA_TGBA_HH  Alexandre Duret-Lutz committed May 27, 2003 25 #include "state.hh"  Alexandre Duret-Lutz committed May 26, 2003 26 #include "succiter.hh"  Alexandre Duret-Lutz committed Jul 14, 2003 27 #include "bdddict.hh"  Alexandre Duret-Lutz committed May 26, 2003 28 29 30  namespace spot {  Alexandre Duret-Lutz committed Nov 17, 2004 31  /// \defgroup tgba TGBA (Transition-based Generalized Büchi Automata)  Alexandre Duret-Lutz committed Nov 16, 2004 32 33 34 35 36 37 38 39 40 41 42 43 44  /// /// Spot is centered around the spot::tgba type. This type and its /// cousins are listed \ref tgba_essentials "here". This is an /// abstract interface. Its implementations are either \ref /// tgba_representation "concrete representations", or \ref /// tgba_on_the_fly_algorithms "on-the-fly algorithms". Other /// algorithms that work on spot::tgba are \ref tgba_algorithms /// "listed separately". /// \addtogroup tgba_essentials Essential TGBA types /// \ingroup tgba /// \ingroup tgba_essentials  Alexandre Duret-Lutz committed Jun 08, 2013 45  /// \brief A Transition-based Generalized Büchi Automaton.  Alexandre Duret-Lutz committed May 27, 2003 46 47 48 49 50 51 52 53  /// /// 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  Alexandre Duret-Lutz committed Nov 28, 2003 54  /// conditions: there are several acceptance sets (of  Alexandre Duret-Lutz committed Feb 23, 2009 55  /// transitions), and a path can be accepted only if it traverses  Alexandre Duret-Lutz committed May 27, 2003 56 57  /// at least one transition of each set infinitely often. ///  Alexandre Duret-Lutz committed Feb 23, 2009 58  /// Browsing such automaton can be achieved using two functions:  Alexandre Duret-Lutz committed May 27, 2003 59  /// \c get_init_state, and \c succ_iter. The former returns  Alexandre Duret-Lutz committed Feb 23, 2009 60  /// the initial state while the latter lists the  Alexandre Duret-Lutz committed May 27, 2003 61 62 63 64 65 66  /// 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 Jul 29, 2013 67  class SPOT_API tgba  Alexandre Duret-Lutz committed May 26, 2003 68  {  Alexandre Duret-Lutz committed Jul 17, 2003 69 70  protected: tgba();  Alexandre Duret-Lutz committed May 26, 2003 71   Alexandre Duret-Lutz committed Jul 17, 2003 72  public:  Alexandre Duret-Lutz committed Jul 25, 2003 73 74  virtual ~tgba();  Alexandre Duret-Lutz committed May 27, 2003 75 76 77  /// \brief Get the initial state of the automaton. /// /// The state has been allocated with \c new. It is the  Alexandre Duret-Lutz committed Jan 27, 2011 78  /// responsability of the caller to \c destroy it when no  Alexandre Duret-Lutz committed May 27, 2003 79 80  /// longer needed. virtual state* get_init_state() const = 0;  Alexandre Duret-Lutz committed May 26, 2003 81   Alexandre Duret-Lutz committed Jul 17, 2003 82  /// \brief Get an iterator over the successors of \a local_state.  Alexandre Duret-Lutz committed May 27, 2003 83 84 85 86 87  /// /// 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 88 89 90 91 92 93 94 95 96  /// 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 97  /// This pointer is not adopted in any way by \c succ_iter, and  Alexandre Duret-Lutz committed Jan 27, 2011 98  /// it is still the caller's responsability to destroy it when  Alexandre Duret-Lutz committed May 27, 2003 99 100  /// appropriate (this can be done during the lifetime of /// the iterator).  Alexandre Duret-Lutz committed Jul 17, 2003 101 102 103  /// \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.  Alexandre Duret-Lutz committed Apr 20, 2004 104  /// \param global_automaton In a product, the global  Alexandre Duret-Lutz committed Jul 17, 2003 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138  /// 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 139 140 141  /// \brief Get the dictionary associated to the automaton. ///  Alexandre Duret-Lutz committed Jun 09, 2013 142 143 144 145 146  /// Atomic propositions and acceptance conditions 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 147  virtual bdd_dict* get_dict() const = 0;  Alexandre Duret-Lutz committed May 27, 2003 148 149 150 151  /// \brief Format the state as a string for printing. /// /// This formating is the responsability of the automata  Alexandre Duret-Lutz committed May 28, 2009 152  /// that owns the state.  Alexandre Duret-Lutz committed May 27, 2003 153  virtual std::string format_state(const state* state) const = 0;  Alexandre Duret-Lutz committed Jun 23, 2003 154   Alexandre Duret-Lutz committed Oct 29, 2004 155 156 157  /// \brief Return a possible annotation for the transition /// pointed to by the iterator. ///  Alexandre Duret-Lutz committed Nov 17, 2011 158 159 160 161 162  /// You may decide to use annotations when building a tgba class /// that represents the state space of a model, for instance to /// indicate how the tgba transitions relate to the original model /// (e.g. the annotation could be the name of a PetriNet /// transition, or the line number of some textual formalism).  Alexandre Duret-Lutz committed Oct 29, 2004 163  ///  Alexandre Duret-Lutz committed Nov 17, 2011 164 165 166 167 168 169 170  /// Implementing this method is optional; the default annotation /// is the empty string. /// /// This method is used for instance in dotty_reachable(), /// and replay_tgba_run(). /// /// \param t a non-done tgba_succ_iterator for this automaton  Alexandre Duret-Lutz committed Oct 29, 2004 171 172 173  virtual std::string transition_annotation(const tgba_succ_iterator* t) const;  Alexandre Duret-Lutz committed Nov 17, 2004 174  /// \brief Project a state on an automaton.  Alexandre Duret-Lutz committed Jul 30, 2003 175 176 177 178 179 180 181 182 183 184 185  /// /// This converts \a s, into that corresponding spot::state for \a /// t. This is useful when you have the state of a product, and /// want restrict this state to a specific automata occuring in /// the product. /// /// It goes without saying that \a s and \a t should be compatible /// (i.e., \a s is a state of \a t). /// /// \return 0 if the projection fails (\a s is unrelated to \a t), /// or a new \c state* (the projected state) that must be  Alexandre Duret-Lutz committed Jan 27, 2011 186  /// destroyed by the caller.  Alexandre Duret-Lutz committed Jul 30, 2003 187 188  virtual state* project_state(const state* s, const tgba* t) const;  Alexandre Duret-Lutz committed Nov 28, 2003 189  /// \brief Return the set of all acceptance conditions used  Alexandre Duret-Lutz committed Jun 23, 2003 190 191 192 193 194 195 196  /// 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.  Alexandre Duret-Lutz committed Nov 28, 2003 197  virtual bdd all_acceptance_conditions() const = 0;  Alexandre Duret-Lutz committed Jun 23, 2003 198   Alexandre Duret-Lutz committed Nov 04, 2004 199  /// The number of acceptance conditions.  Alexandre Duret-Lutz committed Feb 18, 2005 200  virtual unsigned int number_of_acceptance_conditions() const;  Alexandre Duret-Lutz committed Nov 04, 2004 201   Alexandre Duret-Lutz committed Nov 28, 2003 202  /// \brief Return the conjuction of all negated acceptance  Alexandre Duret-Lutz committed Jun 26, 2003 203  /// variables.  Alexandre Duret-Lutz committed Jun 23, 2003 204  ///  Alexandre Duret-Lutz committed Jun 26, 2003 205  /// For instance if the automaton uses variables Acc[a],  Alexandre Duret-Lutz committed Nov 28, 2003 206  /// Acc[b] and Acc[c] to describe acceptance sets,  Alexandre Duret-Lutz committed Jun 26, 2003 207  /// this function should return !Acc[a]\&!Acc[b]\&!Acc[c].  Alexandre Duret-Lutz committed Jun 23, 2003 208  ///  Alexandre Duret-Lutz committed Jul 17, 2003 209  /// This is useful when making products: each operand's condition  Alexandre Duret-Lutz committed Nov 28, 2003 210  /// set should be augmented with the neg_acceptance_conditions() of  Alexandre Duret-Lutz committed Jun 23, 2003 211  /// the other operand.  Alexandre Duret-Lutz committed Nov 28, 2003 212  virtual bdd neg_acceptance_conditions() const = 0;  Alexandre Duret-Lutz committed Jul 17, 2003 213 214 215 216 217 218  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;  Alexandre Duret-Lutz committed Mar 31, 2011 219  protected:  Alexandre Duret-Lutz committed Jul 17, 2003 220 221  mutable const state* last_support_conditions_input_; mutable const state* last_support_variables_input_;  Alexandre Duret-Lutz committed Mar 31, 2011 222 223  private: mutable bdd last_support_conditions_output_;  Alexandre Duret-Lutz committed Jul 17, 2003 224  mutable bdd last_support_variables_output_;  Alexandre Duret-Lutz committed Nov 04, 2004 225  mutable int num_acc_;  Alexandre Duret-Lutz committed May 28, 2003 226  };  Alexandre Duret-Lutz committed May 26, 2003 227   Alexandre Duret-Lutz committed Nov 16, 2004 228 229 230 231 232  /// \addtogroup tgba_representation TGBA representations /// \ingroup tgba /// \addtogroup tgba_algorithms TGBA algorithms /// \ingroup tgba  Alexandre Duret-Lutz committed Nov 17, 2004 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250  /// \addtogroup tgba_on_the_fly_algorithms TGBA on-the-fly algorithms /// \ingroup tgba_algorithms /// \addtogroup tgba_io Input/Output of TGBA /// \ingroup tgba_algorithms /// \addtogroup tgba_ltl Translating LTL formulae into TGBA /// \ingroup tgba_algorithms /// \addtogroup tgba_generic Algorithm patterns /// \ingroup tgba_algorithms /// \addtogroup tgba_reduction TGBA simplifications /// \ingroup tgba_algorithms /// \addtogroup tgba_misc Miscellaneous algorithms on TGBA /// \ingroup tgba_algorithms  Alexandre Duret-Lutz committed May 26, 2003 251 }  Alexandre Duret-Lutz committed May 26, 2003 252 253  #endif // SPOT_TGBA_TGBA_HH