Line data    Source code

       1             : // Author(s): Wieger Wesselink
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : /// \file mcrl2/pbes/pbes_output_tool.h
      10             : /// \brief Base class for tools that produce a (P)BES as output.
      11             : 
      12             : #ifndef MCRL2_PBES_PBES_OUTPUT_TOOL_H
      13             : #define MCRL2_PBES_PBES_OUTPUT_TOOL_H
      14             : 
      15             : #include "mcrl2/utilities/command_line_interface.h"
      16             : #include "mcrl2/pbes/io.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : 
      21             : namespace pbes_system
      22             : {
      23             : 
      24             : namespace tools
      25             : {
      26             : 
      27             : /// \brief Base class for filter tools that produce a pbes as output.
      28             : /// \pre Tool provides output_filename()
      29             : template <typename Tool>
      30             : class pbes_output_tool: public Tool
      31             : {
      32             :   protected:
      33             : 
      34             :     /// \brief The type of the pbes output format
      35             :     utilities::file_format m_pbes_output_format;
      36             : 
      37             :     /// \brief Returns the file formats that are available for this tool.
      38             :     /// Override this method to change the standard behavior.
      39             :     /// \return The set { pbes, text }
      40           0 :     virtual std::set<utilities::file_format> available_output_formats() const
      41             :     {
      42           0 :       std::set<utilities::file_format> result;
      43           0 :       result.insert(pbes_system::pbes_format_internal());
      44           0 :       result.insert(pbes_system::pbes_format_text());
      45           0 :       result.insert(pbes_system::pbes_format_internal_bes());
      46           0 :       result.insert(pbes_system::pbes_format_pgsolver());
      47           0 :       return result;
      48           0 :     }
      49             : 
      50             :     /// \brief Returns the default file format.
      51             :     /// Override this method to change the standard behavior.
      52             :     /// \return The default format is determined based on the extension of the output file. 
      53             :     //          If this fails, pbes_format_internal() is returned. 
      54           0 :     virtual utilities::file_format default_output_format() const
      55             :     {
      56           0 :       utilities::file_format result= pbes_system::guess_format(Tool::output_filename());
      57           0 :       if (result == utilities::file_format())
      58             :       {
      59           0 :         result = pbes_system::pbes_format_internal();
      60             :       }
      61           0 :       return result;
      62           0 :     }
      63             : 
      64             :     /// \brief Add options to an interface description. Also includes
      65             :     /// output format options.
      66             :     /// \param desc An interface description
      67           0 :     void add_options(utilities::interface_description& desc)
      68             :     {
      69           0 :       Tool::add_options(desc);
      70           0 :       std::set<utilities::file_format> types = available_output_formats();
      71           0 :       auto option_argument = utilities::make_enum_argument<std::string>("FORMAT");
      72           0 :       for (const utilities::file_format& type: types)
      73             :       {
      74           0 :         option_argument.add_value_desc(type.shortname(), type.description(), type == default_output_format());
      75             :       }
      76           0 :       desc.add_option("out", option_argument, "use output format FORMAT:", 'o');
      77           0 :     }
      78             : 
      79             :     /// \brief Parse non-standard options
      80             :     /// \param parser A command line parser
      81           0 :     void parse_options(const utilities::command_line_parser& parser)
      82             :     {
      83           0 :       Tool::parse_options(parser);
      84           0 :       m_pbes_output_format = utilities::file_format();
      85           0 :       if(parser.options.count("out"))
      86             :       {
      87           0 :         std::set<utilities::file_format> types = available_output_formats();
      88           0 :         std::string arg = parser.option_argument_as<std::string>("out");
      89           0 :         for (const utilities::file_format& type: types)
      90             :         {
      91           0 :           if (type.shortname() == arg)
      92             :           {
      93           0 :             m_pbes_output_format = type;
      94             :           }
      95             :         }
      96           0 :         if (m_pbes_output_format == utilities::file_format())
      97             :         {
      98           0 :           mCRL2log(log::warning) << "Invalid input format given (" << arg << ").\n";
      99             :         }
     100           0 :       }
     101           0 :       if (m_pbes_output_format == utilities::file_format())
     102             :       {
     103           0 :         m_pbes_output_format = default_output_format();
     104           0 :         mCRL2log(log::verbose) << "Guessing output format: " << m_pbes_output_format.description()
     105           0 :                                << std::endl;
     106             :       }
     107           0 :     }
     108             : 
     109             : 
     110             :   public:
     111             :     /// \brief Constructor.
     112             :     /// \param name The name of the tool
     113             :     /// \param author The author(s) of the tool
     114             :     /// \param what_is One-line "what is" description of the tool
     115             :     /// \param tool_description The description of the tool
     116             :     /// \param known_issues Known issues with the tool
     117           0 :     pbes_output_tool(const std::string& name,
     118             :                      const std::string& author,
     119             :                      const std::string& what_is,
     120             :                      const std::string& tool_description,
     121             :                      std::string known_issues = "")
     122           0 :       : Tool(name, author, what_is, tool_description, known_issues)
     123           0 :     {}
     124             : 
     125             :     /// \brief Destructor.
     126           0 :     virtual ~pbes_output_tool() = default;
     127             : 
     128             :     /// \brief Returns the output format
     129             :     /// \return The output format
     130           0 :     utilities::file_format pbes_output_format() const
     131             :     {
     132           0 :       return m_pbes_output_format;
     133             :     }
     134             : };
     135             : 
     136             : } // namespace tools
     137             : 
     138             : } // namespace pbes_system
     139             : 
     140             : } // namespace mcrl2
     141             : 
     142             : #endif // MCRL2_PBES_PBES_OUTPUT_TOOL_H