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_input_tool.h
      10             : /// \brief Base class for tools that produce a (P)BES as output.
      11             : 
      12             : #ifndef MCRL2_PBES_PBES_INPUT_TOOL_H
      13             : #define MCRL2_PBES_PBES_INPUT_TOOL_H
      14             : 
      15             : #include "mcrl2/utilities/command_line_interface.h"
      16             : #include "mcrl2/pbes/io.h"
      17             : #include "mcrl2/pbes/io.h"
      18             : 
      19             : namespace mcrl2
      20             : {
      21             : 
      22             : namespace pbes_system
      23             : {
      24             : 
      25             : namespace tools
      26             : {
      27             : 
      28             : /// \brief Base class for filter tools that take a pbes as input.
      29             : /// \pre Tool provides input_filename()
      30             : template <typename Tool>
      31             : class pbes_input_tool: public Tool
      32             : {
      33             :   protected:
      34             : 
      35             :     /// \brief The type of the pbes input format
      36             :     utilities::file_format m_pbes_input_format;
      37             : 
      38             :     /// \brief Returns the file formats that are available for this tool.
      39             :     /// Override this method to change the standard behavior.
      40             :     /// \return The set { pbes, bes, pgsolver }
      41           0 :     virtual std::set<utilities::file_format> available_input_formats() const
      42             :     {
      43           0 :       std::set<utilities::file_format> result;
      44           0 :       result.insert(pbes_system::pbes_format_internal());
      45           0 :       result.insert(pbes_system::pbes_format_text());
      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 file format based on the extension of the input file, or if it is not possible to
      53             :     //          determine the file format in this way, pbes_format_internal() is returned. 
      54           0 :     virtual utilities::file_format default_input_format() const
      55             :     {
      56           0 :       utilities::file_format result = pbes_system::guess_format(Tool::input_filename());
      57           0 :       if (result == utilities::file_format())
      58             :       {
      59           0 :         result = pbes_system::guess_format(Tool::input_filename());
      60             :       }
      61           0 :       if (result == utilities::file_format())
      62             :       {
      63           0 :         result = pbes_system::pbes_format_internal();
      64             :       }
      65           0 :       return result;
      66           0 :     }
      67             : 
      68             :     /// \brief Add options to an interface description. Also includes
      69             :     /// input format options.
      70             :     /// \param desc An interface description
      71           0 :     void add_options(utilities::interface_description& desc)
      72             :     {
      73           0 :       Tool::add_options(desc);
      74           0 :       std::set<utilities::file_format> types = available_input_formats();
      75           0 :       auto option_argument = utilities::make_enum_argument<std::string>("FORMAT");
      76           0 :       for (const utilities::file_format& type: types)
      77             :       {
      78           0 :         option_argument.add_value_desc(type.shortname(), type.description(), type == default_input_format());
      79             :       }
      80           0 :       desc.add_option("in", option_argument, "use input format FORMAT:", 'i');
      81           0 :     }
      82             : 
      83             :     /// \brief Parse non-standard options
      84             :     /// \param parser A command line parser
      85           0 :     void parse_options(const utilities::command_line_parser& parser)
      86             :     {
      87           0 :       Tool::parse_options(parser);
      88           0 :       m_pbes_input_format = utilities::file_format();
      89           0 :       if(parser.options.count("in"))
      90             :       {
      91           0 :         std::set<utilities::file_format> types = available_input_formats();
      92           0 :         std::string arg = parser.option_argument_as<std::string>("in");
      93           0 :         for (const utilities::file_format& type: types)
      94             :         {
      95           0 :           if (type.shortname() == arg)
      96             :           {
      97           0 :             m_pbes_input_format = type;
      98             :           }
      99             :         }
     100           0 :         if (m_pbes_input_format == utilities::file_format())
     101             :         {
     102           0 :           mCRL2log(log::warning) << "Invalid input format given (" << arg << ").\n";
     103             :         }
     104           0 :       }
     105           0 :       if (m_pbes_input_format == utilities::file_format())
     106             :       {
     107           0 :         m_pbes_input_format = default_input_format();
     108           0 :         mCRL2log(log::verbose) << "Guessing input format: " << m_pbes_input_format.description()
     109           0 :                                << std::endl;
     110             :       }
     111           0 :     }
     112             : 
     113             : 
     114             :   public:
     115             :     /// \brief Constructor.
     116             :     /// \param name The name of the tool
     117             :     /// \param author The author(s) of the tool
     118             :     /// \param what_is One-line "what is" description of the tool
     119             :     /// \param tool_description The description of the tool
     120             :     /// \param known_issues Known issues with the tool
     121           0 :     pbes_input_tool(const std::string& name,
     122             :                        const std::string& author,
     123             :                        const std::string& what_is,
     124             :                        const std::string& tool_description,
     125             :                        std::string known_issues = ""
     126             :                       )
     127           0 :       : Tool(name, author, what_is, tool_description, known_issues)
     128           0 :     {}
     129             : 
     130             :     /// \brief Destructor.
     131           0 :     virtual ~pbes_input_tool() = default;
     132             : 
     133             :     /// \brief Returns the input file format
     134             :     /// \return The input format
     135           0 :     utilities::file_format pbes_input_format() const
     136             :     {
     137           0 :       return m_pbes_input_format;
     138             :     }
     139             : };
     140             : 
     141             : } // namespace tools
     142             : 
     143             : } // namespace pbes_system
     144             : 
     145             : } // namespace mcrl2
     146             : 
     147             : #endif // MCRL2_PBES_PBES_INPUT_TOOL_H