magic.hh 3.06 KB
 Alexandre Duret-Lutz committed Jul 28, 2003 1 2 3 4 5 6 7 8 9 10 11 ``````#ifndef SPOT_TGBAALGOS_MAGIC_HH # define SPOT_TGBAALGOS_MAGIC_HH #include #include #include #include "tgba/tgbatba.hh" namespace spot { /// \brief Emptiness check on spot::tgba_tba_proxy automata using `````` Alexandre Duret-Lutz committed Jul 30, 2003 12 `````` /// the Magic Search algorithm. `````` Alexandre Duret-Lutz committed Jul 28, 2003 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 `````` /// /// This algorithm comes from /// \verbatim /// @InProceedings{ godefroid.93.pstv, /// author = {Patrice Godefroid and Gerard .J. Holzmann}, /// title = {On the verification of temporal properties}, /// booktitle = {Proceedings of the 13th IFIP TC6/WG6.1 International /// Symposium on Protocol Specification, Testing, and /// Verification (PSTV'93)}, /// month = {May}, /// editor = {Andr{\'e} A. S. Danthine and Guy Leduc /// and Pierre Wolper}, /// address = {Liege, Belgium}, /// pages = {109--124}, /// publisher = {North-Holland}, /// year = {1993}, /// series = {IFIP Transactions}, /// volume = {C-16}, /// isbn = {0-444-81648-8} /// } /// \endverbatim struct magic_search { /// Initialize the Magic Search algorithm on the automaton \a a. magic_search(const tgba_tba_proxy *a); ~magic_search(); /// \brief Perform a Magic Search. `````` Alexandre Duret-Lutz committed Jul 30, 2003 41 `````` /// `````` Alexandre Duret-Lutz committed Jul 28, 2003 42 43 44 45 46 47 48 `````` /// \return true iff the algorithm has found a new accepting /// path. /// /// check() can be called several times until it return false, /// to enumerate all accepting paths. bool check(); `````` Alexandre Duret-Lutz committed Jul 30, 2003 49 50 51 52 `````` /// \brief Print the last accepting path found. /// /// Restrict printed states to \a the state space of restrict if /// supplied. `````` Alexandre Duret-Lutz committed Jul 30, 2003 53 `````` std::ostream& print_result(std::ostream& os, `````` Alexandre Duret-Lutz committed Jul 30, 2003 54 `````` const tgba* restrict = 0) const; `````` Alexandre Duret-Lutz committed Jul 28, 2003 55 56 57 58 59 60 61 62 63 64 65 66 `````` private: // The names "stack", "h", and "x", are those used in the paper. /// \brief Records whether a state has be seen with the magic bit /// on or off. struct magic { bool seen_without : 1; bool seen_with : 1; }; `````` Alexandre Duret-Lutz committed Jul 30, 2003 67 `````` `````` Alexandre Duret-Lutz committed Jul 28, 2003 68 69 70 71 72 73 74 75 76 77 78 79 `````` /// \brief A state for the spot::magic_search algorithm. struct magic_state { const state* s; bool m; ///< The state of the magic demon. }; typedef std::pair state_iter_pair; typedef std::list stack_type; stack_type stack; ///< Stack of visited states on the path. typedef std::list tstack_type; `````` Alexandre Duret-Lutz committed Jul 30, 2003 80 `````` /// \brief Stack of transitions. `````` Alexandre Duret-Lutz committed Jul 28, 2003 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 `````` /// /// This is an addition to the data from the paper. tstack_type tstack; // FIXME: use a hash_map. typedef std::map hash_type; hash_type h; ///< Map of visited states. /// Append a new state to the current path. void push(const state* s, bool m); /// Check whether we already visited \a s with the Magic bit set to \a m. bool has(const state* s, bool m) const; const tgba_tba_proxy* a; ///< The automata to check. /// The state for which we are currently seeking an SCC. `````` Alexandre Duret-Lutz committed Jul 30, 2003 96 `````` const state* x; `````` Alexandre Duret-Lutz committed Jul 28, 2003 97 98 99 100 101 102 `````` }; } #endif // SPOT_TGBAALGOS_MAGIC_HH``````