ta.hh 8.28 KB
 Alexandre Duret-Lutz committed Jul 29, 2013 1 // -*- coding: utf-8 -*-  Alexandre Duret-Lutz committed Mar 30, 2017 2 // Copyright (C) 2010, 2012-2017 Laboratoire de Recherche et  Alexandre Duret-Lutz committed Jul 29, 2013 3 // Developpement de l Epita (LRDE).  Ala Eddine committed Jul 15, 2012 4 5 6 7 8 // // 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 9 // the Free Software Foundation; either version 3 of the License, or  Ala Eddine committed Jul 15, 2012 10 11 12 13 14 15 16 17 // (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 18 // along with this program. If not, see .  Ala Eddine committed Jul 15, 2012 19   Etienne Renault committed Mar 23, 2015 20 #pragma once  Ala Eddine committed Jul 15, 2012 21 22 23 24  #include #include  Alexandre Duret-Lutz committed Dec 04, 2015 25 26 #include #include  Ala Eddine committed Jul 15, 2012 27 28 29  namespace spot {  Ala-Eddine Ben-Salem committed Aug 21, 2012 30   Ala Eddine committed Jul 15, 2012 31 32 33  // Forward declarations. See below. class ta_succ_iterator;  Ala-Eddine Ben-Salem committed Aug 21, 2012 34 35 36 37 38  /// \defgroup ta TA (Testing Automata) /// /// This type and its cousins are listed \ref ta_essentials "here". /// This is an abstract interface. Its implementations are \ref /// ta_representation "concrete representations". The  Alexandre Duret-Lutz committed Feb 02, 2016 39  /// algorithms that work on spot::ta are \ref ta_algorithms  Ala-Eddine Ben-Salem committed Aug 21, 2012 40 41 42 43 44 45  /// "listed separately". /// \addtogroup ta_essentials Essential TA types /// \ingroup ta /// \ingroup ta_essentials  Alexandre Duret-Lutz committed Jun 08, 2013 46  /// \brief A Testing Automaton.  Ala-Eddine Ben-Salem committed Aug 21, 2012 47 48 49  /// /// The Testing Automata (TA) were introduced by /// Henri Hansen, Wojciech Penczek and Antti Valmari  Ala-Eddine Ben-Salem committed Aug 21, 2012 50  /// in "Stuttering-insensitive automata for on-the-fly detection of livelock  Alexandre Duret-Lutz committed Jul 29, 2013 51  /// properties" In Proc. of FMICSÕ02, vol. 66(2) of Electronic Notes in  Ala-Eddine Ben-Salem committed Aug 21, 2012 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67  /// Theoretical Computer Science.Elsevier. /// /// While a TGBA automaton observes the value of the atomic propositions, the /// basic idea of TA is to detect the changes in these values; if a valuation /// does not change between two consecutive valuations of an execution, /// the TA stay in the same state. A TA transition \c (s,k,d) is labeled by a /// "changeset" \c k: i.e. the set of atomic propositions that change between /// states \c s and \c d, if the changeset is empty then the transition is /// called stuttering transition. /// To detect execution that ends by stuttering in the same TA state, a /// new kind of acceptance states is introduced: "livelock-acceptance states" /// (in addition to the standard Buchi-acceptance states). /// /// Browsing such automaton can be achieved using two functions: /// \c get_initial_states_set or \c get_artificial_initial_state, and \c /// succ_iter. The former returns the initial state(s) while the latter lists  Ala-Eddine Ben-Salem committed Aug 21, 2012 68  /// the successor states of any state (filtred by "changeset").  Ala-Eddine Ben-Salem committed Aug 21, 2012 69 70 71 72 73 74  /// /// 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 75  class SPOT_API ta  Ala Eddine committed Jul 15, 2012 76  {  Alexandre Duret-Lutz committed Oct 06, 2014 77 78  protected: acc_cond acc_;  Alexandre Duret-Lutz committed Feb 04, 2015 79  bdd_dict_ptr dict_;  Ala Eddine committed Jul 15, 2012 80 81  public:  Alexandre Duret-Lutz committed Oct 06, 2014 82  ta(const bdd_dict_ptr& d)  Alexandre Duret-Lutz committed Feb 04, 2015 83  : dict_(d)  Alexandre Duret-Lutz committed Oct 06, 2014 84 85 86  { }  Ala Eddine committed Jul 15, 2012 87 88 89 90 91 92  virtual ~ta() { } typedef std::set states_set_t;  Alexandre Duret-Lutz committed Nov 28, 2015 93  typedef std::set const_states_set_t;  Ala Eddine committed Jul 15, 2012 94   Ala-Eddine Ben-Salem committed Aug 21, 2012 95  /// \brief Get the initial states set of the automaton.  Alexandre Duret-Lutz committed Nov 28, 2015 96  virtual const_states_set_t  Ala Eddine committed Jul 15, 2012 97  get_initial_states_set() const = 0;  Ala Eddine committed Jul 15, 2012 98   Ala-Eddine Ben-Salem committed Aug 21, 2012 99 100 101  /// \brief Get the artificial initial state set of the automaton. /// Return 0 if this artificial state is not implemented /// (in this case, use \c get_initial_states_set)  Alexandre Duret-Lutz committed Mar 30, 2017 102  /// The aim of adding this state is to have a unique initial state. This  Ala-Eddine Ben-Salem committed Aug 21, 2012 103 104 105  /// artificial initial state have one transition to each real initial state, /// and this transition is labeled by the corresponding initial condition. /// (For more details, see the paper cited above)  Alexandre Duret-Lutz committed Nov 28, 2015 106  virtual const spot::state*  Ala-Eddine Ben-Salem committed Aug 21, 2012 107 108  get_artificial_initial_state() const {  Alexandre Duret-Lutz committed Sep 26, 2015 109  return nullptr;  Ala-Eddine Ben-Salem committed Aug 21, 2012 110  }  Ala-Eddine Ben-Salem committed Jul 15, 2012 111   Ala-Eddine Ben-Salem committed Aug 21, 2012 112 113 114 115 116 117  /// \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. ///  Ala Eddine committed Jul 15, 2012 118  virtual ta_succ_iterator*  Ala-Eddine Ben-Salem committed Aug 21, 2012 119  succ_iter(const spot::state* state) const = 0;  Ala Eddine committed Jul 15, 2012 120   Ala-Eddine Ben-Salem committed Aug 21, 2012 121  /// \brief Get an iterator over the successors of \a state  Ala-Eddine Ben-Salem committed Aug 21, 2012 122  /// filtred by the changeset on transitions  Ala-Eddine Ben-Salem committed Aug 21, 2012 123 124 125 126 127  /// /// The iterator has been allocated with \c new. It is the /// responsability of the caller to \c delete it when no /// longer needed. ///  Ala Eddine committed Jul 15, 2012 128  virtual ta_succ_iterator*  Ala-Eddine Ben-Salem committed Aug 21, 2012 129  succ_iter(const spot::state* state, bdd changeset) const = 0;  Ala Eddine committed Jul 15, 2012 130   Ala-Eddine Ben-Salem committed Aug 21, 2012 131 132 133 134 135 136 137  /// \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 Oct 06, 2014 138 139 140  bdd_dict_ptr get_dict() const {  Alexandre Duret-Lutz committed Feb 04, 2015 141  return dict_;  Alexandre Duret-Lutz committed Oct 06, 2014 142  }  Ala Eddine committed Jul 15, 2012 143   Ala-Eddine Ben-Salem committed Aug 21, 2012 144 145 146 147  /// \brief Format the state as a string for printing. /// /// This formating is the responsability of the automata /// that owns the state.  Ala Eddine committed Jul 15, 2012 148  virtual std::string  Ala Eddine committed Jul 15, 2012 149  format_state(const spot::state* s) const = 0;  Ala Eddine committed Jul 15, 2012 150   Ala-Eddine Ben-Salem committed Aug 21, 2012 151  /// \brief Return true if \a s is a Buchi-accepting state, otherwise false  Ala Eddine committed Jul 15, 2012 152  virtual bool  Ala Eddine committed Jul 15, 2012 153  is_accepting_state(const spot::state* s) const = 0;  Ala Eddine committed Jul 15, 2012 154   Ala-Eddine Ben-Salem committed Aug 21, 2012 155 156  /// \brief Return true if \a s is a livelock-accepting state /// , otherwise false  Ala Eddine committed Jul 15, 2012 157  virtual bool  Ala Eddine committed Jul 15, 2012 158  is_livelock_accepting_state(const spot::state* s) const = 0;  Ala Eddine committed Jul 15, 2012 159   Ala-Eddine Ben-Salem committed Aug 21, 2012 160  /// \brief Return true if \a s is an initial state, otherwise false  Ala Eddine committed Jul 15, 2012 161  virtual bool  Ala Eddine committed Jul 15, 2012 162  is_initial_state(const spot::state* s) const = 0;  Ala Eddine committed Jul 15, 2012 163   Ala-Eddine Ben-Salem committed Aug 21, 2012 164 165  /// \brief Return a BDD condition that represents the valuation /// of atomic propositions in the state \a s  Ala Eddine committed Jul 15, 2012 166  virtual bdd  Ala Eddine committed Jul 15, 2012 167 168  get_state_condition(const spot::state* s) const = 0;  Ala-Eddine Ben-Salem committed Aug 21, 2012 169  /// \brief Release a state \a s  Ala Eddine committed Jul 15, 2012 170 171  virtual void free_state(const spot::state* s) const = 0;  Ala Eddine committed Jul 15, 2012 172   Alexandre Duret-Lutz committed Oct 06, 2014 173 174 175 176 177 178 179 180 181 182  const acc_cond& acc() const { return acc_; } acc_cond& acc() { return acc_; }  Ala-Eddine Ben-Salem committed Jul 15, 2012 183   Ala Eddine committed Jul 15, 2012 184 185  };  Alexandre Duret-Lutz committed Aug 15, 2014 186 187 188  typedef std::shared_ptr ta_ptr; typedef std::shared_ptr const_ta_ptr;  Ala-Eddine Ben-Salem committed Aug 21, 2012 189  /// \ingroup ta_essentials  Alexandre Duret-Lutz committed Jun 08, 2013 190  /// \brief Iterate over the successors of a state.  Ala-Eddine Ben-Salem committed Aug 21, 2012 191 192 193 194 195 196  /// /// This class provides the basic functionalities required to /// iterate over the successors of a state, as well as querying /// transition labels. Because transitions are never explicitely /// encoded, labels (conditions and acceptance conditions) can only /// be queried while iterating over the successors.  Alexandre Duret-Lutz committed Apr 22, 2015 197  class ta_succ_iterator : public twa_succ_iterator  Ala Eddine committed Jul 15, 2012 198 199 200 201 202 203 204 205  { public: virtual ~ta_succ_iterator() { } };  Alexandre Duret-Lutz committed Sep 04, 2012 206 #ifndef SWIG  Ala Eddine committed Jul 15, 2012 207  // A stack of Strongly-Connected Components  Ala Eddine committed Jul 15, 2012 208  class scc_stack_ta  Ala Eddine committed Jul 15, 2012 209 210 211 212 213  { public: struct connected_component { public:  Etienne Renault committed Nov 29, 2018 214  connected_component(int index = -1) noexcept;  Ala Eddine committed Jul 15, 2012 215 216 217 218 219 220  /// Index of the SCC. int index; bool is_accepting;  Ala-Eddine Ben-Salem committed Jul 15, 2012 221 222  /// The bdd condition is the union of all acceptance conditions of /// transitions which connect the states of the connected component.  Alexandre Duret-Lutz committed Oct 06, 2014 223  acc_cond::mark_t condition;  Ala-Eddine Ben-Salem committed Jul 15, 2012 224   Alexandre Duret-Lutz committed Nov 28, 2015 225  std::list rem;  Ala Eddine committed Jul 15, 2012 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248  }; /// Stack a new SCC with index \a index. void push(int index); /// Access the top SCC. connected_component& top(); /// Access the top SCC. const connected_component& top() const; /// Pop the top SCC. void pop(); /// How many SCC are in stack. size_t size() const; /// The \c rem member of the top SCC.  Alexandre Duret-Lutz committed Nov 28, 2015 249  std::list&  Ala Eddine committed Jul 15, 2012 250 251 252 253 254 255 256 257 258  rem(); /// Is the stack empty? bool empty() const; typedef std::list stack_type; stack_type s; };  Alexandre Duret-Lutz committed Sep 04, 2012 259 #endif // !SWIG  Ala Eddine committed Jul 15, 2012 260   Ala-Eddine Ben-Salem committed Aug 21, 2012 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 /// \addtogroup ta_representation TA representations /// \ingroup ta /// \addtogroup ta_algorithms TA algorithms /// \ingroup ta /// \addtogroup ta_io Input/Output of TA /// \ingroup ta_algorithms /// \addtogroup tgba_ta Transforming TGBA into TA /// \ingroup ta_algorithms /// \addtogroup ta_generic Algorithm patterns /// \ingroup ta_algorithms /// \addtogroup ta_reduction TA simplifications /// \ingroup ta_algorithms /// \addtogroup ta_misc Miscellaneous algorithms on TA /// \ingroup ta_algorithms  Ala Eddine committed Jul 15, 2012 282 }