postproc.cc 2.79 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 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 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119
// -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
//
// 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
// the Free Software Foundation; either version 2 of the License, or
// (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
// along with Spot; see the file COPYING.  If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.

#include "postproc.hh"
#include "minimize.hh"
#include "simulation.hh"
#include "sccfilter.hh"
#include "degen.hh"
#include "stats.hh"

namespace spot
{
  unsigned count_states(const tgba* a)
  {
    // FIXME: the number of states can be found more
    // efficiently in explicit automata.
    tgba_statistics st = stats_reachable(a);
    return st.states;
  }

  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;
    }

    if (pref_ == Any)
      {
	if (type_ == BA)
	  {
	    const tgba* d = degeneralize(a);
	    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)
	  {
	    const tgba* d = degeneralize(sim);
	    delete sim;
	    sim = d;
	  }
      }

    delete a;

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

	    if (type_ == TGBA && level_ == High)
	      {
		const tgba* s = scc_filter(sim, true);
		delete sim;
		sim = s;
	      }
	  }
	else
	  {
	    delete sim;
	    sim = 0;
	  }
      }

    return wdba ? wdba : sim;
  }
}