LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts - parse.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 68 82 82.9 %
Date: 2019-06-26 00:32:26 Functions: 10 11 90.9 %
Legend: Lines: hit not hit

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

Generated by: LCOV version 1.12