spot  2.8.3
postproc.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2012-2019 Laboratoire de Recherche et Développement
3 // de l'Epita (LRDE).
4 //
5 // This file is part of Spot, a model checking library.
6 //
7 // Spot is free software; you can redistribute it and/or modify it
8 // under the terms of the GNU General Public License as published by
9 // the Free Software Foundation; either version 3 of the License, or
10 // (at your option) any later version.
11 //
12 // Spot is distributed in the hope that it will be useful, but WITHOUT
13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15 // License for more details.
16 //
17 // You should have received a copy of the GNU General Public License
18 // along with this program. If not, see <http://www.gnu.org/licenses/>.
19 
20 #pragma once
21 
22 #include <spot/twa/twagraph.hh>
23 
24 namespace spot
25 {
26  class option_map;
27 
30 
66  class SPOT_API postprocessor
67  {
68  public:
73  postprocessor(const option_map* opt = nullptr);
74 
75  enum output_type { TGBA = 0, // should be renamed GeneralizedBuchi
76  BA = 1, // should be renamed Buchi and not imply SBAcc
77  Monitor = 2,
78  Generic = 3,
79  Parity = 4,
80  ParityMin = Parity | 8,
81  ParityMax = Parity | 16,
82  ParityOdd = Parity | 32,
83  ParityEven = Parity | 64,
84  ParityMinOdd = ParityMin | ParityOdd,
85  ParityMaxOdd = ParityMax | ParityOdd,
86  ParityMinEven = ParityMin | ParityEven,
87  ParityMaxEven = ParityMax | ParityEven,
88  CoBuchi = 128,
89  };
90 
130  void
131  set_type(output_type type)
132  {
133  type_ = type;
134  }
135 
136  enum
137  {
138  Any = 0,
139  Small = 1, // Small and Deterministic
140  Deterministic = 2, // are exclusive choices.
141  Complete = 4,
142  SBAcc = 8, // State-based acceptance.
143  Unambiguous = 16,
144  Colored = 32, // Colored parity; requires parity acceptance
145  };
146  typedef int output_pref;
147 
188  void
189  set_pref(output_pref pref)
190  {
191  pref_ = pref;
192  }
193 
194  enum optimization_level { Low, Medium, High };
209  void
210  set_level(optimization_level level)
211  {
212  level_ = level;
213  }
214 
219  twa_graph_ptr run(twa_graph_ptr input, formula f = nullptr);
220 
221  protected:
222  twa_graph_ptr do_simul(const twa_graph_ptr& input, int opt) const;
223  twa_graph_ptr do_sba_simul(const twa_graph_ptr& input, int opt) const;
224  twa_graph_ptr do_degen(const twa_graph_ptr& input) const;
225  twa_graph_ptr do_degen_tba(const twa_graph_ptr& input) const;
226  twa_graph_ptr do_scc_filter(const twa_graph_ptr& a, bool arg) const;
227  twa_graph_ptr do_scc_filter(const twa_graph_ptr& a) const;
228  twa_graph_ptr finalize(twa_graph_ptr tmp) const;
229 
230  output_type type_ = TGBA;
231  int pref_ = Small;
232  optimization_level level_ = High;
233  // Fine-tuning options fetched from the option_map.
234  bool degen_reset_ = true;
235  bool degen_order_ = false;
236  int degen_cache_ = 1;
237  bool degen_lskip_ = true;
238  bool degen_lowinit_ = false;
239  bool degen_remscc_ = true;
240  bool det_scc_ = true;
241  bool det_simul_ = true;
242  bool det_stutter_ = true;
243  int det_max_states_ = -1;
244  int det_max_edges_ = -1;
245  int simul_ = -1;
246  int scc_filter_ = -1;
247  int ba_simul_ = -1;
248  bool tba_determinisation_ = false;
249  int sat_minimize_ = 0;
250  int sat_incr_steps_ = 0;
251  bool sat_langmap_ = false;
252  int sat_acc_ = 0;
253  int sat_states_ = 0;
254  bool state_based_ = false;
255  bool wdba_minimize_ = true;
256  };
258 }
Definition: automata.hh:26
Manage a map of options.
Definition: optionmap.hh:37
void set_level(optimization_level level)
Set the optimization level.
Definition: postproc.hh:210
Main class for temporal logic formula.
Definition: formula.hh:686
void set_type(output_type type)
Select the desired output type.
Definition: postproc.hh:131
void set_pref(output_pref pref)
Select the desired characteristics of the output automaton.
Definition: postproc.hh:189
Wrap TGBA/BA/Monitor post-processing algorithms in an easy interface.
Definition: postproc.hh:66

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.8.13