simulation.hh 5.97 KB
 Thomas Badie committed Apr 18, 2012 1 ``````// -*- coding: utf-8 -*- `````` Alexandre Duret-Lutz committed Jan 19, 2015 2 ``````// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et `````` Alexandre Duret-Lutz committed Jun 20, 2014 3 ``````// Développement de l'Epita (LRDE). `````` Thomas Badie committed Apr 18, 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 `````` 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 `````` `````` Etienne Renault committed Mar 23, 2015 20 ``````#pragma once `````` Thomas Badie committed Apr 18, 2012 21 `````` `````` Alexandre Duret-Lutz committed Dec 04, 2015 22 23 ``````#include #include `````` Alexandre Duret-Lutz committed Jul 29, 2013 24 `````` `````` Thomas Badie committed Apr 18, 2012 25 26 ``````namespace spot { `````` Alexandre Duret-Lutz committed Apr 22, 2015 27 `````` /// \addtogroup twa_reduction `````` Thomas Badie committed Apr 18, 2012 28 29 `````` /// @{ `````` Alexandre Duret-Lutz committed May 12, 2013 30 `````` /// @{ `````` Alexandre Duret-Lutz committed Aug 21, 2012 31 32 33 34 35 `````` /// \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 `````` Alexandre Duret-Lutz committed May 14, 2015 36 `````` /// based on the following paper, but generalized to handle TωA `````` Alexandre Duret-Lutz committed Aug 21, 2012 37 `````` /// directly. `````` Thomas Badie committed Apr 18, 2012 38 `````` /// `````` Alexandre Duret-Lutz committed Jun 09, 2013 39 40 41 42 43 `````` /** \verbatim @InProceedings{ etessami.00.concur, author = {Kousha Etessami and Gerard J. Holzmann}, title = {Optimizing {B\"u}chi Automata}, booktitle = {Proceedings of the 11th International Conference on `````` Laurent XU committed Mar 10, 2016 44 `````` Concurrency Theory (Concur'00)}, `````` Alexandre Duret-Lutz committed Jun 09, 2013 45 46 47 48 49 50 51 52 53 `````` pages = {153--167}, year = {2000}, editor = {C. Palamidessi}, volume = {1877}, series = {Lecture Notes in Computer Science}, address = {Pennsylvania, USA}, publisher = {Springer-Verlag} } \endverbatim */ `````` Thomas Badie committed Apr 18, 2012 54 `````` /// `````` 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 `````` Alexandre Duret-Lutz committed Apr 22, 2015 70 71 72 `````` SPOT_API twa_graph_ptr simulation(const const_twa_graph_ptr& automaton); SPOT_API twa_graph_ptr `````` Alexandre Lewkowicz committed Feb 12, 2016 73 `````` simulation(const const_twa_graph_ptr& automaton, `````` Alexandre Duret-Lutz committed Oct 21, 2016 74 `````` std::vector* implications); `````` Alexandre Lewkowicz committed Feb 12, 2016 75 `````` SPOT_API twa_graph_ptr `````` Alexandre Duret-Lutz committed Apr 22, 2015 76 `````` simulation_sba(const const_twa_graph_ptr& automaton); `````` Alexandre Duret-Lutz committed May 12, 2013 77 `````` /// @} `````` Thomas Badie committed Apr 18, 2012 78 `````` `````` Alexandre Duret-Lutz committed May 12, 2013 79 `````` /// @{ `````` Alexandre Duret-Lutz committed Aug 21, 2012 80 81 82 83 84 85 `````` /// \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. /// `````` Alexandre Duret-Lutz committed Jan 19, 2015 86 `````` /// Reverse simulation is discussed in the following paper, `````` Alexandre Duret-Lutz committed May 14, 2015 87 `````` /// but generalized to handle TωA directly. `````` Alexandre Duret-Lutz committed Jun 09, 2013 88 89 `````` /** \verbatim @InProceedings{ somenzi.00.cav, `````` Laurent XU committed Mar 10, 2016 90 91 `````` author = {Fabio Somenzi and Roderick Bloem}, title = {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}}, `````` Alexandre Duret-Lutz committed Jun 09, 2013 92 93 94 95 96 97 98 99 100 101 `````` 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} } \endverbatim */ `````` Alexandre Duret-Lutz committed Aug 21, 2012 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 `````` /// /// 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 123 124 125 `````` /// \param automaton the automaton to simulate. /// \return a new automaton which is at worst a copy of the received /// one `````` Alexandre Duret-Lutz committed Apr 22, 2015 126 127 128 129 `````` SPOT_API twa_graph_ptr cosimulation(const const_twa_graph_ptr& automaton); SPOT_API twa_graph_ptr cosimulation_sba(const const_twa_graph_ptr& automaton); `````` Alexandre Duret-Lutz committed May 12, 2013 130 `````` /// @} `````` Thomas Badie committed Aug 21, 2012 131 `````` `````` Alexandre Duret-Lutz committed May 12, 2013 132 `````` /// @{ `````` Alexandre Duret-Lutz committed Aug 21, 2012 133 134 135 136 137 138 139 140 141 142 143 144 145 146 `````` /// \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 `````` Alexandre Duret-Lutz committed Apr 22, 2015 147 148 149 150 `````` SPOT_API twa_graph_ptr iterated_simulations(const const_twa_graph_ptr& automaton); SPOT_API twa_graph_ptr iterated_simulations_sba(const const_twa_graph_ptr& automaton); `````` Alexandre Duret-Lutz committed May 12, 2013 151 `````` /// @} `````` Thomas Badie committed Aug 21, 2012 152 `````` `````` Thomas Badie committed Apr 18, 2012 153 ``} // End namespace spot.``