postproc.cc 5.17 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 114 115 116 117 118 119 120 121 122 123 124 125 126
    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;
      }
127

128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144
    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;

145
	const tgba* sim = do_simul(a, simul_);
146 147 148
	if (a == sim)
	  // simulation was disabled.
	  return a;
149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169
	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;
	  }
      }

170 171 172
    if (pref_ == Any)
      {
	if (type_ == BA)
173
	  a = do_degen(a);
174 175 176 177 178 179 180 181 182 183 184 185 186 187
	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;
188
	// The WDBA is a BA, so no degeneralization is required.
189 190 191 192 193 194
      }

    // 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))
      {
195 196 197 198
	sim = do_simul(a, simul_);

	if (sim != a)
	  delete a;
199 200 201

	// Degeneralize the result of the simulation if needed.
	if (type_ == BA)
202
	  sim = do_degen(sim);
203
      }
204 205 206 207
    else
      {
	delete a;
      }
208 209 210 211 212 213 214 215 216 217 218 219 220 221 222

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

223
    if (sim && type_ == TGBA && level_ == High && scc_filter_ != 0)
224 225 226 227 228 229
      {
	const tgba* s = scc_filter(sim, true);
	delete sim;
	return s;
      }

230 231 232
    return wdba ? wdba : sim;
  }
}