postproc.cc 4.11 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 48 49 50 51 52 53 54 55 56 57
  postprocessor::postprocessor(const option_map* opt)
    : type_(TGBA), pref_(Small), level_(High),
      degen_reset(true), degen_order(false), degen_cache(true)
  {
    if (opt)
      {
	degen_order = opt->get("degen-order", 0);
	degen_reset = opt->get("degen-reset", 1);
	degen_cache = opt->get("degen-lcache", 1);
      }
  }

58 59 60 61 62 63 64 65 66 67 68 69
  const tgba* postprocessor::run(const tgba* a, const ltl::formula* f)
  {
    if (type_ == TGBA && pref_ == Any && level_ == Low)
      return a;

    // Remove useless SCCs.
    {
      const tgba* s = scc_filter(a, false);
      delete a;
      a = s;
    }

70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112
    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;

	const tgba* sim;
	if (level_ == Low)
	  sim = simulation(a);
	else
	  sim = iterated_simulations(a);
	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;
	  }
      }

113 114 115 116
    if (pref_ == Any)
      {
	if (type_ == BA)
	  {
117 118 119 120
	    const tgba* d = degeneralize(a,
					 degen_reset,
					 degen_order,
					 degen_cache);
121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152
	    delete a;
	    a = d;
	  }
	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;
	// The WDBA is a BA, so no degeneralization required.
      }

    // 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))
      {
	if (level_ == Low)
	  sim = simulation(a);
	else
	  sim = iterated_simulations(a);

	// Degeneralize the result of the simulation if needed.
	if (type_ == BA)
	  {
153 154 155 156
	    const tgba* d = degeneralize(sim,
					 degen_reset,
					 degen_order,
					 degen_cache);
157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177
	    delete sim;
	    sim = d;
	  }
      }

    delete a;

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

178 179 180 181 182 183 184
    if (sim && type_ == TGBA && level_ == High)
      {
	const tgba* s = scc_filter(sim, true);
	delete sim;
	return s;
      }

185 186 187
    return wdba ? wdba : sim;
  }
}