postproc.cc 4.74 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)
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 60 61
      }
  }

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

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

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

97 98
    if (simul_ < 0)
      simul_ = (level_ == Low) ? 1 : 3;
99 100
    if (scc_filter_ < 0)
      scc_filter_ = 1;
101

102
    // Remove useless SCCs.
103
    if (scc_filter_ > 0 || type_ == Monitor)
104
    {
105
      const tgba* s = scc_filter(a, scc_filter_ > 1);
106 107 108 109
      delete a;
      a = s;
    }

110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126
    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;

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

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

    // 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))
      {
177
	sim = do_simul(a);
178 179 180

	// Degeneralize the result of the simulation if needed.
	if (type_ == BA)
181
	  sim = do_degen(sim);
182 183
      }

184 185
    if (sim != a)
      delete a;
186 187 188 189 190 191 192 193 194 195 196 197 198 199 200

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

201
    if (sim && type_ == TGBA && level_ == High && scc_filter_ != 0)
202 203 204 205 206 207
      {
	const tgba* s = scc_filter(sim, true);
	delete sim;
	return s;
      }

208 209 210
    return wdba ? wdba : sim;
  }
}