lps_rewriter_tool.h

Go to the documentation of this file.

// Author(s): Jan Friso Groote (based on mcrl2/bes/pbes_rewriter_tool.h by 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_LPS_LPS_REWRITER_TOOL_H
#define MCRL2_LPS_LPS_REWRITER_TOOL_H
 
#include <set>
#include "mcrl2/utilities/command_line_interface.h"
#include "mcrl2/lps/lps_rewriter_type.h"
 
namespace mcrl2
{
 
namespace lps
{
 
namespace tools
{
 
template <typename Tool>
class lps_rewriter_tool: public Tool
{
  protected:
    lps::lps_rewriter_type m_lps_rewriter_type;
 
    virtual std::set<lps::lps_rewriter_type> available_rewriters() const
    {
      std::set<lps::lps_rewriter_type> result;
      result.insert(lps::simplify);
      result.insert(lps::quantifier_one_point);
      result.insert(lps::condition_one_point);
      return result;
    }
 
    virtual lps::lps_rewriter_type default_rewriter() const
    {
      return lps::simplify;
    }
 
    void add_options(utilities::interface_description& desc)
    {
      Tool::add_options(desc);
 
      utilities::interface_description::enum_argument<lps::lps_rewriter_type> arg(utilities::make_enum_argument<lps::lps_rewriter_type>("NAME"));
 
      // Compute the available rewriters, and add the approriate arguments
      for (const lps::lps_rewriter_type& type: available_rewriters())
      {
        arg.add_value(type, type==default_rewriter());
      }
 
      desc.add_option(
        "lps-rewriter",
        arg,
        "use lps rewrite strategy NAME:",
        'p'
      );
    }
 
    void parse_options(const utilities::command_line_parser& parser)
    {
      Tool::parse_options(parser);
      m_lps_rewriter_type = parser.option_argument_as<lps::lps_rewriter_type>("lps-rewriter");
    }
 
 
  public:
    lps_rewriter_tool(const std::string& name,
                       const std::string& author,
                       const std::string& what_is,
                       const std::string& tool_description,
                       std::string known_issues = ""
                      )
      : Tool(name, author, what_is, tool_description, known_issues)
    {}
 
    virtual ~lps_rewriter_tool() = default;
 
    lps::lps_rewriter_type rewriter_type() const
    {
      return m_lps_rewriter_type;
    }
};
 
} // namespace tools
 
} // namespace lps
 
} // namespace mcrl2
 
#endif // MCRL2_LPS_LPS_REWRITER_TOOL_H