spot/src/ltlvisit/snf.cc

// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et
// Developpement 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 3 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 this program.  If not, see <http://www.gnu.org/licenses/>.

#include "snf.hh"

namespace spot
{
  namespace ltl
  {
    namespace
    {
      // E°  if bounded=false
      // E^□ if nounded=true
      template<bool bounded>
      class snf_visitor
      {
      protected:
	formula result_;
	snf_cache* cache_;
      public:
	snf_visitor(snf_cache* c)
	  : cache_(c)
	{
	}

	formula visit(formula f)
	{
	  if (!f.accepts_eword())
	    return f;

	  snf_cache::const_iterator i = cache_->find(f);
	  if (i != cache_->end())
	    return i->second;

	  formula out;
	  switch (f.kind())
	    {
	    case op::EmptyWord:
	      out = formula::ff();
	      break;
	    case op::Star:
	      if (!bounded)
		out = visit(f.nth(0)); // Strip the star.
	      else
		out = formula::Star(visit(f.nth(0)),
				    std::max(unsigned(f.min()), 1U), f.max());
	      break;
	    case op::Concat:
	      if (bounded)
		{
		  out = f;
		  break;
		}
	      // Fall through
	    case op::OrRat:
	    case op::AndNLM:
	      // Let F designate expressions that accept [*0],
	      // and G designate expressions that do not.

	      // (G₁;G₂;G₃)° = G₁;G₂;G₃
	      // (G₁;F₂;G₃)° = (G₁°);F₂;(G₃°) = G₁;F₂;G₃
	      // because there is nothing to do recursively on a G.
	      //
	      // AndNLM can be dealt with similarly.
	      //
	      // The above cases are already handled by the
	      // accepts_eword() tests at the top of this method.  So
	      // we reach this switch, we only have to deal with...
	      //
	      // (F₁;F₂;F₃)° = (F₁°)|(F₂°)|(F₃°)
	      // (F₁&F₂&F₃)° = (F₁°)|(F₂°)|(F₃°)
	      // (F₁|G₂|F₃)° = (F₁°)|(G₂°)|(F₃°)
	      {
		unsigned s = f.size();
		std::vector<formula> v;
		v.reserve(s);
		for (unsigned pos = 0; pos < s; ++pos)
		  v.emplace_back(visit(f.nth(pos)));
		out = formula::OrRat(v);
		break;
	      }
	    case op::False:
	    case op::True:
	    case op::AP:
	    case op::Not:
	    case op::X:
	    case op::F:
	    case op::G:
	    case op::Closure:
	    case op::NegClosure:
	    case op::NegClosureMarked:
	    case op::Xor:
	    case op::Implies:
	    case op::Equiv:
	    case op::U:
	    case op::R:
	    case op::W:
	    case op::M:
	    case op::EConcat:
	    case op::EConcatMarked:
	    case op::UConcat:
	    case op::Fusion:
	    case op::Or:
	    case op::And:
	      SPOT_UNREACHABLE();
	    case op::AndRat:	// Can AndRat be handled better?
	    case op::FStar:	// Can FStar be handled better?
	      out = f;
	      break;
	    }

	  return (*cache_)[f] = out;
	}
      };
    }


    formula
    star_normal_form(formula sere, snf_cache* cache)
    {
      snf_visitor<false> v(cache);
      return v.visit(sere);
    }

    formula
    star_normal_form_bounded(formula sere, snf_cache* cache)
    {
      snf_visitor<true> v(cache);
      return v.visit(sere);
    }

  }
}