postproc.cc 4.53 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 49
      degen_reset_(true), degen_order_(false), degen_cache_(true),
      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 58 59
      }
  }

60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92
  const tgba* postprocessor::do_simul(const tgba* a)
  {
    // supported values for simul_:
    // 1 => direct simulation
    // 2 => reverse-simulation only
    // 3 => both simulations, iterated
    if (simul_ < 0)
      simul_ = (level_ == Low) ? 1 : 3;

    switch (simul_)
      {
      case 0:
	return a;
      case 1:
	return simulation(a);
      case 2:
	return cosimulation(a);
      case 3:
      default:
	return iterated_simulations(a);
      }
  }

  const tgba* postprocessor::do_degen(const tgba* a)
  {
    const tgba* d = degeneralize(a,
				 degen_reset_,
				 degen_order_,
				 degen_cache_);
    delete a;
    return d;
  }

93 94 95 96 97
  const tgba* postprocessor::run(const tgba* a, const ltl::formula* f)
  {
    if (type_ == TGBA && pref_ == Any && level_ == Low)
      return a;

98 99


100 101 102 103 104 105 106
    // Remove useless SCCs.
    {
      const tgba* s = scc_filter(a, false);
      delete a;
      a = s;
    }

107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123
    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;

124 125 126 127
	const tgba* sim = do_simul(a);
	if (a == sim)
	  // simulation was disabled.
	  return a;
128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148
	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;
	  }
      }

149 150 151
    if (pref_ == Any)
      {
	if (type_ == BA)
152
	  a = do_degen(a);
153 154 155 156 157 158 159 160 161 162 163 164 165 166
	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;
167
	// The WDBA is a BA, so no degeneralization is required.
168 169 170 171 172 173
      }

    // 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))
      {
174
	sim = do_simul(a);
175 176 177

	// Degeneralize the result of the simulation if needed.
	if (type_ == BA)
178
	  sim = do_degen(sim);
179 180
      }

181 182
    if (sim != a)
      delete a;
183 184 185 186 187 188 189 190 191 192 193 194 195 196 197

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

198 199 200 201 202 203 204
    if (sim && type_ == TGBA && level_ == High)
      {
	const tgba* s = scc_filter(sim, true);
	delete sim;
	return s;
      }

205 206 207
    return wdba ? wdba : sim;
  }
}