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: 76 82 92.7 %
Date: 2019-09-14 00:54:39 Functions: 11 11 100.0 %
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         111 : 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         226 :     states next_state(states state)
      50             :     {
      51         226 :       switch (state)
      52             :       {
      53             :         case PARAMETERS:
      54             :         {
      55         111 :           builder.write_parameters();
      56         111 :           return STATES;
      57             :         }
      58         111 :         case STATES: return TRANSITIONS;
      59           4 :         case TRANSITIONS: return INITIAL_DISTRIBUTION;
      60           0 :         default: throw mcrl2::runtime_error("unexpected split line --- encountered while parsing FSM!");
      61             :       }
      62             :     }
      63             : 
      64         168 :     std::vector<std::string> parse_domain_values(const std::string& text)
      65             :     {
      66         168 :       std::vector<std::string> result;
      67             : 
      68         336 :       boost::xpressive::sregex_token_iterator cur(text.begin(), text.end(), regex_quoted_string);
      69         336 :       boost::xpressive::sregex_token_iterator end;
      70         988 :       for (; cur != end; ++cur)
      71             :       {
      72         820 :         std::string value = *cur;
      73         410 :         if (value.size() > 0)
      74             :         {
      75         410 :           result.push_back(value.substr(1, value.size() - 2));
      76             :         }
      77             :       }
      78             : 
      79         336 :       return result;
      80             :     }
      81             : 
      82         168 :     void parse_parameter(const std::string& line)
      83             :     {
      84         336 :       std::string text = utilities::trim_copy(line);
      85         336 :       boost::xpressive::smatch what;
      86         168 :       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         336 :       std::string name = what[1];
      91         336 :       std::string cardinality = what[2];
      92         336 :       std::string sort = utilities::trim_copy(what[3]);
      93         336 :       std::vector<std::string> domain_values = parse_domain_values(what[4]);
      94         168 :       builder.add_parameter(name, cardinality, sort, domain_values);
      95         168 :     }
      96             : 
      97         764 :     void parse_state(const std::string& line)
      98             :     {
      99             :       try
     100             :       {
     101        1528 :         std::vector<std::size_t> values = utilities::parse_natural_number_sequence(line);
     102         764 :         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         764 :     }
     109             : 
     110        1595 :     void parse_transition(const std::string& line)
     111             :     {
     112        3190 :       std::string text = utilities::trim_copy(line);
     113        3190 :       boost::xpressive::smatch what;
     114        1595 :       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        3190 :       std::string source = what[1];
     119        3190 :       std::string target = what[3];
     120        3190 :       std::string label = what[5];
     121        1595 :       builder.add_transition(source, target, label);
     122        1595 :     }
     123             : 
     124           4 :     void parse_initial_distribution(const std::string& line)
     125             :     {
     126           8 :       std::string text = utilities::trim_copy(line);
     127           8 :       boost::xpressive::smatch what;
     128           4 :       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           4 :       builder.add_initial_distribution(what[0]);
     133           4 :     }
     134             : 
     135             :   public:
     136         111 :     simple_fsm_parser(probabilistic_lts_fsm_t& fsm)
     137         111 :       : 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         111 :       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         111 :       regex_transition = boost::xpressive::sregex::compile("(0|([1-9][0-9]*))+\\s+(0|([1-9][0-9]*|\\[[^\\]]*\\]))+\\s+\"([^\"]*)\"");
     152             : 
     153         111 :       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         111 :       regex_probabilistic_initial_distribution = boost::xpressive::sregex::compile("0|([1-9][0-9]*)|\\[[^\\]]*\\]");
     158         111 :     }
     159             : 
     160         111 :     void run(std::istream& from)
     161             :     {
     162         111 :       builder.start();
     163             : 
     164         111 :       states state = PARAMETERS;
     165         222 :       std::string line;
     166        5633 :       while (std::getline(from, line))
     167             :       {
     168             : 
     169        2761 :         utilities::trim(line);
     170        2761 :         if (line != "")  // This deals with the case when there are empty lines in or at the end of the file.
     171             :         { 
     172        2757 :           if (line == "---")
     173             :           {
     174         226 :             state = next_state(state);
     175             :           }
     176             :           else 
     177             :           { 
     178        2531 :             switch (state)
     179             :             {
     180         168 :               case PARAMETERS: { parse_parameter(line); break; }
     181         764 :               case STATES: { parse_state(line); break; }
     182        1595 :               case TRANSITIONS: { parse_transition(line); break; }
     183           4 :               case INITIAL_DISTRIBUTION: { parse_initial_distribution(line); break; }
     184             :             }
     185             :           }
     186             :         }
     187             :       }
     188         111 :       builder.finish();
     189         111 :     }
     190             : };
     191             : 
     192             : } // namespace detail
     193             : 
     194             : inline
     195         111 : void parse_fsm_specification(std::istream& from, probabilistic_lts_fsm_t& result)
     196             : {
     197         222 :   detail::simple_fsm_parser fsm_parser(result);
     198         111 :   fsm_parser.run(from);
     199         111 : }
     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