Line data    Source code

       1             : // Author(s): Jan Friso Groote
       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/lps/linearisation_method.h
      10             : 
      11             : #ifndef MCRL2_LPS_LINEARISATION_METHOD_H
      12             : #define MCRL2_LPS_LINEARISATION_METHOD_H
      13             : 
      14             : #include "mcrl2/utilities/exception.h"
      15             : #include <string>
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : 
      20             : namespace lps
      21             : {
      22             : 
      23             : /// \brief The available linearisation methods
      24             : typedef enum { lmStack, lmRegular, lmRegular2 } t_lin_method;
      25             : 
      26             : /// \brief String representation of a linearisation method
      27             : /// \param[in] lin_method A linerisation method
      28             : /// \return String representation of \a lin_method
      29             : inline
      30          18 : std::string print_lin_method(const t_lin_method lin_method)
      31             : {
      32          18 :   switch(lin_method)
      33             :   {
      34           6 :     case lmStack: return "stack";
      35           9 :     case lmRegular: return "regular";
      36           3 :     case lmRegular2: return "regular2";
      37           0 :     default: throw mcrl2::runtime_error("unknown linearisation method");
      38             :   }
      39             : }
      40             : 
      41             : inline
      42             : std::string description(const t_lin_method lin_method)
      43             : {
      44             :   switch(lin_method)
      45             :   {
      46             :     case lmStack: return "for using stack data types (useful when 'regular' and 'regular2' do not work)";
      47             :     case lmRegular: return "for generating an LPS in regular form (specification should be regular)";
      48             :     case lmRegular2: return "for a variant of 'regular' that uses more data variables (useful when 'regular' does not work)";
      49             :     default: throw mcrl2::runtime_error("unknown linearisation method");
      50             :   }
      51             : }
      52             : 
      53             : /// \brief Parse a linearisation method
      54             : /// \param[in] s A string
      55             : /// \return The linearisation method represented by \a s
      56             : inline
      57             : t_lin_method parse_lin_method(const std::string& s)
      58             : {
      59             :   if(s == "stack")
      60             :   {
      61             :     return lmStack;
      62             :   }
      63             :   else if (s == "regular")
      64             :   {
      65             :     return lmRegular;
      66             :   }
      67             :   else if (s == "regular2")
      68             :   {
      69             :     return lmRegular2;
      70             :   }
      71             :   else
      72             :   {
      73             :     throw mcrl2::runtime_error("unknown linearisation strategy " + s);
      74             :   }
      75             : }
      76             : 
      77             : // \overload
      78             : inline
      79             : std::istream& operator>>(std::istream& is, t_lin_method& l)
      80             : {
      81             :   try {
      82             :     std::stringbuf buffer;
      83             :     is >> &buffer;
      84             :     l = parse_lin_method(buffer.str());
      85             :   }
      86             :   catch (mcrl2::runtime_error&)
      87             :   {
      88             :     is.setstate(std::ios_base::failbit);
      89             :   }
      90             : 
      91             :   return is;
      92             : }
      93             : 
      94             : // \overload
      95             : inline
      96          18 : std::ostream& operator<<(std::ostream& os, const t_lin_method l)
      97             : {
      98          18 :   os << print_lin_method(l);
      99          18 :   return os;
     100             : }
     101             : 
     102             : } // namespace lps
     103             : } // namespace mcrl2
     104             : 
     105             : #endif // MCRL2_LPS_LINEARISATION_METHOD_H