mCRL2
Loading...
Searching...
No Matches
parse.h
Go to the documentation of this file.
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//
11
12#ifndef MCRL2_LTS_PARSE_H
13#define MCRL2_LTS_PARSE_H
14
15#include <regex>
17
18namespace mcrl2::lts {
19
20namespace detail {
21
23{
24 protected:
26
27 // Used for constructing an FSM
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
45 {
46 switch (state)
47 {
48 case PARAMETERS:
49 {
50 builder.write_parameters();
51 return STATES;
52 }
53 case STATES: return TRANSITIONS;
55 default: throw mcrl2::runtime_error("unexpected split line --- encountered while parsing FSM!");
56 }
57 }
58
59 std::vector<std::string> parse_domain_values(const std::string& text)
60 {
61 std::vector<std::string> result;
62
63 std::regex_token_iterator cur{text.begin(), text.end(), regex_quoted_string};
64 std::regex_token_iterator<std::string::const_iterator> end;
65 for (; cur != end; ++cur)
66 {
67 std::string value = cur->str();
68 if (!value.empty())
69 {
70 result.push_back(value.substr(1, value.size() - 2));
71 }
72 }
73
74 return result;
75 }
76
77 void parse_parameter(const std::string& line)
78 {
79 std::string text = utilities::trim_copy(line);
80 std::smatch what;
81 if (!std::regex_match(line, what, regex_parameter))
82 {
83 throw mcrl2::runtime_error("could not parse the following line as an FSM parameter: " + text);
84 }
85 std::string name = what[1];
86 std::string cardinality = what[2];
87 std::string sort = utilities::trim_copy(what[3]);
88 std::vector<std::string> domain_values = parse_domain_values(what[4]);
89 builder.add_parameter(name, cardinality, sort, domain_values);
90 }
91
92 void parse_state(const std::string& line)
93 {
94 try
95 {
96 std::vector<std::size_t> values = utilities::parse_natural_number_sequence(line);
97 builder.add_state(values);
98 }
100 {
101 throw mcrl2::runtime_error("could not parse the following line as an FSM state: " + line);
102 }
103 }
104
105 void parse_transition(const std::string& line)
106 {
107 std::string text = utilities::trim_copy(line);
108 std::smatch what;
109 if (!std::regex_match(line, what, regex_transition))
110 {
111 throw mcrl2::runtime_error("could not parse the following line as an FSM transition: " + text);
112 }
113 std::string source = what[1];
114 std::string target = what[3];
115 std::string label = what[5];
116 builder.add_transition(source, target, label);
117 }
118
119 void parse_initial_distribution(const std::string& line)
120 {
121 std::string text = utilities::trim_copy(line);
122 std::smatch what;
123 if (!std::regex_match(line, what, regex_probabilistic_initial_distribution))
124 {
125 throw mcrl2::runtime_error("Could not parse the following line as an initial distribution: " + line + ".");
126 }
127 builder.add_initial_distribution(what[0]);
128 }
129
130 public:
132 : builder(fsm)
133 {}
134
135 void run(std::istream& from)
136 {
137 builder.start();
138
140 std::string line;
141 while (std::getline(from, line))
142 {
143 utilities::trim(line);
144 if (!line.empty()) // This deals with the case when there are empty lines in or at the end of the file.
145 {
146 if (line == "---")
147 {
149 }
150 else
151 {
152 switch (state)
153 {
154 case PARAMETERS: { parse_parameter(line); break; }
155 case STATES: { parse_state(line); break; }
156 case TRANSITIONS: { parse_transition(line); break; }
158 }
159 }
160 }
161 }
162 builder.finish();
163 }
164};
165
166} // namespace detail
167
168inline
170{
171 detail::simple_fsm_parser fsm_parser(result);
172 fsm_parser.run(from);
173}
174
175inline
176void parse_fsm_specification(const std::string& text, probabilistic_lts_fsm_t& result)
177{
178 std::istringstream is(text);
179 parse_fsm_specification(is, result);
180}
181
182} // namespace mcrl2::lts
183
184#endif // MCRL2_LTS_PARSE_H
Read-only balanced binary tree of terms.
std::vector< std::string > parse_domain_values(const std::string &text)
Definition parse.h:59
void run(std::istream &from)
Definition parse.h:135
void parse_parameter(const std::string &line)
Definition parse.h:77
states next_state(states state)
Definition parse.h:44
const std::regex regex_quoted_string
Definition parse.h:39
void parse_state(const std::string &line)
Definition parse.h:92
const std::regex regex_parameter
Definition parse.h:30
simple_fsm_parser(probabilistic_lts_fsm_t &fsm)
Definition parse.h:131
const std::regex regex_transition
Definition parse.h:37
void parse_initial_distribution(const std::string &line)
Definition parse.h:119
detail::fsm_builder builder
Definition parse.h:28
void parse_transition(const std::string &line)
Definition parse.h:105
const std::regex regex_probabilistic_initial_distribution
Definition parse.h:42
The class lts_fsm_t contains labelled transition systems in .fsm format.
Definition lts_fsm.h:276
Standard exception class for reporting runtime errors.
Definition exception.h:27
The code in this file is used to construct an lts in fsm format.
The main LTS namespace.
void parse_fsm_specification(std::istream &from, probabilistic_lts_fsm_t &result)
Definition parse.h:169
std::size_t label(const outgoing_pair_t &p)
Label of a pair of a label and target state.
std::size_t from(const outgoing_transitions_per_state_action_t::const_iterator &i)
From state of an iterator exploring transitions per outgoing state and action.
void trim(std::string &text)
Remove all trailing and leading spaces from the input.
std::string trim_copy(const std::string &text)
Remove all trailing and leading spaces from the input.
std::vector< std::size_t > parse_natural_number_sequence(const std::string &text)
Parses a sequence of natural numbers (separated by spaces) from a string.