simulation.hh 5.84 KB
 Thomas Badie committed Apr 18, 2012 1 ``````// -*- coding: utf-8 -*- `````` Alexandre Duret-Lutz committed May 12, 2013 2 ``````// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement `````` Thomas Badie committed Apr 18, 2012 3 4 5 6 7 8 ``````// de l'Epita (LRDE). // // 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 `````` Thomas Badie committed Apr 18, 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 . `````` Thomas Badie committed Apr 18, 2012 19 20 21 22 23 24 25 26 27 28 29 `````` #ifndef SPOT_TGBAALGOS_SIMULATION_HH # define SPOT_TGBAALGOS_SIMULATION_HH namespace spot { class tgba; /// \addtogroup tgba_reduction /// @{ `````` Alexandre Duret-Lutz committed May 12, 2013 30 `````` /// @{ `````` Alexandre Duret-Lutz committed Aug 21, 2012 31 32 33 34 35 36 37 `````` /// \brief Attempt to reduce the automaton by direct simulation. /// /// When the suffixes (letter and acceptance conditions) reachable /// from one state are included in the suffixes seen by another one, /// the former state can be merged into the latter. The algorithm is /// based on the following paper, but generalized to handle TGBA /// directly. `````` Thomas Badie committed Apr 18, 2012 38 39 `````` /// /// \verbatim `````` Alexandre Duret-Lutz committed Apr 27, 2012 40 `````` /// @InProceedings{ etessami.00.concur, `````` Thomas Badie committed Apr 18, 2012 41 42 43 `````` /// author = {Kousha Etessami and Gerard J. Holzmann}, /// title = {Optimizing {B\"u}chi Automata}, /// booktitle = {Proceedings of the 11th International Conference on `````` Alexandre Duret-Lutz committed Apr 27, 2012 44 `````` /// Concurrency Theory (Concur'00)}, `````` Thomas Badie committed Apr 18, 2012 45 46 47 48 49 50 51 52 53 54 `````` /// pages = {153--167}, /// year = {2000}, /// editor = {C. Palamidessi}, /// volume = {1877}, /// series = {Lecture Notes in Computer Science}, /// address = {Pennsylvania, USA}, /// publisher = {Springer-Verlag} /// } /// \endverbatim /// `````` Alexandre Duret-Lutz committed Aug 21, 2012 55 56 57 58 59 60 61 62 63 64 65 66 `````` /// Our reconstruction of the quotient automaton based on this /// suffix-inclusion relation will also improve determinism. /// /// We recommend to call scc_filter() to first simplify the /// automaton that should be reduced by simulation. /// /// Reducing an automaton by simulation does not change the number /// of acceptance conditions. In some rare cases (1 out of more /// than 500 in our benchmark), the reduced automaton will use more /// acceptance conditions than necessary, and running scc_filter() /// again afterwards will remove these superfluous conditions. /// `````` Alexandre Duret-Lutz committed Apr 27, 2012 67 `````` /// \param automaton the automaton to simulate. `````` Thomas Badie committed Apr 18, 2012 68 `````` /// \return a new automaton which is at worst a copy of the received `````` Alexandre Duret-Lutz committed Apr 27, 2012 69 `````` /// one `````` Thomas Badie committed Apr 18, 2012 70 `````` tgba* simulation(const tgba* automaton); `````` Alexandre Duret-Lutz committed May 12, 2013 71 72 `````` tgba* simulation_sba(const tgba* automaton); /// @} `````` Thomas Badie committed Apr 18, 2012 73 `````` `````` Alexandre Duret-Lutz committed May 12, 2013 74 `````` /// @{ `````` Alexandre Duret-Lutz committed Aug 21, 2012 75 76 77 78 79 80 81 `````` /// \brief Attempt to reduce the automaton by reverse simulation. /// /// When the prefixes (letter and acceptance conditions) leading to /// one state are included in the prefixes leading to one, the former /// state can be merged into the latter. /// /// Reverse simulation is discussed in the following paper, bu `````` Thomas Badie committed Aug 21, 2012 82 83 `````` /// following paper, but generalized to handle TGBA directly. /// \verbatim `````` Alexandre Duret-Lutz committed Aug 21, 2012 84 85 86 87 88 89 90 91 92 93 94 `````` /// @InProceedings{ somenzi.00.cav, /// author = {Fabio Somenzi and Roderick Bloem}, /// title = {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}}, /// booktitle = {Proceedings of the 12th International Conference on /// Computer Aided Verification (CAV'00)}, /// pages = {247--263}, /// year = {2000}, /// volume = {1855}, /// series = {Lecture Notes in Computer Science}, /// address = {Chicago, Illinois, USA}, /// publisher = {Springer-Verlag} `````` Thomas Badie committed Aug 21, 2012 95 96 `````` /// } /// \endverbatim `````` Alexandre Duret-Lutz committed Aug 21, 2012 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 `````` /// /// Our reconstruction of the quotient automaton based on this /// prefix-inclusion relation will also improve codeterminism. /// /// We recommend to call scc_filter() to first simplify the /// automaton that should be reduced by cosimulation. /// /// Reducing an automaton by reverse simulation (1) does not change /// the number of acceptance conditions so the resulting automaton /// may have superfluous acceptance conditions, and (2) can create /// SCCs that are terminal and non-accepting. For these reasons, /// you should call scc_filer() to prune useless SCCs and acceptance /// conditions afterwards. /// /// If you plan to run both simulation() and cosimulation() on the /// same automaton, you should start with simulation() so that the /// codeterminism improvements achieved by cosimulation() does not /// hinder the determinism improvements attempted by simulation(). /// (This of course assumes that you prefer determinism over /// codeterminism.) /// `````` Thomas Badie committed Aug 21, 2012 118 119 120 121 `````` /// \param automaton the automaton to simulate. /// \return a new automaton which is at worst a copy of the received /// one tgba* cosimulation(const tgba* automaton); `````` Alexandre Duret-Lutz committed May 12, 2013 122 123 `````` tgba* cosimulation_sba(const tgba* automaton); /// @} `````` Thomas Badie committed Aug 21, 2012 124 `````` `````` Alexandre Duret-Lutz committed May 12, 2013 125 `````` /// @{ `````` Alexandre Duret-Lutz committed Aug 21, 2012 126 127 128 129 130 131 132 133 134 135 136 137 138 139 `````` /// \brief Iterate simulation() and cosimulation(). /// /// Runs simulation(), cosimulation(), and scc_filter() in a loop, /// until the automaton does not change size (states and /// transitions). /// /// We recommend to call scc_filter() to first simplify the /// automaton that should be reduced by iterated simulations, since /// this algorithm will only call scc_filter() at the end of the /// loop. /// /// \param automaton the automaton to simulate. /// \return a new automaton which is at worst a copy of the received /// one `````` Thomas Badie committed Aug 21, 2012 140 `````` tgba* iterated_simulations(const tgba* automaton); `````` Alexandre Duret-Lutz committed May 12, 2013 141 142 `````` tgba* iterated_simulations_sba(const tgba* automaton); /// @} `````` Thomas Badie committed Aug 21, 2012 143 `````` `````` Thomas Badie committed Apr 09, 2013 144 145 146 147 148 149 150 `````` tgba* dont_care_simulation(const tgba* t, int limit = -1); tgba* dont_care_iterated_simulations(const tgba* t, int limit = -1); `````` Thomas Badie committed Apr 18, 2012 151 152 153 154 155 156 `````` /// @} } // End namespace spot. #endif // !SPOT_TGBAALGOS_SIMULATION_HH``````