postproc.hh 3.93 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
3
// Développement de l'Epita (LRDE).
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
9
// the Free Software Foundation; either version 3 of the License, or
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
18
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
19

20
#pragma once
21

22
#include "tgba/tgbagraph.hh"
23
24
25

namespace spot
{
26
27
  class option_map;

28
29
30
  /// \addtogroup tgba_reduction
  /// @{

31
32
  /// \brief Wrap TGBA/BA/Monitor post-processing algorithms in an
  /// easy interface.
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
  ///
  /// This class is a shell around scc_filter(),
  /// minimize_obligation(), simulation(), iterated_simulations(), and
  /// degeneralize().  These different algorithms will be combined
  /// depending on the various options set with set_type(),
  /// set_pref(), and set_level().
  ///
  /// 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.)
  ///
  /// Use set_pref() method to specify whether you favor
  /// deterministic automata or small automata.  If you don't care,
  /// less post processing will be done.
  ///
49
50
51
  /// 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
52
53
54
55
56
57
  /// (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().
58
  class SPOT_API postprocessor
59
60
  {
  public:
61
62
63
64
65
    /// \brief Construct a postprocessor.
    ///
    /// The \a opt argument can be used to pass extra fine-tuning
    /// options used for debugging or benchmarking.
    postprocessor(const option_map* opt = 0);
66

67
    enum output_type { TGBA, BA, Monitor, Generic };
68
69
70
71
72
73
    void
    set_type(output_type type)
    {
      type_ = type;
    }

74
75
76
77
78
79
80
81
82
83
84
    enum
    {
      Any = 0,
      Small = 1,
      Deterministic = 2,
      // 3 reserved for unambiguous
      // Combine Complete as 'Small | Complete' or 'Deterministic | Complete'
      Complete = 4
    };
    typedef int output_pref;

85
86
87
88
89
90
91
92
93
94
95
96
97
    void
    set_pref(output_pref pref)
    {
      pref_ = pref;
    }

    enum optimization_level { Low, Medium, High };
    void
    set_level(optimization_level level)
    {
      level_ = level;
    }

98
99
100
101
102
103
    /// \brief Optimize an automaton.
    ///
    /// The returned automaton might be a new automaton,
    /// or an in-place modification of the \a input automaton.
    tgba_digraph_ptr run(tgba_digraph_ptr input,
			 const ltl::formula* f);
104

105
  protected:
106
107
108
    tgba_digraph_ptr do_simul(const tgba_digraph_ptr& input, int opt);
    tgba_digraph_ptr do_ba_simul(const tgba_digraph_ptr& input, int opt);
    tgba_digraph_ptr do_degen(const tgba_digraph_ptr& input);
109

110
    output_type type_;
111
    int pref_;
112
    optimization_level level_;
113
114
115
    // Fine-tuning options fetched from the option_map.
    bool degen_reset_;
    bool degen_order_;
116
117
    int degen_cache_;
    bool degen_lskip_;
118
    bool degen_lowinit_;
119
    int simul_;
120
    int scc_filter_;
121
    int ba_simul_;
122
    bool tba_determinisation_;
123
124
125
    int sat_minimize_;
    int sat_acc_;
    int sat_states_;
126
    bool state_based_;
127
    bool wdba_minimize_;
128
129
130
  };
  /// @}
}