twa.hh 42.8 KB
 Alexandre Duret-Lutz committed Feb 12, 2014 1 // -*- coding: utf-8 -*-  Alexandre Duret-Lutz committed Jan 13, 2016 2 3 // Copyright (C) 2009, 2011, 2013, 2014, 2015, 2016 Laboratoire de // Recherche et Développement de l'Epita (LRDE).  Guillaume Sadegh committed Jan 24, 2010 4 // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de  Alexandre Duret-Lutz committed Feb 12, 2014 5 6 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie.  Alexandre Duret-Lutz committed Nov 21, 2003 7 8 9 10 11 // // 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 12 // the Free Software Foundation; either version 3 of the License, or  Alexandre Duret-Lutz committed Nov 21, 2003 13 14 15 16 17 18 19 20 // (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 21 // along with this program. If not, see .  Alexandre Duret-Lutz committed Nov 21, 2003 22   Etienne Renault committed Mar 23, 2015 23 #pragma once  Alexandre Duret-Lutz committed May 26, 2003 24   Alexandre Duret-Lutz committed Jul 18, 2016 25 #include  Alexandre Duret-Lutz committed Dec 04, 2015 26 27 28 #include #include #include  Alexandre Duret-Lutz committed Aug 19, 2014 29 30 #include #include  Alexandre Duret-Lutz committed Oct 08, 2014 31 32 #include #include  Alexandre Duret-Lutz committed Jan 03, 2015 33 #include  Etienne Renault committed Sep 24, 2015 34 #include  Alexandre Duret-Lutz committed Dec 04, 2015 35 36 37 #include #include #include  Alexandre Duret-Lutz committed Jan 13, 2016 38 #include  Alexandre Duret-Lutz committed May 26, 2003 39 40 41  namespace spot {  Alexandre Duret-Lutz committed Apr 22, 2015 42  /// \ingroup twa_essentials  Alexandre Duret-Lutz committed Aug 19, 2014 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84  /// \brief Abstract class for states. class SPOT_API state { public: /// \brief Compares two states (that come from the same automaton). /// /// This method returns an integer less than, equal to, or greater /// than zero if \a this is found, respectively, to be less than, equal /// to, or greater than \a other according to some implicit total order. /// /// This method should not be called to compare states from /// different automata. /// /// \sa spot::state_ptr_less_than virtual int compare(const state* other) const = 0; /// \brief Hash a state. /// /// This method returns an integer that can be used as a /// hash value for this state. /// /// Note that the hash value is guaranteed to be unique for all /// equal states (in compare()'s sense) for only has long has one /// of these states exists. So it's OK to use a spot::state as a /// key in a \c hash_map because the mere use of the state as a /// key in the hash will ensure the state continues to exist. /// /// However if you create the state, get its hash key, delete the /// state, recreate the same state, and get its hash key, you may /// obtain two different hash keys if the same state were not /// already used elsewhere. In practice this weird situation can /// occur only when the state is BDD-encoded, because BDD numbers /// (used to build the hash value) can be reused for other /// formulas. That probably doesn't matter, since the hash value /// is meant to be used in a \c hash_map, but it had to be noted. virtual size_t hash() const = 0; /// Duplicate a state. virtual state* clone() const = 0; /// \brief Release a state. ///  Alexandre Duret-Lutz committed Apr 22, 2015 85  /// Methods from the tgba or twa_succ_iterator always return a  Alexandre Duret-Lutz committed Aug 19, 2014 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100  /// new state that you should deallocate with this function. /// Before Spot 0.7, you had to "delete" your state directly. /// Starting with Spot 0.7, you should update your code to use /// this function instead. destroy() usually call delete, except /// in subclasses that destroy() to allow better memory management /// (e.g., no memory allocation for explicit automata). virtual void destroy() const { delete this; } protected: /// \brief Destructor. /// /// Note that client code should call  Alexandre Duret-Lutz committed Feb 02, 2016 101 102 103  /// \code s->destroy(); \endcode /// instead of /// \code delete s; \endcode .  Alexandre Duret-Lutz committed Aug 19, 2014 104 105 106 107 108  virtual ~state() { } };  Alexandre Duret-Lutz committed Apr 22, 2015 109  /// \ingroup twa_essentials  Alexandre Duret-Lutz committed Aug 19, 2014 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130  /// \brief Strict Weak Ordering for \c state*. /// /// This is meant to be used as a comparison functor for /// STL \c map whose key are of type \c state*. /// /// For instance here is how one could declare /// a map of \c state*. /// \code /// // Remember how many times each state has been visited. /// std::map seen; /// \endcode struct state_ptr_less_than { bool operator()(const state* left, const state* right) const { assert(left); return left->compare(right) < 0; } };  Alexandre Duret-Lutz committed Apr 22, 2015 131  /// \ingroup twa_essentials  Alexandre Duret-Lutz committed Aug 19, 2014 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153  /// \brief An Equivalence Relation for \c state*. /// /// This is meant to be used as a comparison functor for /// an \c unordered_map whose key are of type \c state*. /// /// For instance here is how one could declare /// a map of \c state*. /// \code /// // Remember how many times each state has been visited. /// std::unordered_map seen; /// \endcode struct state_ptr_equal { bool operator()(const state* left, const state* right) const { assert(left); return 0 == left->compare(right); } };  Alexandre Duret-Lutz committed Apr 22, 2015 154  /// \ingroup twa_essentials  Alexandre Duret-Lutz committed Aug 19, 2014 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177  /// \ingroup hash_funcs /// \brief Hash Function for \c state*. /// /// This is meant to be used as a hash functor for /// an \c unordered_map whose key are of type \c state*. /// /// For instance here is how one could declare /// a map of \c state*. /// \code /// // Remember how many times each state has been visited. /// std::unordered_map seen; /// \endcode struct state_ptr_hash { size_t operator()(const state* that) const { assert(that); return that->hash(); } };  Alexandre Duret-Lutz committed Jan 28, 2016 178 179 180 181 182  /// \brief Unordered set of abstract states /// /// Destroying each state if needed is the user's responsibility. /// /// \see state_unicity_table  Alexandre Duret-Lutz committed Aug 19, 2014 183  typedef std::unordered_set state_set;  Alexandre Duret-Lutz committed Aug 19, 2014 185   Alexandre Duret-Lutz committed Jan 28, 2016 186 187 188 189 190  /// \brief Unordered map of abstract states /// /// Destroying each state if needed is the user's responsibility. template using state_map = std::unordered_map;  Alexandre Duret-Lutz committed Aug 19, 2014 192   Alexandre Duret-Lutz committed Apr 22, 2015 193  /// \ingroup twa_essentials  Alexandre Duret-Lutz committed Aug 19, 2014 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211  /// \brief Render state pointers unique via a hash table. class SPOT_API state_unicity_table { state_set m; public: /// \brief Canonicalize state pointer. /// /// If this is the first time a state is seen, this return the /// state pointer as-is, otherwise it frees the state and returns /// a point to the previously seen copy. /// /// States are owned by the table and will be freed on /// destruction. const state* operator()(const state* s) { auto p = m.insert(s); if (!p.second)  Laurent XU committed Mar 10, 2016 212  s->destroy();  Alexandre Duret-Lutz committed Aug 19, 2014 213 214 215 216 217 218 219 220 221 222 223  return *p.first; } /// \brief Canonicalize state pointer. /// /// Same as operator(), except that a nullptr /// is returned if the state is not new. const state* is_new(const state* s) { auto p = m.insert(s); if (!p.second)  Laurent XU committed Mar 10, 2016 224 225 226 227  { s->destroy(); return nullptr; }  Alexandre Duret-Lutz committed Aug 19, 2014 228 229 230 231 232 233  return *p.first; } ~state_unicity_table() { for (state_set::iterator i = m.begin(); i != m.end();)  Laurent XU committed Mar 10, 2016 234 235 236 237 238 239  { // Advance the iterator before destroying its key. This // avoid issues with old g++ implementations. state_set::iterator old = i++; (*old)->destroy(); }  Alexandre Duret-Lutz committed Aug 19, 2014 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257  } size_t size() { return m.size(); } }; // Functions related to shared_ptr. ////////////////////////////////////////////////// typedef std::shared_ptr shared_state; inline void shared_state_deleter(state* s) { s->destroy(); }  Alexandre Duret-Lutz committed Apr 22, 2015 258  /// \ingroup twa_essentials  Alexandre Duret-Lutz committed Aug 19, 2014 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281  /// \brief Strict Weak Ordering for \c shared_state /// (shared_ptr). /// /// This is meant to be used as a comparison functor for /// STL \c map whose key are of type \c shared_state. /// /// For instance here is how one could declare /// a map of \c shared_state. /// \code /// // Remember how many times each state has been visited. /// std::map seen; /// \endcode struct state_shared_ptr_less_than { bool operator()(shared_state left, shared_state right) const { assert(left); return left->compare(right.get()) < 0; } };  Alexandre Duret-Lutz committed Apr 22, 2015 282  /// \ingroup twa_essentials  Alexandre Duret-Lutz committed Aug 19, 2014 283 284 285 286  /// \brief An Equivalence Relation for \c shared_state /// (shared_ptr). /// /// This is meant to be used as a comparison functor for  Alexandre Duret-Lutz committed Jan 28, 2016 287  /// an \c unordered_map whose key are of type \c shared_state.  Alexandre Duret-Lutz committed Aug 19, 2014 288 289 290 291 292 293 294 295 296  /// /// For instance here is how one could declare /// a map of \c shared_state /// \code /// // Remember how many times each state has been visited. /// std::unordered_map seen; /// \endcode  Alexandre Duret-Lutz committed Jan 28, 2016 297 298  /// /// \see shared_state_set  Alexandre Duret-Lutz committed Aug 19, 2014 299 300 301 302 303 304 305 306 307 308 309  struct state_shared_ptr_equal { bool operator()(shared_state left, shared_state right) const { assert(left); return 0 == left->compare(right.get()); } };  Alexandre Duret-Lutz committed Apr 22, 2015 310  /// \ingroup twa_essentials  Alexandre Duret-Lutz committed Aug 19, 2014 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325  /// \ingroup hash_funcs /// \brief Hash Function for \c shared_state (shared_ptr). /// /// This is meant to be used as a hash functor for /// an \c unordered_map whose key are of type /// \c shared_state. /// /// For instance here is how one could declare /// a map of \c shared_state. /// \code /// // Remember how many times each state has been visited. /// std::unordered_map seen; /// \endcode  Alexandre Duret-Lutz committed Jan 28, 2016 326 327  /// /// \see shared_state_set  Alexandre Duret-Lutz committed Aug 19, 2014 328 329 330 331 332 333 334 335 336 337  struct state_shared_ptr_hash { size_t operator()(shared_state that) const { assert(that); return that->hash(); } };  Alexandre Duret-Lutz committed Jan 28, 2016 338  /// Unordered set of shared states  Alexandre Duret-Lutz committed Aug 19, 2014 339  typedef std::unordered_set shared_state_set;  Alexandre Duret-Lutz committed Aug 19, 2014 342   Alexandre Duret-Lutz committed Apr 22, 2015 343  /// \ingroup twa_essentials  Alexandre Duret-Lutz committed Aug 19, 2014 344 345  /// \brief Iterate over the successors of a state. ///  Alexandre Duret-Lutz committed Feb 15, 2016 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390  /// This class provides the basic functionality required to iterate /// over the set of edges leaving a given state. Instance of /// twa_succ_iterator should normally not be created directly. /// Instead, they are created by passing a "source" state to /// twa::succ_iter(), which will create the instance of /// twa_succ_iterator to iterate over the successors of that state. /// /// This twa_succ_iterator class offers two types of services, /// offered by two groups of methods. The methods first(), next(), /// and done() allow iteration over the set of outgoing edges. /// The methods cond(), acc(), dst(), allow inspecting the current /// edge. /// /// The twa_succ_iterator is usually subclassed so that iteration /// methods and accessor methods can be implemented differently in /// different automata. In particular, this interface allows /// computing the set of successor on the fly if needed. /// /// The iterator can be used to iterate over all successors in a /// loop as follows: /// /// \code /// for (i->first(); !i->done(); i->next()) /// { /// // use i->cond(), i->acc(), i->dst() /// } /// \endcode /// /// If there are n successors, there will be 1 call to first(), n /// calls to next() and n+1 calls to done(), so a total of 2(n+1) /// calls to virtual methods just to handle the iteration. For this /// reason, we usually favor the following more efficient way of /// performing the same loop: /// /// \code /// if (i->first()) /// do /// { /// // use i->cond(), i->acc(), i->dst() /// } /// while(i->next()); /// \endcode /// /// This loops uses the return value of first() and next() to save /// n+1 calls to done().  Alexandre Duret-Lutz committed Apr 22, 2015 391  class SPOT_API twa_succ_iterator  Alexandre Duret-Lutz committed Aug 19, 2014 392 393 394  { public: virtual  Alexandre Duret-Lutz committed Apr 22, 2015 395  ~twa_succ_iterator()  Alexandre Duret-Lutz committed Aug 19, 2014 396 397 398 399  { } /// \name Iteration  Alexandre Duret-Lutz committed Feb 15, 2016 400  ///@{  Alexandre Duret-Lutz committed Aug 19, 2014 401 402 403  /// \brief Position the iterator on the first successor (if any). ///  Alexandre Duret-Lutz committed Feb 15, 2016 404 405  /// This method can be called several times in order to make /// multiple passes over successors.  Alexandre Duret-Lutz committed Aug 19, 2014 406 407 408 409 410 411  /// /// \warning One should always call \c done() (or better: check /// the return value of first()) to ensure there is a successor, /// even after \c first(). A common trap is to assume that there /// is at least one successor: this is wrong. ///  Alexandre Duret-Lutz committed Feb 15, 2016 412 413 414 415  /// \return true iff there is at least one successor /// /// If first() returns false, it is invalid to call next(), /// cond(), acc(), or dst().  Alexandre Duret-Lutz committed Aug 19, 2014 416 417 418 419 420 421 422  virtual bool first() = 0; /// \brief Jump to the next successor (if any). /// /// \warning Again, one should always call \c done() (or better: /// check the return value of next()) ensure there is a successor. ///  Alexandre Duret-Lutz committed Feb 15, 2016 423 424 425 426 427  /// \return true if the iterator moved to a new successor, false /// if the iterator could not move to a new successor. /// /// If next() returns false, it is invalid to call next() again, /// or to call cond(), acc() or dst().  Alexandre Duret-Lutz committed Aug 19, 2014 428 429 430 431 432 433 434  virtual bool next() = 0; /// \brief Check whether the iteration is finished. /// /// This function should be called after any call to \c first() /// or \c next() and before any enquiry about the current state. ///  Alexandre Duret-Lutz committed Feb 15, 2016 435  /// The typical use case of done() is in a \c for loop such as:  Alexandre Duret-Lutz committed Aug 19, 2014 436 437 438  /// /// for (s->first(); !s->done(); s->next()) /// ...  Alexandre Duret-Lutz committed Feb 15, 2016 439 440 441 442 443 444  /// /// \return false iff the iterator is pointing to a successor. /// /// It is incorrect to call done() if first() hasn't been called /// before. If done() returns true, it is invalid to call /// next(), cond(), acc(), or dst().  Alexandre Duret-Lutz committed Aug 19, 2014 445 446  virtual bool done() const = 0;  Alexandre Duret-Lutz committed Feb 15, 2016 447  ///@}  Alexandre Duret-Lutz committed Aug 19, 2014 448 449  /// \name Inspection  Alexandre Duret-Lutz committed Feb 15, 2016 450  ///@{  Alexandre Duret-Lutz committed Aug 19, 2014 451   Alexandre Duret-Lutz committed Feb 15, 2016 452  /// \brief Get the destination state of the current edge.  Alexandre Duret-Lutz committed Aug 19, 2014 453  ///  Alexandre Duret-Lutz committed Feb 15, 2016 454 455 456  /// Each call to dst() (even several times on the same edge) /// creates a new state that has to be destroyed (see /// state::destroy()). by the caller after it is no longer used.  Alexandre Duret-Lutz committed Aug 19, 2014 457  ///  Alexandre Duret-Lutz committed Feb 15, 2016 458 459 460  /// Note that the same state may occur at different points in the /// iteration, as different outgoing edges (usually with different /// labels or acceptance membership) may go to the same state.  Alexandre Duret-Lutz committed Nov 28, 2015 461  virtual const state* dst() const = 0;  Alexandre Duret-Lutz committed Feb 15, 2016 462  /// \brief Get the condition on the edge leading to this successor.  Alexandre Duret-Lutz committed Aug 19, 2014 463 464  /// /// This is a boolean function of atomic propositions.  Alexandre Duret-Lutz committed Oct 28, 2015 465  virtual bdd cond() const = 0;  Alexandre Duret-Lutz committed Feb 15, 2016 466 467  /// \brief Get the acceptance mark of the edge leading to this /// successor.  Alexandre Duret-Lutz committed Oct 28, 2015 468  virtual acc_cond::mark_t acc() const = 0;  Alexandre Duret-Lutz committed Aug 19, 2014 469   Alexandre Duret-Lutz committed Feb 15, 2016 470  ///@}  Alexandre Duret-Lutz committed Aug 19, 2014 471 472 473 474  }; namespace internal {  Alexandre Duret-Lutz committed Feb 02, 2016 475  /// \brief Helper structure to iterate over the successor of a  Alexandre Duret-Lutz committed Feb 15, 2016 476  /// state using the on-the-fly interface.  Alexandre Duret-Lutz committed Feb 02, 2016 477 478 479  /// /// This one emulates an STL-like iterator over the /// twa_succ_iterator interface.  Alexandre Duret-Lutz committed Aug 19, 2014 480 481 482  struct SPOT_API succ_iterator { protected:  Alexandre Duret-Lutz committed Apr 22, 2015 483  twa_succ_iterator* it_;  Alexandre Duret-Lutz committed Aug 19, 2014 484 485  public:  Alexandre Duret-Lutz committed Apr 22, 2015 486  succ_iterator(twa_succ_iterator* it):  Laurent XU committed Mar 10, 2016 487  it_(it)  Alexandre Duret-Lutz committed Aug 19, 2014 488 489 490 491 492  { } bool operator==(succ_iterator o) const {  Laurent XU committed Mar 10, 2016 493  return it_ == o.it_;  Alexandre Duret-Lutz committed Aug 19, 2014 494 495 496 497  } bool operator!=(succ_iterator o) const {  Laurent XU committed Mar 10, 2016 498  return it_ != o.it_;  Alexandre Duret-Lutz committed Aug 19, 2014 499 500  }  Alexandre Duret-Lutz committed Apr 22, 2015 501  const twa_succ_iterator* operator*() const  Alexandre Duret-Lutz committed Aug 19, 2014 502  {  Laurent XU committed Mar 10, 2016 503  return it_;  Alexandre Duret-Lutz committed Aug 19, 2014 504 505 506 507  } void operator++() {  Laurent XU committed Mar 10, 2016 508 509  if (!it_->next()) it_ = nullptr;  Alexandre Duret-Lutz committed Aug 19, 2014 510 511 512  } }; }  Alexandre Duret-Lutz committed Feb 12, 2014 513   Alexandre Duret-Lutz committed Apr 22, 2015 514  /// \defgroup twa TωA (Transition-based ω-Automata)  Alexandre Duret-Lutz committed Nov 16, 2004 515  ///  Alexandre Duret-Lutz committed Apr 22, 2015 516  /// Spot is centered around the spot::twa type. This type and its  Alexandre Duret-Lutz committed Feb 02, 2016 517  /// cousins are listed \ref twa_essentials "here". This is an  Alexandre Duret-Lutz committed Nov 16, 2004 518  /// abstract interface. Its implementations are either \ref  Alexandre Duret-Lutz committed Feb 02, 2016 519 520 521  /// twa_representation "concrete representations", or \ref /// twa_on_the_fly_algorithms "on-the-fly algorithms". Other /// algorithms that work on spot::twa are \ref twa_algorithms  Alexandre Duret-Lutz committed Nov 16, 2004 522 523  /// "listed separately".  Alexandre Duret-Lutz committed Apr 22, 2015 524  /// \addtogroup twa_essentials Essential TωA types  Alexandre Duret-Lutz committed Apr 22, 2015 525  /// \ingroup twa  Alexandre Duret-Lutz committed Nov 16, 2004 526   Alexandre Duret-Lutz committed Apr 22, 2015 527  /// \ingroup twa_essentials  Alexandre Duret-Lutz committed Apr 22, 2015 528  /// \brief A Transition-based ω-Automaton.  Alexandre Duret-Lutz committed May 27, 2003 529  ///  Alexandre Duret-Lutz committed Apr 22, 2015 530 531 532 533  /// The acronym TωA stands for Transition-based ω-automaton. /// We may write it as TwA or twa, but never as TWA as the /// w is just a non-utf8 replacement for ω that should not be /// capitalized.  Alexandre Duret-Lutz committed May 27, 2003 534  ///  Alexandre Duret-Lutz committed Feb 15, 2016 535 536 537 538 539 540  /// TωAs are transition-based automata, meanings that not-only do /// they have labels on edges, but they also have an acceptance /// condition defined in term of sets of transitions. The /// acceptance condition can be anything supported by the HOA format /// (http://adl.github.io/hoaf/). The only restriction w.r.t. the /// format is that this class does not support alternating automata.  Alexandre Duret-Lutz committed Apr 22, 2015 541  ///  Alexandre Duret-Lutz committed Feb 02, 2016 542  /// Previous versions of Spot supported a type of automata called  Alexandre Duret-Lutz committed Apr 22, 2015 543  /// TGBA, which are TωA in which the acceptance condition is a set  Alexandre Duret-Lutz committed Feb 15, 2016 544  /// of sets of transitions that must be visited infinitely often.  Alexandre Duret-Lutz committed Apr 22, 2015 545 546  /// /// In this version, TGBAs are now represented by TωAs for which  Alexandre Duret-Lutz committed May 27, 2003 547  ///  Alexandre Duret-Lutz committed Feb 15, 2016 548 549 550 551 552 553 554 555  /// aut->acc().is_generalized_buchi() /// /// returns true. /// /// Browsing a TωA is usually achieved using two methods: \c /// get_init_state(), and succ(). The former returns the initial /// state while the latter allows iterating over the outgoing edges /// of any given state.  Alexandre Duret-Lutz committed May 27, 2003 556  ///  Alexandre Duret-Lutz committed Apr 22, 2015 557  /// Note that although this is a transition-based automata, we never  Alexandre Duret-Lutz committed Feb 15, 2016 558  /// represent edges in the API. Information about edges can be  Alexandre Duret-Lutz committed Apr 22, 2015 559 560  /// obtained by querying the iterator over the successors of a /// state.  Alexandre Duret-Lutz committed Feb 15, 2016 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577  /// /// The interface presented here is what we call the on-the-fly /// interface of automata, because the TωA class can be subclassed /// to implement an object that computes its successors on-the-fly. /// The down-side is that all these methods are virtual, so you you /// pay the cost of virtual calls when iterating over automata /// constructed on-the-fly. Also the interface assumes that each /// successor state is a new object whose memory management is the /// responsibility of the caller, who should then call /// state::destroy() to release it. /// /// If you want to work with a TωA that is explicitly stored as a /// graph in memory, use the spot::twa_graph subclass instead. A /// twa_graph object can be used as a spot::twa (using the /// on-the-fly interface, even though nothing needs to be /// constructed), but it also offers a faster interface that do not /// use virtual methods.  Alexandre Duret-Lutz committed Apr 22, 2015 578  class SPOT_API twa: public std::enable_shared_from_this  Alexandre Duret-Lutz committed May 26, 2003 579  {  Alexandre Duret-Lutz committed Jul 17, 2003 580  protected:  Alexandre Duret-Lutz committed Apr 22, 2015 581  twa(const bdd_dict_ptr& d);  Alexandre Duret-Lutz committed Feb 02, 2016 582  /// Any iterator returned via release_iter.  Alexandre Duret-Lutz committed Apr 22, 2015 583  mutable twa_succ_iterator* iter_cache_;  Alexandre Duret-Lutz committed Feb 02, 2016 584  /// BDD dictionary used by the automaton.  Alexandre Duret-Lutz committed Feb 04, 2015 585  bdd_dict_ptr dict_;  Alexandre Duret-Lutz committed Jul 17, 2003 586  public:  Alexandre Duret-Lutz committed Feb 12, 2014 587 588  #ifndef SWIG  Alexandre Duret-Lutz committed Feb 02, 2016 589 590 591 592 593  /// \brief Helper class to iterate over the successor of a state /// using the on-the-fly interface /// /// This one emulates an STL-like container with begin()/end() /// methods so that it can be iterated using a ranged-for.  Alexandre Duret-Lutz committed Feb 12, 2014 594 595 596  class succ_iterable { protected:  Alexandre Duret-Lutz committed Apr 22, 2015 597  const twa* aut_;  Alexandre Duret-Lutz committed Apr 22, 2015 598  twa_succ_iterator* it_;  Alexandre Duret-Lutz committed Feb 12, 2014 599  public:  Alexandre Duret-Lutz committed Apr 22, 2015 600  succ_iterable(const twa* aut, twa_succ_iterator* it)  Laurent XU committed Mar 10, 2016 601  : aut_(aut), it_(it)  Alexandre Duret-Lutz committed Feb 12, 2014 602 603 604 605  { } succ_iterable(succ_iterable&& other)  Laurent XU committed Mar 10, 2016 606  : aut_(other.aut_), it_(other.it_)  Alexandre Duret-Lutz committed Feb 12, 2014 607  {  Laurent XU committed Mar 10, 2016 608  other.it_ = nullptr;  Alexandre Duret-Lutz committed Feb 12, 2014 609 610 611 612  } ~succ_iterable() {  Laurent XU committed Mar 10, 2016 613 614  if (it_) aut_->release_iter(it_);  Alexandre Duret-Lutz committed Feb 12, 2014 615 616 617 618  } internal::succ_iterator begin() {  Laurent XU committed Mar 10, 2016 619  return it_->first() ? it_ : nullptr;  Alexandre Duret-Lutz committed Feb 12, 2014 620 621 622 623  } internal::succ_iterator end() {  Laurent XU committed Mar 10, 2016 624  return nullptr;  Alexandre Duret-Lutz committed Feb 12, 2014 625 626 627 628  } }; #endif  Alexandre Duret-Lutz committed Apr 22, 2015 629  virtual ~twa();  Alexandre Duret-Lutz committed Jul 25, 2003 630   Alexandre Duret-Lutz committed May 27, 2003 631 632 633  /// \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 634  /// responsability of the caller to \c destroy it when no  Alexandre Duret-Lutz committed May 27, 2003 635  /// longer needed.  Alexandre Duret-Lutz committed Nov 28, 2015 636  virtual const state* get_init_state() const = 0;  Alexandre Duret-Lutz committed May 26, 2003 637   Alexandre Duret-Lutz committed Jul 17, 2003 638  /// \brief Get an iterator over the successors of \a local_state.  Alexandre Duret-Lutz committed May 27, 2003 639 640 641 642  /// /// 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 Feb 15, 2016 643 644  /// /// \see succ()  Alexandre Duret-Lutz committed Apr 22, 2015 645  virtual twa_succ_iterator*  Alexandre Duret-Lutz committed Feb 17, 2014 646  succ_iter(const state* local_state) const = 0;  Alexandre Duret-Lutz committed Feb 12, 2014 647   Alexandre Duret-Lutz committed Feb 12, 2014 648 #ifndef SWIG  Alexandre Duret-Lutz committed Feb 12, 2014 649 650 651  /// \brief Build an iterable over the successors of \a s. /// /// This is meant to be used as  Alexandre Duret-Lutz committed Feb 15, 2016 652 653 654 655 656 657 658 659 660 661  /// /// \code /// for (auto i: aut->succ(s)) /// { /// // use i->cond(), i->acc(), i->dst() /// } /// \endcode /// /// and the above loop is in fact syntactic sugar for ///  Alexandre Duret-Lutz committed Feb 02, 2016 662  /// \code  Alexandre Duret-Lutz committed Feb 15, 2016 663 664 665 666 667 668 669 670  /// twa_succ_iterator* i = aut->succ_iter(s); /// if (i->first()) /// do /// { /// // use i->cond(), i->acc(), i->dst() /// } /// while (i->next()); /// aut->release_iter(i);  Alexandre Duret-Lutz committed Feb 02, 2016 671  /// \endcode  Alexandre Duret-Lutz committed Feb 12, 2014 672  succ_iterable  Alexandre Duret-Lutz committed Feb 12, 2014 673 674 675 676  succ(const state* s) const { return {this, succ_iter(s)}; }  Alexandre Duret-Lutz committed Feb 12, 2014 677 678 679 680 681 682 #endif /// \brief Release an iterator after usage. /// /// This iterator can then be reused by succ_iter() to avoid /// memory allocation.  Alexandre Duret-Lutz committed Apr 22, 2015 683  void release_iter(twa_succ_iterator* i) const  Alexandre Duret-Lutz committed Feb 12, 2014 684 685  { if (iter_cache_)  Laurent XU committed Mar 10, 2016 686  delete i;  Alexandre Duret-Lutz committed Feb 12, 2014 687  else  Laurent XU committed Mar 10, 2016 688  iter_cache_ = i;  Alexandre Duret-Lutz committed Feb 12, 2014 689  }  Alexandre Duret-Lutz committed Jul 17, 2003 690   Alexandre Duret-Lutz committed May 27, 2003 691 692  /// \brief Get the dictionary associated to the automaton. ///  Alexandre Duret-Lutz committed Feb 15, 2016 693 694 695 696 697 698 699 700 701 702 703 704 705 706  /// Automata are labeled by Boolean formulas over atomic /// propositions. These Boolean formula are represented as BDDs. /// The dictionary allows to map BDD variables back to atomic /// propositions, and vice versa. /// /// Usually automata that are involved in the same computations /// should share their dictionaries so that operations between /// BDDs of the two automata work naturally. /// /// It is however possible to declare automata that use different /// sets of atomic propositions with different dictionaries. That /// way a BDD variable associated to some atomic proposition in /// one automaton might be reused for another atomic proposition /// in the other automaton.  Alexandre Duret-Lutz committed Oct 06, 2014 707 708  bdd_dict_ptr get_dict() const {  Alexandre Duret-Lutz committed Feb 04, 2015 709  return dict_;  Alexandre Duret-Lutz committed Oct 06, 2014 710  }  Alexandre Duret-Lutz committed May 27, 2003 711   Alexandre Duret-Lutz committed Feb 15, 2016 712 713 714 715 716 717 718 719 720  ///@{ /// \brief Register an atomic proposition designated by \a ap. /// /// This is the preferred way to declare that an automaton is using /// a given atomic proposition. /// /// This adds the atomic proposition to the list of atomic /// proposition of the automaton, and also register it to the /// bdd_dict.  Etienne Renault committed Sep 24, 2015 721  ///  Alexandre Duret-Lutz committed Feb 15, 2016 722 723  /// \return The BDD variable number assigned for this atomic /// proposition.  Alexandre Duret-Lutz committed Sep 28, 2015 724  int register_ap(formula ap)  Etienne Renault committed Sep 24, 2015 725  {  Alexandre Duret-Lutz committed Dec 24, 2015 726 727  int res = dict_->has_registered_proposition(ap, this); if (res < 0)  Laurent XU committed Mar 10, 2016 728 729 730 731 732  { aps_.push_back(ap); res = dict_->register_proposition(ap, this); bddaps_ &= bdd_ithvar(res); }  Etienne Renault committed Sep 24, 2015 733 734 735  return res; }  Alexandre Duret-Lutz committed Feb 15, 2016 736  int register_ap(std::string ap)  Etienne Renault committed Sep 24, 2015 737  {  Alexandre Duret-Lutz committed Feb 15, 2016 738  return register_ap(formula::ap(ap));  Etienne Renault committed Sep 24, 2015 739  }  Alexandre Duret-Lutz committed Feb 15, 2016 740  ///@}  Etienne Renault committed Sep 24, 2015 741   Alexandre Duret-Lutz committed May 01, 2016 742 743 744 745  /// \brief Unregister an atomic proposition. /// /// \param num the BDD variable number returned by register_ap(). void unregister_ap(int num);  Alexandre Duret-Lutz committed Apr 29, 2016 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773  /// \brief Register all atomic propositions that have /// already be register by the bdd_dict for this automaton. /// /// This method may only be called on an automaton with an empty /// list of AP. It will fetch all atomic proposition that have /// been set in the bdd_dict for this particular automaton. /// /// The typical use-case for this function is when the labels of /// an automaton are created by functions such as /// formula_to_bdd(). This is for instance done in the parser /// for never claims or LBTT. void register_aps_from_dict() { if (!aps_.empty()) throw std::runtime_error("register_ap_from_dict() may not be" " called on an automaton that has already" " registered some AP"); auto& m = get_dict()->bdd_map; unsigned s = m.size(); for (unsigned n = 0; n < s; ++n) if (m[n].refs.find(this) != m[n].refs.end()) { aps_.push_back(m[n].f); bddaps_ &= bdd_ithvar(n); } }  Alexandre Duret-Lutz committed Feb 15, 2016 774  /// \brief The vector of atomic propositions registered by this  Etienne Renault committed Sep 24, 2015 775  /// automaton.  Alexandre Duret-Lutz committed Mar 02, 2016 776  const std::vector& ap() const  Etienne Renault committed Sep 24, 2015 777 778 779 780  { return aps_; }  Alexandre Duret-Lutz committed Feb 15, 2016 781  /// \brief The set of atomic propositions as a conjunction.  Alexandre Duret-Lutz committed Mar 02, 2016 782  bdd ap_vars() const  Etienne Renault committed Sep 24, 2015 783 784 785 786  { return bddaps_; }  Alexandre Duret-Lutz committed May 27, 2003 787 788  /// \brief Format the state as a string for printing. ///  Alexandre Duret-Lutz committed Feb 15, 2016 789 790 791 792 793  /// Formating is the responsability of the automata that owns the /// state, so that state objects could be implemented as very /// small objects, maybe sharing data with other state objects via /// data structure stored in the automaton. virtual std::string format_state(const state* s) const = 0;  Alexandre Duret-Lutz committed Jun 23, 2003 794   Alexandre Duret-Lutz committed Nov 17, 2004 795  /// \brief Project a state on an automaton.  Alexandre Duret-Lutz committed Jul 30, 2003 796 797 798 799 800 801 802 803 804 805 806  /// /// 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 807  /// destroyed by the caller.  Alexandre Duret-Lutz committed Aug 15, 2014 808  virtual state* project_state(const state* s,  Laurent XU committed Mar 10, 2016 809  const const_twa_ptr& t) const;  Alexandre Duret-Lutz committed Jul 30, 2003 810   Alexandre Duret-Lutz committed Feb 15, 2016 811 812  ///@{ /// \brief The acceptance condition of the automaton.  Alexandre Duret-Lutz committed Oct 06, 2014 813 814 815 816  const acc_cond& acc() const { return acc_; }  Alexandre Duret-Lutz committed Nov 04, 2004 817   Alexandre Duret-Lutz committed Oct 06, 2014 818 819 820 821  acc_cond& acc() { return acc_; }  Alexandre Duret-Lutz committed Feb 15, 2016 822  ///@}  Alexandre Duret-Lutz committed Jul 17, 2003 823   Alexandre Duret-Lutz committed Feb 02, 2016 824  /// Check whether the language of the automaton is empty.  Alexandre Duret-Lutz committed Aug 23, 2014 825 826  virtual bool is_empty() const;  Alexandre Duret-Lutz committed Feb 02, 2016 827  private:  Alexandre Duret-Lutz committed Oct 06, 2014 828 829  acc_cond acc_;  Alexandre Duret-Lutz committed Mar 18, 2015 830 831 832  void set_num_sets_(unsigned num) { if (num < acc_.num_sets())  Laurent XU committed Mar 10, 2016 833 834 835 836  { acc_.~acc_cond(); new (&acc_) acc_cond; }  Alexandre Duret-Lutz committed Mar 18, 2015 837 838 839  acc_.add_sets(num - acc_.num_sets()); }  Alexandre Duret-Lutz committed Feb 23, 2015 840  public:  Alexandre Duret-Lutz committed Feb 02, 2016 841  /// Number of acceptance sets used by the automaton.  Alexandre Duret-Lutz committed Jun 11, 2015 842 843 844 845 846  unsigned num_sets() const { return acc_.num_sets(); }  Alexandre Duret-Lutz committed Feb 02, 2016 847  /// Acceptance formula used by the automaton.  Alexandre Duret-Lutz committed Feb 26, 2015 848  const acc_cond::acc_code& get_acceptance() const  Alexandre Duret-Lutz committed Feb 23, 2015 849 850 851  { return acc_.get_acceptance(); }  Alexandre Duret-Lutz committed Feb 23, 2015 852   Alexandre Duret-Lutz committed Feb 02, 2016 853 854 855 856  /// \brief Set the acceptance condition of the automaton. /// /// \param num the number of acceptance sets used /// \param c the acceptance formula  Alexandre Duret-Lutz committed Feb 23, 2015 857 858  void set_acceptance(unsigned num, const acc_cond::acc_code& c) {  Alexandre Duret-Lutz committed Mar 18, 2015 859  set_num_sets_(num);  Alexandre Duret-Lutz committed Feb 23, 2015 860 861  acc_.set_acceptance(c); if (num == 0)  Laurent XU committed Mar 10, 2016 862  prop_state_acc(true);  Alexandre Duret-Lutz committed Feb 23, 2015 863 864  }  Alexandre Duret-Lutz committed Feb 02, 2016 865  /// Copy the acceptance condition of another TωA.  Alexandre Duret-Lutz committed Apr 22, 2015 866  void copy_acceptance_of(const const_twa_ptr& a)  Alexandre Duret-Lutz committed Mar 18, 2015 867 868 869 870  { acc_ = a->acc(); unsigned num = acc_.num_sets(); if (num == 0)  Laurent XU committed Mar 10, 2016 871  prop_state_acc(true);  Alexandre Duret-Lutz committed Mar 18, 2015 872 873  }  Alexandre Duret-Lutz committed Feb 02, 2016 874  /// Copy the atomic propositions of another TωA  Alexandre Duret-Lutz committed Apr 22, 2015 875  void copy_ap_of(const const_twa_ptr& a)  Alexandre Duret-Lutz committed Mar 18, 2015 876  {  Alexandre Duret-Lutz committed Sep 26, 2015 877  for (auto f: a->ap())  Laurent XU committed Mar 10, 2016 878  this->register_ap(f);  Alexandre Duret-Lutz committed Mar 18, 2015 879 880  }  Alexandre Duret-Lutz committed Feb 02, 2016 881 882 883 884 885 886 887 888 889 890 891 892  /// \brief Set generalized Büchi acceptance /// /// \param num the number of acceptance sets to used /// /// The acceptance formula of the form /// \code /// Inf(0)&Inf(1)&...&Inf(num-1) /// \endcode /// is generated. /// /// In the case where \a num is null, the state-acceptance /// property is automatically turned on.  Alexandre Duret-Lutz committed Mar 18, 2015 893 894 895 896 897  void set_generalized_buchi(unsigned num) { set_num_sets_(num); acc_.set_generalized_buchi(); if (num == 0)  Laurent XU committed Mar 10, 2016 898  prop_state_acc(true);  Alexandre Duret-Lutz committed Mar 18, 2015 899 900  }  Alexandre Duret-Lutz committed Feb 02, 2016 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915  /// \brief Set Büchi acceptance. /// /// This declares a single acceptance set, and \c Inf(0) /// acceptance. The returned mark \c {0} can be used to tag /// accepting transition. /// /// Note that this does not make the automaton as using /// state-based acceptance. If you want to create a Büchi /// automaton with state-based acceptance, call /// \code /// prop_state_acc(true) /// \endcode /// in addition. /// /// \see prop_state_acc  Alexandre Duret-Lutz committed Mar 18, 2015 916 917 918 919 920 921  acc_cond::mark_t set_buchi() { set_generalized_buchi(1); return acc_.mark(0); }  Alexandre Duret-Lutz committed Mar 31, 2011 922  private:  Alexandre Duret-Lutz committed Sep 28, 2015 923  std::vector aps_;  Etienne Renault committed Sep 24, 2015 924  bdd bddaps_;  Alexandre Duret-Lutz committed Aug 15, 2014 925   Alexandre Duret-Lutz committed Feb 02, 2016 926  /// Helper structure used to store property flags.  Alexandre Duret-Lutz committed Aug 15, 2014 927 928  struct bprop {  Alexandre Duret-Lutz committed Jan 13, 2016 929 930  trival::repr_t state_based_acc:2; // State-based acceptance. trival::repr_t inherently_weak:2; // Inherently Weak automaton.  Laurent XU committed Mar 10, 2016 931 932  trival::repr_t weak:2; // Weak automaton. trival::repr_t terminal:2; // Terminal automaton.  Alexandre Duret-Lutz committed Jan 13, 2016 933 934 935  trival::repr_t deterministic:2; // Deterministic automaton. trival::repr_t unambiguous:2; // Unambiguous automaton. trival::repr_t stutter_invariant:2; // Stutter invariant language.  Alexandre Duret-Lutz committed Aug 15, 2014 936 937 938 939 940 941 942  }; union { unsigned props; bprop is; };  Alexandre Duret-Lutz committed Oct 08, 2014 943 944 945 #ifndef SWIG // Dynamic properties, are given with a name and a destructor function. std::unordered_map>> named_prop_;  Alexandre Duret-Lutz committed Oct 08, 2014 948 #endif  Alexandre Duret-Lutz committed Dec 09, 2014 949 950  void* get_named_prop_(std::string s) const;  Alexandre Duret-Lutz committed Aug 15, 2014 951 952  public:  Alexandre Duret-Lutz committed Oct 08, 2014 953 #ifndef SWIG  Alexandre Duret-Lutz committed Feb 02, 2016 954 955  /// \brief Declare a named property ///  Alexandre Duret-Lutz committed Jul 18, 2016 956  /// Arbitrary objects can be attached to automata. Those are called  Alexandre Duret-Lutz committed Feb 02, 2016 957 958 959 960 961 962 963 964  /// named properties. They are used for instance to name all the /// state of an automaton. /// /// This function attaches the object \a val to the current automaton, /// under the name \a s. /// /// When the automaton is destroyed, the \a destructor function will /// be called to destroy the attached object.  Alexandre Duret-Lutz committed Jul 15, 2016 965 966 967  /// /// See https://spot.lrde.epita.fr/concepts.html#named-properties /// for a list of named properties used by Spot.  Alexandre Duret-Lutz committed Oct 08, 2014 968  void set_named_prop(std::string s,  Laurent XU committed Mar 10, 2016 969  void* val, std::function destructor);  Alexandre Duret-Lutz committed Dec 09, 2014 970   Alexandre Duret-Lutz committed Feb 02, 2016 971 972  /// \brief Declare a named property ///  Alexandre Duret-Lutz committed Jul 18, 2016 973  /// Arbitrary objects can be attached to automata. Those are called  Alexandre Duret-Lutz committed Feb 02, 2016 974 975 976  /// named properties. They are used for instance to name all the /// state of an automaton. ///  Alexandre Duret-Lutz committed Jul 18, 2016 977  ///  Alexandre Duret-Lutz committed Feb 02, 2016 978 979 980  /// This function attaches the object \a val to the current automaton, /// under the name \a s. ///  Alexandre Duret-Lutz committed Jul 18, 2016 981 982  /// When the automaton is destroyed, the \a destructor function will /// be called to destroy the attached object.  Alexandre Duret-Lutz committed Jul 15, 2016 983 984 985  /// /// See https://spot.lrde.epita.fr/concepts.html#named-properties /// for a list of named properties used by Spot.  Alexandre Duret-Lutz committed Dec 09, 2014 986 987 988 989 990 991  template void set_named_prop(std::string s, T* val) { set_named_prop(s, val, [](void *p) { delete static_cast(p); }); }  Alexandre Duret-Lutz committed Jul 18, 2016 992 993 994 995 996 997 998 999 1000  /// \brief Erase a named property /// /// Arbitrary objects can be attached to automata. Those are called /// named properties. They are used for instance to name all the /// state of an automaton. /// /// This function removes the property \a s if it exists. /// /// See https://spot.lrde.epita.fr/concepts.html#named-properties