emptiness.hh 16.4 KB
 Alexandre Duret-Lutz committed Jul 29, 2013 1 // -*- coding: utf-8 -*-  Alexandre Duret-Lutz committed Mar 18, 2018 2 // Copyright (C) 2011, 2013, 2014, 2015, 2016, 2017, 2018 Laboratoire de  Alexandre Duret-Lutz committed Feb 04, 2017 3 // Recherche et Developpement de l'Epita (LRDE).  Alexandre Duret-Lutz committed Oct 26, 2011 4 // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),  Alexandre Duret-Lutz committed Jul 29, 2013 5 // département Systèmes Répartis Coopératifs (SRC), Université Pierre  Alexandre Duret-Lutz committed Oct 27, 2004 6 7 8 9 10 11 // et Marie Curie. // // 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 Oct 27, 2004 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 Oct 27, 2004 22   Etienne Renault committed Mar 23, 2015 23 #pragma once  Alexandre Duret-Lutz committed Oct 27, 2004 24   Denis Poitrenaud committed Feb 07, 2005 25 #include  Alexandre Duret-Lutz committed Oct 27, 2004 26 27 #include #include  Alexandre Duret-Lutz committed Oct 30, 2014 28 #include  Alexandre Duret-Lutz committed Dec 04, 2015 29 30 31 #include #include #include  Alexandre Duret-Lutz committed Oct 27, 2004 32 33 34  namespace spot {  Alexandre Duret-Lutz committed Oct 24, 2015 35 36 37  struct twa_run; typedef std::shared_ptr twa_run_ptr; typedef std::shared_ptr const_twa_run_ptr;  Alexandre Duret-Lutz committed Nov 10, 2004 38   Alexandre Duret-Lutz committed Nov 17, 2004 39  /// \addtogroup emptiness_check Emptiness-checks  Alexandre Duret-Lutz committed Apr 22, 2015 40  /// \ingroup twa_algorithms  Alexandre Duret-Lutz committed Nov 10, 2004 41  ///  Alexandre Duret-Lutz committed Apr 20, 2016 42 43 44 45 46 47 48 49 50  /// You can create an emptiness check either by instantiating it /// explicitly (calling one of the functions of \ref /// emptiness_check_algorithms "this list"), or indirectly via /// spot::make_emptiness_check_instantiator(). The latter function /// allows user-options to influence the choice of the /// emptiness-check algorithm used, and the intermediate /// instantiator object can be used to query to properties of the /// emptiness check selected. ///  Alexandre Duret-Lutz committed Nov 16, 2004 51 52  /// All emptiness-check algorithms follow the same interface. /// Basically once you have constructed an instance of  Alexandre Duret-Lutz committed Apr 20, 2016 53  /// spot::emptiness_check, you should call  Alexandre Duret-Lutz committed Nov 16, 2004 54  /// spot::emptiness_check::check() to check the automaton.  Alexandre Duret-Lutz committed Nov 10, 2004 55  ///  Alexandre Duret-Lutz committed Nov 16, 2004 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73  /// If spot::emptiness_check::check() returns 0, then the automaton /// was found empty. Otherwise the automaton accepts some run. /// (Beware that some algorithms---those using bit-state /// hashing---may found the automaton to be empty even if it is not /// actually empty.) /// /// When spot::emptiness_check::check() does not return 0, it /// returns an instance of spot::emptiness_check_result. You can /// try to call spot::emptiness_check_result::accepting_run() to /// obtain an accepting run. For some emptiness-check algorithms, /// spot::emptiness_check_result::accepting_run() will require some /// extra computation. Most emptiness-check algorithms are able to /// return such an accepting run, however this is not mandatory and /// spot::emptiness_check_result::accepting_run() can return 0 (this /// does not means by anyway that no accepting run exist). /// /// The acceptance run returned by /// spot::emptiness_check_result::accepting_run(), if any, is of  Alexandre Duret-Lutz committed Oct 24, 2015 74  /// type spot::twa_run. \ref twa_run "This page" gathers existing  Alexandre Duret-Lutz committed Nov 16, 2004 75 76 77  /// operations on these objects. /// /// @{  Alexandre Duret-Lutz committed Oct 27, 2004 78 79 80 81 82 83  /// \brief The result of an emptiness check. /// /// Instances of these class should not last longer than the /// instances of emptiness_check that produced them as they /// may reference data internal to the check.  Alexandre Duret-Lutz committed Jul 29, 2013 84  class SPOT_API emptiness_check_result  Alexandre Duret-Lutz committed Oct 27, 2004 85 86  { public:  Alexandre Duret-Lutz committed Apr 22, 2015 87  emptiness_check_result(const const_twa_ptr& a,  Laurent XU committed Mar 10, 2016 88  option_map o = option_map())  Denis Poitrenaud committed Feb 07, 2005 89 90 91 92 93 94  : a_(a), o_(o) { } virtual ~emptiness_check_result()  Alexandre Duret-Lutz committed Nov 25, 2004 95 96 97  { }  Alexandre Duret-Lutz committed Oct 27, 2004 98 99 100 101 102 103 104 105 106 107 108 109  /// \brief Return a run accepted by the automata passed to /// the emptiness check. /// /// This method might actually compute the acceptance run. (Not /// all emptiness check algorithms actually produce a /// counter-example as a side-effect of checking emptiness, some /// need some post-processing.) /// /// This can also return 0 if the emptiness check algorithm /// cannot produce a counter example (that does not mean there /// is no counter-example; the mere existence of an instance of /// this class asserts the existence of a counter-example).  Alexandre Duret-Lutz committed Oct 24, 2015 110  virtual twa_run_ptr accepting_run();  Alexandre Duret-Lutz committed Nov 25, 2004 111 112  /// The automaton on which an accepting_run() was found.  Alexandre Duret-Lutz committed Apr 22, 2015 113  const const_twa_ptr&  Alexandre Duret-Lutz committed Nov 25, 2004 114 115 116 117  automaton() const { return a_; }  Alexandre Duret-Lutz committed Feb 03, 2005 118   Denis Poitrenaud committed Feb 07, 2005 119 120 121 122 123 124 125  /// Return the options parametrizing how the accepting run is computed. const option_map& options() const { return o_; }  Alexandre Duret-Lutz committed Feb 17, 2005 126 127  /// Modify the algorithm options. const char* parse_options(char* options);  Denis Poitrenaud committed Feb 07, 2005 128   Alexandre Duret-Lutz committed Feb 03, 2005 129 130 131  /// Return statistics, if available. virtual const unsigned_statistics* statistics() const;  Alexandre Duret-Lutz committed Nov 25, 2004 132  protected:  Alexandre Duret-Lutz committed Feb 17, 2005 133 134  /// Notify option updates. virtual void options_updated(const option_map& old);  Denis Poitrenaud committed Feb 07, 2005 135   Laurent XU committed Mar 10, 2016 136 137  const_twa_ptr a_; ///< The automaton. option_map o_; ///< The options.  Alexandre Duret-Lutz committed Oct 27, 2004 138 139  };  Alexandre Duret-Lutz committed Aug 23, 2014 140 141  typedef std::shared_ptr emptiness_check_result_ptr;  Alexandre Duret-Lutz committed Oct 27, 2004 142  /// Common interface to emptiness check algorithms.  Alexandre Duret-Lutz committed Aug 23, 2014 143 144  class SPOT_API emptiness_check: public std::enable_shared_from_this  Alexandre Duret-Lutz committed Oct 27, 2004 145 146  { public:  Alexandre Duret-Lutz committed Apr 22, 2015 147  emptiness_check(const const_twa_ptr& a, option_map o = option_map())  Denis Poitrenaud committed Feb 07, 2005 148  : a_(a), o_(o)  Alexandre Duret-Lutz committed Nov 25, 2004 149 150  { }  Alexandre Duret-Lutz committed Oct 27, 2004 151 152  virtual ~emptiness_check();  Alexandre Duret-Lutz committed Nov 25, 2004 153  /// The automaton that this emptiness-check inspects.  Alexandre Duret-Lutz committed Apr 22, 2015 154  const const_twa_ptr&  Alexandre Duret-Lutz committed Nov 25, 2004 155 156 157 158 159  automaton() const { return a_; }  Denis Poitrenaud committed Feb 07, 2005 160 161 162 163 164 165 166  /// Return the options parametrizing how the emptiness check is realized. const option_map& options() const { return o_; }  Alexandre Duret-Lutz committed Feb 17, 2005 167 168 169 170 171  /// Modify the algorithm options. const char* parse_options(char* options); /// Return false iff accepting_run() can return 0 for non-empty automata. virtual bool safe() const;  Denis Poitrenaud committed Feb 07, 2005 172   Alexandre Duret-Lutz committed Oct 27, 2004 173 174  /// \brief Check whether the automaton contain an accepting run. ///  Alexandre Duret-Lutz committed Feb 17, 2005 175  /// Return 0 if the automaton accepts no run. Return an instance  Alexandre Duret-Lutz committed Oct 27, 2004 176 177 178 179 180 181 182  /// of emptiness_check_result otherwise. This instance might /// allow to obtain one sample acceptance run. The result has to /// be destroyed before the emptiness_check instance that /// generated it. /// /// Some emptiness_check algorithms may allow check() to be called /// several time, but generally you should not assume that.  Alexandre Duret-Lutz committed Feb 17, 2005 183 184 185 186  /// /// Some emptiness_check algorithms, especially those using bit state /// hashing may return 0 even if the automaton is not empty. /// \see safe()  Alexandre Duret-Lutz committed Aug 23, 2014 187  virtual emptiness_check_result_ptr check() = 0;  Alexandre Duret-Lutz committed Oct 27, 2004 188   Alexandre Duret-Lutz committed Feb 03, 2005 189 190 191  /// Return statistics, if available. virtual const unsigned_statistics* statistics() const;  Alexandre Duret-Lutz committed Aug 23, 2014 192 193 194  /// Return emptiness check statistics, if available. virtual const ec_statistics* emptiness_check_statistics() const;  Alexandre Duret-Lutz committed Oct 27, 2004 195 196  /// Print statistics, if any. virtual std::ostream& print_stats(std::ostream& os) const;  Alexandre Duret-Lutz committed Nov 25, 2004 197   Alexandre Duret-Lutz committed Feb 17, 2005 198 199  /// Notify option updates. virtual void options_updated(const option_map& old);  Denis Poitrenaud committed Feb 07, 2005 200   Alexandre Duret-Lutz committed Nov 25, 2004 201  protected:  Laurent XU committed Mar 10, 2016 202 203  const_twa_ptr a_; ///< The automaton. option_map o_; ///< The options  Alexandre Duret-Lutz committed Oct 27, 2004 204 205  };  Alexandre Duret-Lutz committed Aug 23, 2014 206 207 208 209 210  typedef std::shared_ptr emptiness_check_ptr; class emptiness_check_instantiator; typedef std::shared_ptr emptiness_check_instantiator_ptr;  Alexandre Duret-Lutz committed Feb 17, 2005 211   Alexandre Duret-Lutz committed Apr 20, 2016 212  /// Dynamically create emptiness checks. Given their name and options.  Alexandre Duret-Lutz committed Jul 29, 2013 213  class SPOT_API emptiness_check_instantiator  Alexandre Duret-Lutz committed Feb 17, 2005 214 215 216  { public: /// Actually instantiate the emptiness check, for \a a.  Alexandre Duret-Lutz committed Apr 22, 2015 217  emptiness_check_ptr instantiate(const const_twa_ptr& a) const;  Alexandre Duret-Lutz committed Feb 17, 2005 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233  /// Accessor to the options. /// @{ const option_map& options() const { return o_; } option_map& options() { return o_; } /// @}  Alexandre Duret-Lutz committed Mar 03, 2016 234  /// \brief Minimum number of acceptance sets supported by  Alexandre Duret-Lutz committed Feb 17, 2005 235  /// the emptiness check.  Alexandre Duret-Lutz committed Mar 03, 2016 236  unsigned int min_sets() const;  Alexandre Duret-Lutz committed Feb 17, 2005 237 238 239 240 241  /// \brief Maximum number of acceptance conditions supported by /// the emptiness check. /// /// \return \c -1U if no upper bound exists.  Alexandre Duret-Lutz committed Mar 03, 2016 242  unsigned int max_sets() const;  Alexandre Duret-Lutz committed Aug 23, 2014 243  protected:  Alexandre Duret-Lutz committed Feb 17, 2005 244  emptiness_check_instantiator(option_map o, void* i);  Alexandre Duret-Lutz committed Aug 23, 2014 245   Alexandre Duret-Lutz committed Feb 17, 2005 246 247 248 249  option_map o_; void *info_; };  Alexandre Duret-Lutz committed Aug 23, 2014 250 251 252  /// \brief Create an emptiness-check instantiator, given the name /// of an emptiness check. ///  Alexandre Duret-Lutz committed Apr 20, 2016 253 254 255 256  /// This is a convenient entry point to instantiate an emptiness /// check with user-supplied options. /// /// \param name should have the form \c "name" or \c "name(options)".  Alexandre Duret-Lutz committed Aug 23, 2014 257  ///  Alexandre Duret-Lutz committed Apr 20, 2016 258 259 260  /// \return Return an emptiness-check instantiator. On error, the /// function returns \c nullptr. If the name of the algorithm was /// unknown, \c *err will be set to \c name. If some fragment of  Alexandre Duret-Lutz committed Aug 23, 2014 261 262  /// the options could not be parsed, \c *err will point to that /// fragment.  Alexandre Duret-Lutz committed Apr 20, 2016 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360  /// /// The following names supported and correspond to different emptiness /// check algorithms: /// - Cou99 uses spot::couvreur99(), that works with Fin-less /// acceptance conditions, with any number of acceptance sets. /// The following options can be used: /// - shy Compute all successors of each state, then explore already /// visited states first. This usually helps to merge SCCs, and /// thus exit sooner. However because all successors have to be /// computed and stored, it often consume more memory. /// - group Setting this option is meaningful only when shy is /// used. If set (the default), the successors of all the states /// that belong to the same SCC will be considered when choosing /// a successor. Otherwise, only the successor of the topmost /// state on the DFS stack are considered. /// - poprem Specifies how the algorithm should handle the /// destruction of non-accepting maximal strongly connected /// components. If poprem is set, the algorithm will keep a list /// of all states of a SCC that are fully processed and should be /// removed once the MSCC is popped. If poprem is unset (the /// default), the MSCC will be traversed again (i.e. generating /// the successors of the root recursively) for deletion. This /// is a choice between memory and speed. /// /// Examples: /// \code /// Cou99 /// Cou99(shy !group) /// Cou99(shy group) /// Cou99(poprem) /// Cou99(poprem shy !group) /// Cou99(poprem shy group) /// \endcode /// /// - GC04 uses spot::explicit_gv04_check() and works on automata /// with Fin-less acceptance conditions using at most one acceptance /// set. No options are supported. /// /// Example: /// \code /// GC04 /// \endcode /// /// - CVWY90 uses spot::magic_search() and work on automata with /// Fin-less acceptance conditions using at most one acceptance /// set. Set option bsh to the size of a hash-table if you want /// to activate bit-state hashing. /// /// Examples: /// \code /// CVWY90 /// CVWY90(bsh=4M) /// \endcode /// /// - SE05 uses spot::se05() and works on work on automata with /// Fin-less acceptance conditions using at most one acceptance /// set. Set option bsh to the size of a hash-table if you want /// to activate bit-state hashing. /// /// Examples: /// \code /// SE05 /// SE05(bsh=4M) /// \endcode /// /// - Tau03 uses spot::explicit_tau03_search() and work on automata with /// Fin-less acceptance conditions using at least one acceptance /// set. No options are supported. /// /// Example: /// \code /// Tau03 /// \endcode /// /// - Tau03_opt uses spot::explicit_tau03_opt_search() and work on /// automata with any Fin-less acceptance. The following options are /// supported: /// - weights This option is set by default and activates the usage /// of weights in the top-level DFS as well as in nested DFSs. /// - redweights This option is set by default, and activates the /// usage of weights in nested DFSs. It is meaningful only if /// weights is set. /// - condstack This option is unset by default, and activates /// the use of the "conditional stack" optimization described by /// Heikki Tauriainen. /// - ordering This option is unset by default, and activates the /// use of the "ordering" heuristic described by Heikki Tauriainen /// in Research Report A96 from the Helsinki University of Technology. /// /// Example: /// \code /// Tau03_opt /// Tau03_opt(!weights) /// Tau03_opt(!redweights) /// Tau03_opt(condstack) /// Tau03_opt(condstack !weights) /// Tau03_opt(condstack !redweights) /// \endcode  Alexandre Duret-Lutz committed Aug 23, 2014 361 362  SPOT_API emptiness_check_instantiator_ptr make_emptiness_check_instantiator(const char* name, const char** err);  Alexandre Duret-Lutz committed Feb 17, 2005 363   Alexandre Duret-Lutz committed Apr 20, 2016 364 365  /// @}  Alexandre Duret-Lutz committed Nov 16, 2004 366 367 368 369  /// \addtogroup emptiness_check_algorithms Emptiness-check algorithms /// \ingroup emptiness_check  Alexandre Duret-Lutz committed Oct 25, 2015 370  /// \addtogroup twa_run TωA runs and supporting functions  Alexandre Duret-Lutz committed Nov 16, 2004 371 372 373  /// \ingroup emptiness_check /// @{  Alexandre Duret-Lutz committed Oct 25, 2015 374 375  /// An accepted run, for a twa. struct SPOT_API twa_run final  Alexandre Duret-Lutz committed Nov 16, 2004 376 377 378 379  { struct step { const state* s; bdd label;  Alexandre Duret-Lutz committed Oct 06, 2014 380  acc_cond::mark_t acc;  Alexandre Duret-Lutz committed Jan 09, 2015 381 382  step(const state* s, bdd label, acc_cond::mark_t acc)  Laurent XU committed Mar 10, 2016 383  : s(s), label(label), acc(acc)  Alexandre Duret-Lutz committed Jan 09, 2015 384 385 386 387 388  { } step() { }  Alexandre Duret-Lutz committed Nov 16, 2004 389 390 391 392 393 394  }; typedef std::list steps; steps prefix; steps cycle;  Alexandre Duret-Lutz committed Oct 25, 2015 395  const_twa_ptr aut;  Alexandre Duret-Lutz committed Nov 16, 2004 396   Alexandre Duret-Lutz committed Oct 24, 2015 397  ~twa_run();  Alexandre Duret-Lutz committed Oct 25, 2015 398 399  twa_run(const const_twa_ptr& aut) : aut(aut)  Alexandre Duret-Lutz committed Nov 16, 2004 400  {  Alexandre Duret-Lutz committed Oct 25, 2015 401  }  Alexandre Duret-Lutz committed Oct 24, 2015 402 403  twa_run(const twa_run& run); twa_run& operator=(const twa_run& run);  Alexandre Duret-Lutz committed Oct 25, 2015 404   Alexandre Duret-Lutz committed Mar 18, 2018 405 406 407 408 409 410 411 412 413  /// \brief Raise an exception of the cycle is empty. /// /// It is OK for a twa_run to have an empty cycle while the run is /// being filled by some procedure. But after that, we expect /// cycles to be non-empty. Calling this function will raise an /// std::runtime_error if the cycle is empty, giving \a where /// (usually the name of the calling function) as context. void ensure_non_empty_cycle(const char* where) const;  Alexandre Duret-Lutz committed Oct 25, 2015 414 415 416 417 418 419  /// \brief Reduce an accepting run. /// /// Return a run which is still accepting for aut, /// but is no longer than this one. twa_run_ptr reduce() const;  Alexandre Duret-Lutz committed Jul 18, 2016 420 421 422 423 424 425 426 427 428 429  /// \brief Project an accepting run /// /// This only works if the automaton associated to this run has /// been created with otf_product() or product(), and \a other is /// one of the two operands of the product. /// /// Use the \a right Boolean to specify whether \a other was a /// left or right operand. twa_run_ptr project(const const_twa_ptr& other, bool right = false);  Alexandre Duret-Lutz committed Oct 25, 2015 430 431 432 433  /// \brief Replay a run. /// /// This is similar to os << run;, except that the /// run is actually replayed on the automaton while it is printed.  Alexandre Duret-Lutz committed Feb 15, 2016 434  /// The output will stop if the run cannot be completed.  Alexandre Duret-Lutz committed Oct 25, 2015 435 436 437 438 439 440 441  /// /// \param os the stream on which the replay should be traced /// \param debug if set the output will be more verbose and extra /// debugging informations will be output on failure /// \return true iff the run could be completed bool replay(std::ostream& os, bool debug = false) const;  Alexandre Duret-Lutz committed Feb 06, 2016 442 443 444 445 446  /// \brief Highlight the accepting run on the automaton. /// /// Note that this works only if the automaton is a twa_graph_ptr. void highlight(unsigned color);  Alexandre Duret-Lutz committed Oct 25, 2015 447 448 449  /// \brief Return a twa_graph_ptr corresponding to \a run /// /// Identical states are merged.  Alexandre Duret-Lutz committed Feb 04, 2017 450 451 452 453  /// /// If \a preserve_names is set, the created states are named /// using the format_state() result from the original state. twa_graph_ptr as_twa(bool preserve_names = false) const;  Alexandre Duret-Lutz committed Oct 25, 2015 454   Alexandre Duret-Lutz committed Oct 25, 2015 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469  /// \brief Display a twa_run. /// /// Output the prefix and cycle parts of the twa_run \a run on \a os. /// /// The automaton object (stored by \a run) is used only to format /// the states, and to know how to print the BDDs describing the /// conditions and acceptance conditions of the run; it is /// not used to replay the run. In other words this /// function will work even if the twa_run you are trying to print /// appears to connect states that are not connected. /// /// This is unlike replay_twa_run(), which will ensure the run /// actually exists in the automaton (and will also display any /// transition annotation). SPOT_API  Alexandre Duret-Lutz committed Oct 29, 2015 470  friend std::ostream& operator<<(std::ostream& os, const twa_run& run);  Alexandre Duret-Lutz committed Nov 16, 2004 471  };  Denis Poitrenaud committed Dec 08, 2004 472  /// @}  Alexandre Duret-Lutz committed Jan 03, 2005 473 474 475  /// \addtogroup emptiness_check_stats Emptiness-check statistics /// \ingroup emptiness_check  Alexandre Duret-Lutz committed Oct 27, 2004 476 }