postproc.hh 7.24 KB
 Alexandre Duret-Lutz committed Sep 12, 2012 1 ``````// -*- coding: utf-8 -*- `````` Alexandre Duret-Lutz committed Oct 29, 2016 2 3 ``````// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche // et Développement de l'Epita (LRDE). `````` Alexandre Duret-Lutz committed Sep 12, 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 `````` Alexandre Duret-Lutz committed Sep 12, 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 . `````` Alexandre Duret-Lutz committed Sep 12, 2012 19 `````` `````` Etienne Renault committed Mar 23, 2015 20 ``````#pragma once `````` Alexandre Duret-Lutz committed Sep 12, 2012 21 `````` `````` Alexandre Duret-Lutz committed Dec 04, 2015 22 ``````#include `````` Alexandre Duret-Lutz committed Sep 12, 2012 23 24 25 `````` namespace spot { `````` Alexandre Duret-Lutz committed Apr 09, 2013 26 27 `````` class option_map; `````` Alexandre Duret-Lutz committed Apr 22, 2015 28 `````` /// \addtogroup twa_reduction `````` Alexandre Duret-Lutz committed Sep 12, 2012 29 30 `````` /// @{ `````` Alexandre Duret-Lutz committed Oct 21, 2012 31 32 `````` /// \brief Wrap TGBA/BA/Monitor post-processing algorithms in an /// easy interface. `````` Alexandre Duret-Lutz committed Sep 12, 2012 33 34 `````` /// /// This class is a shell around scc_filter(), `````` Alexandre Duret-Lutz committed Feb 12, 2016 35 36 37 38 39 `````` /// minimize_obligation(), simulation(), iterated_simulations(), /// degeneralize(), to_generalized_buchi() and tgba_determinize(). /// These different algorithms will be combined depending on the /// various options set with set_type(), set_pref(), and /// set_level(). `````` Alexandre Duret-Lutz committed Sep 12, 2012 40 41 42 43 44 45 `````` /// /// This helps hiding some of the logic required to combine these /// simplifications efficiently (e.g., there is no point calling /// degeneralize() or any simulation when minimize_obligation() /// succeeded.) /// `````` Alexandre Duret-Lutz committed Feb 12, 2016 46 47 48 `````` /// Use set_type() to select desired output type. /// /// Use the set_pref() method to specify whether you favor `````` Alexandre Duret-Lutz committed Sep 12, 2012 49 50 51 `````` /// deterministic automata or small automata. If you don't care, /// less post processing will be done. /// `````` Alexandre Duret-Lutz committed Apr 09, 2013 52 53 54 `````` /// The set_level() method lets you set the optimization level. /// A higher level enables more costly post-processings. For instance /// pref=Small,level=High will try two different post-processings `````` Alexandre Duret-Lutz committed Sep 12, 2012 55 56 57 58 59 60 `````` /// (one with minimize_obligation(), and one with /// iterated_simulations()) an keep the smallest result. /// pref=Small,level=Medium will only try the iterated_simulations() /// when minimized_obligation failed to produce an automaton smaller /// than its input. pref=Small,level=Low will only run /// simulation(). `````` Alexandre Duret-Lutz committed Feb 12, 2016 61 62 `````` /// /// `````` Alexandre Duret-Lutz committed Jul 29, 2013 63 `````` class SPOT_API postprocessor `````` Alexandre Duret-Lutz committed Sep 12, 2012 64 65 `````` { public: `````` Alexandre Duret-Lutz committed Apr 09, 2013 66 67 68 69 `````` /// \brief Construct a postprocessor. /// /// The \a opt argument can be used to pass extra fine-tuning /// options used for debugging or benchmarking. `````` Alexandre Duret-Lutz committed Sep 26, 2015 70 `````` postprocessor(const option_map* opt = nullptr); `````` Alexandre Duret-Lutz committed Sep 12, 2012 71 `````` `````` Alexandre Duret-Lutz committed Apr 02, 2015 72 `````` enum output_type { TGBA, BA, Monitor, Generic }; `````` Alexandre Duret-Lutz committed Feb 12, 2016 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 `````` /// \brief Select the desired output type. /// /// \c TGBA requires transition-based generalized Büchi acceptance /// while \c BA requests state-based Büchi acceptance. In both /// cases, automata with more complex acceptance conditions will /// be converted into these simpler acceptance. \c Monitor /// requests an automaton with the "all paths are accepting /// condition": this is less expressive, and may output automata /// that recognize a larger language than the input. Finally \c /// Generic remove all constraints about the acceptance condition. /// Using \c Generic can be needed to force the determinization of /// some automata (e.g., not all TGBA can be degeneralized, using /// \c Generic will allow parity acceptance to be used instead). /// /// If set_type() is not called, the default \c output_type is \c TGBA. `````` Alexandre Duret-Lutz committed Sep 12, 2012 89 90 91 92 93 94 `````` void set_type(output_type type) { type_ = type; } `````` Alexandre Duret-Lutz committed Sep 08, 2013 95 96 97 `````` enum { Any = 0, `````` Laurent XU committed Mar 10, 2016 98 99 `````` Small = 1, // Small and Deterministic Deterministic = 2, // are exclusive choices. `````` Alexandre Duret-Lutz committed May 14, 2015 100 `````` Complete = 4, `````` Laurent XU committed Mar 10, 2016 101 `````` SBAcc = 8, // State-based acceptance. `````` Alexandre Duret-Lutz committed May 15, 2015 102 `````` Unambiguous = 16, `````` Alexandre Duret-Lutz committed Sep 08, 2013 103 104 105 `````` }; typedef int output_pref; `````` Alexandre Duret-Lutz committed Feb 12, 2016 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 `````` /// \brief Select the desired characteristics of the output automaton. /// /// Use \c Any if you do not care about any feature of the output /// automaton: less processing will be done. /// /// \c Small and \c Deterministic are exclusive choices and indicate /// whether a smaller non-deterministic automaton should be preferred /// over a deterministic automaton. These are preferences. The \c Small /// option does not guarantee that the resulting automaton will be minimal. /// The \c Deterministic option may not manage to produce a deterministic /// automaton if the target acceptance set with set_type() is TGBA or BA /// (and even if such automaton exists). /// /// Use /// \code /// set_type(postprocessor::Generic); /// set_pref(postprocessor::Deterministic); /// \endcode /// if you absolutely want a deterministic automaton. /// /// The above options can be combined with \c Complete and \c /// SBAcc, to request a complete automaton, and an automaton with /// state-based acceptance. /// /// Note: the postprocessor::Unambiguous option is not actually /// supported by spot::postprocessor; it is only honored by /// spot::translator. /// /// If set_pref() is not called, the default \c output_type is \c Small. `````` Alexandre Duret-Lutz committed Sep 12, 2012 135 136 137 138 139 140 141 `````` void set_pref(output_pref pref) { pref_ = pref; } enum optimization_level { Low, Medium, High }; `````` Alexandre Duret-Lutz committed Feb 12, 2016 142 143 144 145 146 147 148 149 150 151 152 153 154 155 `````` /// \brief Set the optimization level /// /// At \c Low level, very few simplifications are performed on the /// automaton. Use this level if you need a result that matches /// the other constraints, but want it fast. /// /// At \c High level, several simplifications are chained, but /// also the result of different algorithms may be compared to /// pick the best result. This might be slow. /// /// At \c Medium level, several simplifications are chained, but /// only one such "pipeline" is used. /// /// If set_level() is not called, the default \c output_type is \c High. `````` Alexandre Duret-Lutz committed Sep 12, 2012 156 157 158 159 160 161 `````` void set_level(optimization_level level) { level_ = level; } `````` Alexandre Duret-Lutz committed Aug 15, 2014 162 163 164 165 `````` /// \brief Optimize an automaton. /// /// The returned automaton might be a new automaton, /// or an in-place modification of the \a input automaton. `````` Alexandre Duret-Lutz committed Oct 03, 2015 166 `````` twa_graph_ptr run(twa_graph_ptr input, formula f = nullptr); `````` Alexandre Duret-Lutz committed Sep 12, 2012 167 `````` `````` Alexandre Duret-Lutz committed Apr 09, 2013 168 `````` protected: `````` Alexandre Duret-Lutz committed Apr 22, 2015 169 `````` twa_graph_ptr do_simul(const twa_graph_ptr& input, int opt); `````` Alexandre Duret-Lutz committed May 14, 2015 170 `````` twa_graph_ptr do_sba_simul(const twa_graph_ptr& input, int opt); `````` Alexandre Duret-Lutz committed Apr 22, 2015 171 `````` twa_graph_ptr do_degen(const twa_graph_ptr& input); `````` Alexandre Duret-Lutz committed Oct 13, 2015 172 173 `````` twa_graph_ptr do_scc_filter(const twa_graph_ptr& a, bool arg); twa_graph_ptr do_scc_filter(const twa_graph_ptr& a); `````` Alexandre Duret-Lutz committed Apr 09, 2013 174 `````` `````` Alexandre Duret-Lutz committed Feb 12, 2016 175 176 177 `````` output_type type_ = TGBA; int pref_ = Small; optimization_level level_ = High; `````` Alexandre Duret-Lutz committed Apr 09, 2013 178 `````` // Fine-tuning options fetched from the option_map. `````` Alexandre Duret-Lutz committed Feb 12, 2016 179 180 `````` bool degen_reset_ = true; bool degen_order_ = false; `````` Alexandre Duret-Lutz committed Oct 29, 2016 181 `````` int degen_cache_ = 1; `````` Alexandre Duret-Lutz committed Feb 12, 2016 182 183 184 185 186 187 188 189 190 191 `````` bool degen_lskip_ = true; bool degen_lowinit_ = false; bool det_scc_ = true; bool det_simul_ = true; bool det_stutter_ = true; int simul_ = -1; int scc_filter_ = -1; int ba_simul_ = -1; bool tba_determinisation_ = false; int sat_minimize_ = 0; `````` Alexandre GBAGUIDI AISSE committed Jan 06, 2017 192 `````` int param_ = 0; `````` 193 `````` bool dicho_langmap_ = false; `````` Alexandre Duret-Lutz committed Feb 12, 2016 194 195 196 197 `````` int sat_acc_ = 0; int sat_states_ = 0; bool state_based_ = false; bool wdba_minimize_ = true; `````` Alexandre Duret-Lutz committed Sep 12, 2012 198 199 200 `````` }; /// @} }``````