postproc.cc 5.44 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 90 91 92 93 94 95 96 97 98 99
  const tgba* postprocessor::do_ba_simul(const tgba* a, int opt)
  {
    switch (opt)
      {
      case 0:
	return a;
      case 1:
	return simulation_sba(a);
      case 2:
	return cosimulation_sba(a);
      case 3:
      default:
	return iterated_simulations_sba(a);
      }
  }


100 101 102 103 104 105 106
  const tgba* postprocessor::do_degen(const tgba* a)
  {
    const tgba* d = degeneralize(a,
				 degen_reset_,
				 degen_order_,
				 degen_cache_);
    delete a;
107 108 109
    if (ba_simul_ <= 0)
      return d;

110
    const tgba* s = do_ba_simul(d, ba_simul_);
111 112 113 114
    if (s != d)
      delete d;

    return s;
115 116
  }

117 118 119 120 121
  const tgba* postprocessor::run(const tgba* a, const ltl::formula* f)
  {
    if (type_ == TGBA && pref_ == Any && level_ == Low)
      return a;

122 123
    if (simul_ < 0)
      simul_ = (level_ == Low) ? 1 : 3;
124 125
    if (ba_simul_ < 0)
      ba_simul_ = (level_ == High) ? 3 : 0;
126 127
    if (scc_filter_ < 0)
      scc_filter_ = 1;
128

129
    // Remove useless SCCs.
130 131 132 133 134 135 136 137 138 139 140 141 142 143
    if (type_ == Monitor)
      {
	// Do not bother about acceptance conditions, they we be
	// ignored.
	const tgba* s = scc_filter_states(a);
	delete a;
	a = s;
      }
    else if (scc_filter_ > 0)
      {
	const tgba* s = scc_filter(a, scc_filter_ > 1);
	delete a;
	a = s;
      }
144

145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161
    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;

162
	const tgba* sim = do_simul(a, simul_);
163 164 165
	if (a == sim)
	  // simulation was disabled.
	  return a;
166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186
	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;
	  }
      }

187 188 189
    if (pref_ == Any)
      {
	if (type_ == BA)
190
	  a = do_degen(a);
191 192 193 194 195 196 197 198 199 200 201 202 203 204
	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;
205
	// The WDBA is a BA, so no degeneralization is required.
206 207 208 209 210 211
      }

    // 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))
      {
212 213 214 215
	sim = do_simul(a, simul_);

	if (sim != a)
	  delete a;
216 217 218

	// Degeneralize the result of the simulation if needed.
	if (type_ == BA)
219
	  sim = do_degen(sim);
220
      }
221 222 223 224
    else
      {
	delete a;
      }
225 226 227 228 229 230 231 232 233 234 235 236 237 238 239

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

240
    if (sim && type_ == TGBA && level_ == High && scc_filter_ != 0)
241 242 243 244 245 246
      {
	const tgba* s = scc_filter(sim, true);
	delete sim;
	return s;
      }

247 248 249
    return wdba ? wdba : sim;
  }
}