minimize.hh 6.68 KB
 Alexandre Duret-Lutz committed Apr 30, 2012 1 // -*- coding: utf-8 -*-  Alexandre Duret-Lutz committed Jan 28, 2016 2 3 // Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 // Laboratoire de Recherche et Développement de l'Epita (LRDE).  Felix Abecassis committed Jan 05, 2011 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  Felix Abecassis committed Jan 05, 2011 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 .  Felix Abecassis committed Jan 05, 2011 19   Etienne Renault committed Mar 23, 2015 20 #pragma once  Felix Abecassis committed Jan 05, 2011 21   Alexandre Duret-Lutz committed Dec 04, 2015 22 23 #include #include  Felix Abecassis committed Jan 05, 2011 24 25 26  namespace spot {  Alexandre Duret-Lutz committed Apr 22, 2015 27  /// \addtogroup twa_reduction  Alexandre Duret-Lutz committed Jan 05, 2011 28 29 30  /// @{ /// \brief Construct a minimal deterministic monitor.  Alexandre Duret-Lutz committed Jan 05, 2011 31  ///  Alexandre Duret-Lutz committed Jan 05, 2011 32 33 34 35  /// The automaton will be converted into minimal deterministic /// monitor. All useless SCCs should have been previously removed /// (using scc_filter() for instance). Then the automaton will be /// determinized and minimized using the standard DFA construction  Alexandre Duret-Lutz committed Sep 24, 2012 36  /// as if all states were accepting states.  Alexandre Duret-Lutz committed Jan 05, 2011 37  ///  Alexandre Duret-Lutz committed Jan 05, 2011 38  /// For more detail about monitors, see the following paper:  Alexandre Duret-Lutz committed Jun 09, 2013 39 40 41 42 43  /** \verbatim @InProceedings{ tabakov.10.rv, author = {Deian Tabakov and Moshe Y. Vardi}, title = {Optimized Temporal Monitors for SystemC{$^*$}}, booktitle = {Proceedings of the 10th International Conferance  Alexandre Duret-Lutz committed Jan 28, 2016 44  on Runtime Verification},  Alexandre Duret-Lutz committed Jun 09, 2013 45 46 47 48 49 50 51 52  pages = {436--451}, year = 2010, volume = {6418}, series = {Lecture Notes in Computer Science}, month = nov, publisher = {Spring-Verlag} } \endverbatim */  Alexandre Duret-Lutz committed Jan 05, 2011 53 54  /// (Note: although the above paper uses Spot, this function did not /// exist in Spot at that time.)  Alexandre Duret-Lutz committed Jan 05, 2011 55  ///  Alexandre Duret-Lutz committed Jan 05, 2011 56 57 58  /// \param a the automaton to convert into a minimal deterministic monitor /// \pre Dead SCCs should have been removed from \a a before /// calling this function.  Alexandre Duret-Lutz committed Apr 22, 2015 59  SPOT_API twa_graph_ptr minimize_monitor(const const_twa_graph_ptr& a);  Alexandre Duret-Lutz committed Jan 05, 2011 60   Alexandre Duret-Lutz committed Apr 30, 2012 61  /// \brief Minimize a Büchi automaton in the WDBA class.  Alexandre Duret-Lutz committed Jan 05, 2011 62  ///  Alexandre Duret-Lutz committed Aug 28, 2012 63 64 65 66 67  /// This takes a TGBA whose language is representable by a Weak /// Deterministic Büchi Automaton, and construct a minimal WDBA for /// this language. This essentially chains three algorithms: /// determinization, acceptance adjustment (Löding's coloring /// algorithm), and minimization (using a Moore-like approache).  Alexandre Duret-Lutz committed Jan 05, 2011 68  ///  Alexandre Duret-Lutz committed Jan 05, 2011 69 70 71 72 73 74 75 76  /// If the input automaton does not represent a WDBA language, /// the resulting automaton is still a WDBA, but it will not /// be equivalent to the original automaton. Use the /// minimize_obligation() function if you are not sure whether /// it is safe to call this function. /// /// Please see the following paper for a discussion of this /// technique.  Alexandre Duret-Lutz committed Jan 05, 2011 77  ///  Alexandre Duret-Lutz committed Jun 09, 2013 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94  /** \verbatim @InProceedings{ dax.07.atva, author = {Christian Dax and Jochen Eisinger and Felix Klaedtke}, title = {Mechanizing the Powerset Construction for Restricted Classes of {$\omega$}-Automata}, year = 2007, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, volume = 4762, booktitle = {Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA'07)}, editor = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino and Yoshio Okamura}, month = oct } \endverbatim */  Alexandre Duret-Lutz committed Apr 22, 2015 95  SPOT_API twa_graph_ptr minimize_wdba(const const_twa_graph_ptr& a);  Alexandre Duret-Lutz committed Jan 05, 2011 96 97 98  /// \brief Minimize an automaton if it represents an obligation property. ///  Alexandre Duret-Lutz committed Jan 05, 2011 99 100  /// This function attempts to minimize the automaton \a aut_f using the /// algorithm implemented in the minimize_wdba() function, and presented  Alexandre Duret-Lutz committed Jan 05, 2011 101 102  /// by the following paper: ///  Alexandre Duret-Lutz committed Jun 09, 2013 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119  /** \verbatim @InProceedings{ dax.07.atva, author = {Christian Dax and Jochen Eisinger and Felix Klaedtke}, title = {Mechanizing the Powerset Construction for Restricted Classes of {$\omega$}-Automata}, year = 2007, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, volume = 4762, booktitle = {Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA'07)}, editor = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino and Yoshio Okamura}, month = oct } \endverbatim */  Alexandre Duret-Lutz committed Jan 05, 2011 120  ///  Alexandre Duret-Lutz committed Jan 05, 2011 121  /// Because it is hard to determine if an automaton corresponds  Alexandre Duret-Lutz committed Jan 05, 2011 122 123 124 125 126 127 128  /// to an obligation property, you should supply either the formula /// \a f expressed by the automaton \a aut_f, or \a aut_neg_f the negation /// of the automaton \a aut_neg_f. /// /// \param aut_f the automaton to minimize /// \param f the LTL formula represented by the automaton \a aut_f /// \param aut_neg_f an automaton representing the negation of \a aut_f  Alexandre Duret-Lutz committed Jun 09, 2013 129 130  /// \param reject_bigger Whether the minimal WDBA should be discarded if /// it has more states than the input.  Alexandre Duret-Lutz committed Jan 21, 2013 131 132  /// \return a new tgba if the automaton could be minimized, \a aut_f if /// the automaton cannot be minimized, 0 if we do not know if the  Alexandre Duret-Lutz committed Jan 05, 2011 133 134 135 136 137  /// minimization is correct because neither \a f nor \a aut_neg_f /// were supplied. /// /// The function proceeds as follows. If the formula \a f or the /// automaton \a aut can easily be proved to represent an obligation  Alexandre Duret-Lutz committed Jan 05, 2011 138 139 140 141 142 143 144  /// formula, then the result of minimize(aut) is /// returned. Otherwise, if \a aut_neg_f was not supplied but \a f /// was, \a aut_neg_f is built from the negation of \a f. Then we /// check that product(aut,!minimize(aut_f)) and /// product(aut_neg_f,minize(aut)) are both empty. If they /// are, the the minimization was sound. (See the paper for full /// details.)  Alexandre Duret-Lutz committed Aug 28, 2012 145 146 147 148 149 150 151  /// /// If \a reject_bigger is set, this function will return the input /// automaton \a aut_f when the minimized WDBA has more states than /// the input automaton. (More states are possible because of /// determinization step during minimize_wdba().) Note that /// checking the size of the minimized WDBA occurs before ensuring /// that the minimized WDBA is correct.  Alexandre Duret-Lutz committed Apr 22, 2015 152 153  SPOT_API twa_graph_ptr minimize_obligation(const const_twa_graph_ptr& aut_f,  Alexandre Duret-Lutz committed Sep 28, 2015 154  formula f = nullptr,  Alexandre Duret-Lutz committed Apr 22, 2015 155  const_twa_graph_ptr aut_neg_f = nullptr,  Alexandre Duret-Lutz committed Aug 15, 2014 156  bool reject_bigger = false);  Alexandre Duret-Lutz committed Jan 05, 2011 157  /// @}  Felix Abecassis committed Jan 05, 2011 158 }