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/lts/parse.h
      10             : /// \brief A simple straighforward parser for .fsm files.
      11             : 
      12             : #ifndef MCRL2_LTS_PARSE_H
      13             : #define MCRL2_LTS_PARSE_H
      14             : 
      15             : #include <regex>
      16             : #include "mcrl2/lts/detail/fsm_builder.h"
      17             : 
      18             : namespace mcrl2::lts {
      19             : 
      20             : namespace detail {
      21             : 
      22             : class simple_fsm_parser
      23             : {
      24             :   protected:
      25             :     enum states { PARAMETERS, STATES, TRANSITIONS, INITIAL_DISTRIBUTION };
      26             : 
      27             :     // Used for constructing an FSM
      28             :     detail::fsm_builder builder;
      29             : 
      30             :     const std::regex regex_parameter {"\\s*([a-zA-Z_][a-zA-Z0-9_'@]*)\\((\\d+)\\)\\s*([a-zA-Z_][a-zA-Z0-9_'@#\\-> \t=,\\(\\):]*)?\\s*((\"[^\"]*\"\\s*)*)"};
      31             : 
      32             :     // Probabilistic transitions can have one of the following two forms.
      33             :     //        in out "label"
      34             :     //        in [out1 prob1 ... out_n prob_n] "label"
      35             :     // where out is a state number of a state that can be reached with probability 1 in the first format, whereas
      36             :     // it is precisely indicated what the probabilities of the reachable states are in the second form.
      37             :     const std::regex regex_transition {"(0|([1-9][0-9]*))+\\s+(0|([1-9][0-9]*|\\[[^\\]]*\\]))+\\s+\"([^\"]*)\""};
      38             : 
      39             :     const std::regex regex_quoted_string {"\"([^\"]*)\""};
      40             : 
      41             :     // The initial state, is either a number or it has the shape [num1 prob1 ... num_n prob_n].
      42             :     const std::regex regex_probabilistic_initial_distribution {"0|([1-9][0-9]*)|\\[[^\\]]*\\]"};
      43             : 
      44         126 :     states next_state(states state)
      45             :     {
      46         126 :       switch (state)
      47             :       {
      48          61 :         case PARAMETERS:
      49             :         {
      50          61 :           builder.write_parameters();
      51          61 :           return STATES;
      52             :         }
      53          61 :         case STATES: return TRANSITIONS;
      54           4 :         case TRANSITIONS: return INITIAL_DISTRIBUTION;
      55           0 :         default: throw mcrl2::runtime_error("unexpected split line --- encountered while parsing FSM!");
      56             :       }
      57             :     }
      58             : 
      59          92 :     std::vector<std::string> parse_domain_values(const std::string& text)
      60             :     {
      61          92 :       std::vector<std::string> result;
      62             : 
      63          92 :       std::regex_token_iterator cur{text.begin(), text.end(), regex_quoted_string};
      64          92 :       std::regex_token_iterator<std::string::const_iterator> end;
      65         324 :       for (; cur != end; ++cur)
      66             :       {
      67         232 :         std::string value = cur->str();
      68         232 :         if (!value.empty())
      69             :         {
      70         232 :           result.push_back(value.substr(1, value.size() - 2));
      71             :         }
      72         232 :       }
      73             : 
      74         184 :       return result;
      75          92 :     }
      76             : 
      77          92 :     void parse_parameter(const std::string& line)
      78             :     {
      79          92 :       std::string text = utilities::trim_copy(line);
      80          92 :       std::smatch what;
      81          92 :       if (!std::regex_match(line, what, regex_parameter))
      82             :       {
      83           0 :         throw mcrl2::runtime_error("could not parse the following line as an FSM parameter: " + text);
      84             :       }
      85          92 :       std::string name = what[1];
      86          92 :       std::string cardinality = what[2];
      87          92 :       std::string sort = utilities::trim_copy(what[3]);
      88          92 :       std::vector<std::string> domain_values = parse_domain_values(what[4]);
      89          92 :       builder.add_parameter(name, cardinality, sort, domain_values);
      90          92 :     }
      91             : 
      92         414 :     void parse_state(const std::string& line)
      93             :     {
      94             :       try
      95             :       {
      96         414 :         std::vector<std::size_t> values = utilities::parse_natural_number_sequence(line);
      97         414 :         builder.add_state(values);
      98         414 :       }
      99           0 :       catch (mcrl2::runtime_error&)
     100             :       {
     101           0 :         throw mcrl2::runtime_error("could not parse the following line as an FSM state: " + line);
     102           0 :       }
     103         414 :     }
     104             : 
     105         837 :     void parse_transition(const std::string& line)
     106             :     {
     107         837 :       std::string text = utilities::trim_copy(line);
     108         837 :       std::smatch what;
     109         837 :       if (!std::regex_match(line, what, regex_transition))
     110             :       {
     111           0 :         throw mcrl2::runtime_error("could not parse the following line as an FSM transition: " + text);
     112             :       }
     113         837 :       std::string source = what[1];
     114         837 :       std::string target = what[3];
     115         837 :       std::string label = what[5];
     116         837 :       builder.add_transition(source, target, label);
     117         837 :     }
     118             : 
     119           4 :     void parse_initial_distribution(const std::string& line)
     120             :     {
     121           4 :       std::string text = utilities::trim_copy(line);
     122           4 :       std::smatch what;
     123           4 :       if (!std::regex_match(line, what, regex_probabilistic_initial_distribution))
     124             :       {
     125           0 :         throw mcrl2::runtime_error("Could not parse the following line as an initial distribution: " + line + ".");
     126             :       }
     127           4 :       builder.add_initial_distribution(what[0]);
     128           4 :     }
     129             : 
     130             :   public:
     131          61 :     explicit simple_fsm_parser(probabilistic_lts_fsm_t& fsm)
     132          61 :       : builder(fsm)
     133          61 :     {}
     134             : 
     135          61 :     void run(std::istream& from)
     136             :     {
     137          61 :       builder.start();
     138             : 
     139          61 :       states state = PARAMETERS;
     140          61 :       std::string line;
     141        1538 :       while (std::getline(from, line))
     142             :       {
     143        1477 :         utilities::trim(line);
     144        1477 :         if (!line.empty())  // This deals with the case when there are empty lines in or at the end of the file.
     145             :         { 
     146        1473 :           if (line == "---")
     147             :           {
     148         126 :             state = next_state(state);
     149             :           }
     150             :           else 
     151             :           { 
     152        1347 :             switch (state)
     153             :             {
     154          92 :               case PARAMETERS: { parse_parameter(line); break; }
     155         414 :               case STATES: { parse_state(line); break; }
     156         837 :               case TRANSITIONS: { parse_transition(line); break; }
     157           4 :               case INITIAL_DISTRIBUTION: { parse_initial_distribution(line); break; }
     158             :             }
     159             :           }
     160             :         }
     161             :       }
     162          61 :       builder.finish();
     163          61 :     }
     164             : };
     165             : 
     166             : } // namespace detail
     167             : 
     168             : inline
     169          61 : void parse_fsm_specification(std::istream& from, probabilistic_lts_fsm_t& result)
     170             : {
     171          61 :   detail::simple_fsm_parser fsm_parser(result);
     172          61 :   fsm_parser.run(from);
     173          61 : }
     174             : 
     175             : inline
     176           3 : void parse_fsm_specification(const std::string& text, probabilistic_lts_fsm_t& result)
     177             : {
     178           3 :   std::istringstream is(text);
     179           3 :   parse_fsm_specification(is, result);
     180           3 : }
     181             : 
     182             : } // namespace mcrl2::lts
     183             : 
     184             : #endif // MCRL2_LTS_PARSE_H