pbesrewr.h

Go to the documentation of this file.

// Author(s): Wieger Wesselink
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
 
#ifndef MCRL2_PBES_TOOLS_PBESREWR_H
#define MCRL2_PBES_TOOLS_PBESREWR_H
 
#include "mcrl2/data/detail/one_point_rule_preprocessor.h"
#include "mcrl2/pbes/detail/bqnf_traverser.h"
#include "mcrl2/pbes/detail/ppg_rewriter.h"
#include "mcrl2/pbes/detail/ppg_traverser.h"
#include "mcrl2/pbes/io.h"
#include "mcrl2/pbes/normalize.h"
#include "mcrl2/pbes/pbes_rewriter_type.h"
#include "mcrl2/pbes/rewrite.h"
#include "mcrl2/pbes/rewriter.h"
#include "mcrl2/pbes/rewriters/one_point_rule_rewriter.h"
#include "mcrl2/pbes/rewriters/quantifiers_inside_rewriter.h"
 
namespace mcrl2 {
 
namespace pbes_system {
 
void pbesrewr(const std::string& input_filename,
              const std::string& output_filename,
              const utilities::file_format& input_format,
              const utilities::file_format& output_format,
              const data::rewrite_strategy rewrite_strategy,
              pbes_rewriter_type rewriter_type)
{
  // load the pbes
  pbes p;
  load_pbes(p, input_filename, input_format);
 
  // data rewriter
  data::rewriter datar(p.data(), rewrite_strategy);
 
  // pbes rewriter
  switch (rewriter_type)
  {
    case simplify:
    {
      simplify_quantifiers_data_rewriter<data::rewriter> pbesr(datar);
      //simplify_data_rewriter<data::rewriter> pbesr(datar);
      pbes_rewrite(p, pbesr);
      break;
    }
    case quantifier_all:
    {
      bool enumerate_infinite_sorts = true;
      enumerate_quantifiers_rewriter pbesr(datar, p.data(), enumerate_infinite_sorts);
      pbes_rewrite(p, pbesr);
      break;
    }
    case quantifier_finite:
    {
      bool enumerate_infinite_sorts = false;
      enumerate_quantifiers_rewriter pbesr(datar, p.data(), enumerate_infinite_sorts);
      pbes_rewrite(p, pbesr);
      break;
    }
    case quantifier_inside:
    {
      quantifiers_inside_rewriter pbesr;
      pbes_rewrite(p, pbesr);
      break;
    }
    case quantifier_one_point:
    {
      // apply the one point rule rewriter
      one_point_rule_rewriter pbesr;
      bool innermost = false;
      replace_pbes_expressions(p, pbesr, innermost); // use replace, since the one point rule rewriter does the recursion itself
 
      // post processing: apply the simplifying rewriter
      simplify_data_rewriter<data::rewriter> simp(datar);
      pbes_rewrite(p, simp);
      break;
    }
    case pfnf:
    {
      pfnf_rewriter pbesr;
      pbes_system::normalize(p);
      pbes_rewrite(p, pbesr);
      break;
    }
    case ppg:
    {
      //bool bqnf = detail::is_bqnf(p);
      //std::clog << "bqnf_traverser says: p is " << (bqnf ? "" : "NOT ") << "in BQNF." << std::endl;
      bool ppg = detail::is_ppg(p);
      if (ppg)
      {
        mCRL2log(log::verbose) << "PBES is already a PPG." << std::endl;
      }
      else
      {
        mCRL2log(log::verbose) << "Rewriting..." << std::endl;
        pbes q = detail::to_ppg(p);
        mCRL2log(log::verbose) << "Rewriting done." << std::endl;
        ppg = detail::is_ppg(q);
        if (!ppg)
        {
          throw(std::runtime_error("The result PBES if not a PPG!"));
        }
        p = q;
      }
      break;
    }
    case bqnf_quantifier:
    {
      bqnf_rewriter pbesr;
      pbes_rewrite(p, pbesr);
      break;
    }
    case prover:
    default:
    {
      // Just ignore.
      assert(false);  // The PBES rewriter cannot be activated through
      // the commandline. So, we cannot end up here.
      break;
    }
  }
  save_pbes(p, output_filename, output_format);
}
 
} // namespace pbes_system
 
} // namespace mcrl2
 
#endif // MCRL2_PBES_TOOLS_PBESREWR_H