postproc.cc 5.02 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2012, 2013 Laboratoire de Recherche et 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
21
22
23
24
25

#include "postproc.hh"
#include "minimize.hh"
#include "simulation.hh"
#include "sccfilter.hh"
#include "degen.hh"
#include "stats.hh"
26
#include "stripacc.hh"
27
28
#include <cstdlib>
#include "misc/optionmap.hh"
29
30
31
32
33

namespace spot
{
  unsigned count_states(const tgba* a)
  {
34
35
36
37
38
39
40
41
    const sba_explicit_number* se =
      dynamic_cast<const sba_explicit_number*>(a);
    if (se)
      return se->num_states();
    const tgba_explicit_number* te =
      dynamic_cast<const tgba_explicit_number*>(a);
    if (te)
      return te->num_states();
42
43
44
45
    tgba_statistics st = stats_reachable(a);
    return st.states;
  }

46
47
  postprocessor::postprocessor(const option_map* opt)
    : type_(TGBA), pref_(Small), level_(High),
48
      degen_reset_(true), degen_order_(false), degen_cache_(true),
49
      simul_(-1), scc_filter_(-1), ba_simul_(-1)
50
51
52
  {
    if (opt)
      {
53
54
55
56
	degen_order_ = opt->get("degen-order", 0);
	degen_reset_ = opt->get("degen-reset", 1);
	degen_cache_ = opt->get("degen-lcache", 1);
	simul_ = opt->get("simul", -1);
57
	simul_limit_ = opt->get("simul-limit", -1);
58
	scc_filter_ = opt->get("scc-filter", -1);
59
	ba_simul_ = opt->get("ba-simul", -1);
60
61
62
      }
  }

63
  const tgba* postprocessor::do_simul(const tgba* a, int opt)
64
  {
65
    switch (opt)
66
67
68
69
70
71
72
73
74
75
      {
      case 0:
	return a;
      case 1:
	return simulation(a);
      case 2:
	return cosimulation(a);
      case 3:
      default:
	return iterated_simulations(a);
76
77
78
79
      case 4:
	return dont_care_simulation(a, simul_limit_);
      case 5:
	return dont_care_iterated_simulations(a, simul_limit_);
80
81
82
83
84
85
86
87
88
89
      }
  }

  const tgba* postprocessor::do_degen(const tgba* a)
  {
    const tgba* d = degeneralize(a,
				 degen_reset_,
				 degen_order_,
				 degen_cache_);
    delete a;
90
91
92
93
94
95
96
97
    if (ba_simul_ <= 0)
      return d;

    const tgba* s = do_simul(d, ba_simul_);
    if (s != d)
      delete d;

    return s;
98
99
  }

100
101
102
103
104
  const tgba* postprocessor::run(const tgba* a, const ltl::formula* f)
  {
    if (type_ == TGBA && pref_ == Any && level_ == Low)
      return a;

105
106
    if (simul_ < 0)
      simul_ = (level_ == Low) ? 1 : 3;
107
108
    if (ba_simul_ < 0)
      ba_simul_ = (level_ == High) ? 3 : 0;
109
110
    if (scc_filter_ < 0)
      scc_filter_ = 1;
111

112
    // Remove useless SCCs.
113
    if (scc_filter_ > 0 || type_ == Monitor)
114
    {
115
      const tgba* s = scc_filter(a, scc_filter_ > 1);
116
117
118
119
      delete a;
      a = s;
    }

120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
    if (type_ == Monitor)
      {
	if (pref_ == Deterministic)
	  {
	    const tgba* m = minimize_monitor(a);
	    delete a;
	    return m;
	  }
	else
	  {
	    const tgba* m = strip_acceptance(a);
	    delete a;
	    a = m;
	  }
	if (pref_ == Any)
	  return a;

137
	const tgba* sim = do_simul(a, simul_);
138
139
140
	if (a == sim)
	  // simulation was disabled.
	  return a;
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
	if (level_ != High)
	  {
	    delete a;
	    return sim;
	  }
	// For Small,High we return the smallest between the output of
	// the simulation, and that of the deterministic minimization.
	const tgba* m = minimize_monitor(a);
	delete a;
	if (count_states(m) > count_states(sim))
	  {
	    delete m;
	    return sim;
	  }
	else
	  {
	    delete sim;
	    return m;
	  }
      }

162
163
164
    if (pref_ == Any)
      {
	if (type_ == BA)
165
	  a = do_degen(a);
166
167
168
169
170
171
172
173
174
175
176
177
178
179
	return a;
      }

    const tgba* wdba = 0;
    const tgba* sim = 0;

    // (Small,Low) is the only configuration where we do not run
    // WDBA-minimization.
    if (pref_ != Small || level_ != Low)
      {
	bool reject_bigger = (pref_ == Small) && (level_ == Medium);
	wdba = minimize_obligation(a, f, 0, reject_bigger);
	if (wdba == a)	// Minimization failed.
	  wdba = 0;
180
	// The WDBA is a BA, so no degeneralization is required.
181
182
183
184
185
186
      }

    // Run a simulation when wdba failed (or was not run), or
    // at hard levels if we want a small output.
    if (!wdba || (level_ == High && pref_ == Small))
      {
187
188
189
190
	sim = do_simul(a, simul_);

	if (sim != a)
	  delete a;
191
192
193

	// Degeneralize the result of the simulation if needed.
	if (type_ == BA)
194
	  sim = do_degen(sim);
195
      }
196
197
198
199
    else
      {
	delete a;
      }
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214

    if (wdba && sim)
      {
	if (count_states(wdba) > count_states(sim))
	  {
	    delete wdba;
	    wdba = 0;
	  }
	else
	  {
	    delete sim;
	    sim = 0;
	  }
      }

215
    if (sim && type_ == TGBA && level_ == High && scc_filter_ != 0)
216
217
218
219
220
221
      {
	const tgba* s = scc_filter(sim, true);
	delete sim;
	return s;
      }

222
223
224
    return wdba ? wdba : sim;
  }
}