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/detail/fsm_builder.h
10 : /// \brief The code in this file is used to construct an lts in fsm format.
11 :
12 : #ifndef MCRL2_LTS_DETAIL_FSM_BUILDER_H
13 : #define MCRL2_LTS_DETAIL_FSM_BUILDER_H
14 :
15 : #include <map>
16 : #include "mcrl2/lts/lts_fsm.h"
17 : #include "mcrl2/utilities/parse_numbers.h"
18 :
19 : namespace mcrl2::lts::detail {
20 :
21 : // Read a numeric value before a symbol c1 or c2, and remove it from s, including the symbol.
22 336 : inline std::string split_string_until(std::string& s, const std::string& c1, const std::string& c2="")
23 : {
24 336 : std::size_t n=s.find(c1);
25 336 : if (!c2.empty())
26 : {
27 112 : n=std::min(n,s.find(c2));
28 : }
29 336 : if (n==std::string::npos)
30 : {
31 0 : if (c2.empty())
32 : {
33 0 : throw mcrl2::runtime_error("Expect '" + c1 + "' in distribution " + s + ".");
34 : }
35 : else
36 : {
37 0 : throw mcrl2::runtime_error("Expect either '" + c1 + "' or '" + c2 + " in distribution " + s + ".");
38 : }
39 : }
40 336 : std::string result=s.substr(0,n);
41 336 : s=s.substr(n+1);
42 672 : return result;
43 0 : }
44 :
45 841 : inline lts_fsm_base::probabilistic_state parse_distribution(const std::string& distribution)
46 : {
47 841 : if (distribution.find('[')==std::string::npos) // So the distribution must consist of a state index.
48 : {
49 785 : std::size_t state_number=utilities::parse_natural_number(distribution);
50 785 : if (state_number==0)
51 : {
52 0 : throw mcrl2::runtime_error("Transition has a zero as target state number.");
53 : }
54 785 : return lts_fsm_base::probabilistic_state(state_number-1);
55 : }
56 :
57 : // Otherwise the distribution has the shape [state1 enumerator1/denominator1 ... staten enumeratorn/denominatorn]
58 56 : std::vector<lts_fsm_base::state_probability_pair> result;
59 56 : std::string s = utilities::trim_copy(distribution);
60 56 : if (s.substr(0,1) != "[")
61 : {
62 0 : throw mcrl2::runtime_error("Distribution does not start with ']': " + distribution + ".");
63 : }
64 56 : s = s.substr(1); // Remove initial "[";
65 168 : for(; s.size() > 1; s = utilities::trim_copy(s))
66 : {
67 112 : std::size_t state_number = utilities::parse_natural_number(split_string_until(s," "));
68 112 : if (state_number == 0)
69 : {
70 0 : throw mcrl2::runtime_error("Transition has a zero as target state number.");
71 : }
72 224 : std::string enumerator = split_string_until(s,"/");
73 224 : std::string denominator = split_string_until(s," ","]");
74 112 : result.emplace_back(state_number - 1, probabilistic_arbitrary_precision_fraction(enumerator,denominator));
75 112 : }
76 56 : return lts_fsm_base::probabilistic_state(result.begin(), result.end());
77 56 : }
78 :
79 : class fsm_parameter
80 : {
81 : protected:
82 : std::string m_name;
83 : std::size_t m_cardinality;
84 : std::string m_sort;
85 : std::vector<std::string> m_values;
86 :
87 : public:
88 92 : fsm_parameter(const std::string& name, const std::string& cardinality, const std::string& sort, const std::vector<std::string>& values)
89 92 : : m_name(name),
90 92 : m_cardinality(utilities::parse_natural_number(cardinality)),
91 92 : m_sort(sort),
92 92 : m_values(values)
93 92 : {}
94 :
95 92 : const std::string& name() const
96 : {
97 92 : return m_name;
98 : }
99 :
100 : std::string& name()
101 : {
102 : return m_name;
103 : }
104 :
105 92 : const std::string& sort() const
106 : {
107 92 : return m_sort;
108 : }
109 :
110 : std::string& sort()
111 : {
112 : return m_sort;
113 : }
114 :
115 : // If the cardinality is zero, the sort and the values are ignored in the FSM.
116 92 : std::size_t cardinality() const
117 : {
118 92 : return m_cardinality;
119 : }
120 :
121 : std::size_t& cardinality()
122 : {
123 : return m_cardinality;
124 : }
125 :
126 92 : const std::vector<std::string>& values() const
127 : {
128 92 : return m_values;
129 : }
130 :
131 : std::vector<std::string>& values()
132 : {
133 : return m_values;
134 : }
135 : };
136 :
137 : /// \brief Transitions in an FSM
138 : ///
139 : /// \note All state numbers in an FSM file are larger or equal to 1. When reading one is subtracted.
140 : class fsm_transition
141 : {
142 : protected:
143 : std::size_t m_source;
144 : detail::lts_fsm_base::probabilistic_state m_target;
145 : std::string m_label;
146 :
147 : public:
148 : fsm_transition(std::size_t source, std::size_t target, const std::string& label)
149 : : m_source(source - 1),
150 : m_target(detail::lts_fsm_base::probabilistic_state(target - 1)),
151 : m_label(label)
152 : {
153 : if (source == 0 || target == 0)
154 : {
155 : throw mcrl2::runtime_error("A transition contains a state with state number 0.");
156 : }
157 : }
158 :
159 837 : fsm_transition(const std::string& source_text, const std::string& target_text, const std::string& label)
160 837 : : m_label(label)
161 : {
162 837 : std::size_t source = utilities::parse_natural_number(source_text);
163 837 : if (source == 0)
164 : {
165 0 : throw mcrl2::runtime_error("A transition constains a source state with number 0.");
166 : }
167 837 : m_source = source - 1;
168 837 : m_target = parse_distribution(target_text);
169 837 : }
170 :
171 : std::size_t source() const
172 : {
173 : return m_source;
174 : }
175 :
176 1674 : std::size_t& source()
177 : {
178 1674 : return m_source;
179 : }
180 :
181 : const lts_fsm_base::probabilistic_state& target() const
182 : {
183 : return m_target;
184 : }
185 :
186 1674 : lts_fsm_base::probabilistic_state& target()
187 : {
188 1674 : return m_target;
189 : }
190 :
191 : const std::string& label() const
192 : {
193 : return m_label;
194 : }
195 :
196 2211 : std::string& label()
197 : {
198 2211 : return m_label;
199 : }
200 : };
201 :
202 : struct fsm_builder
203 : {
204 61 : explicit fsm_builder(probabilistic_lts_fsm_t& fsm_)
205 61 : : fsm(fsm_),
206 61 : m_initial_state_is_set(false)
207 61 : {}
208 :
209 : // Contains the result
210 : probabilistic_lts_fsm_t& fsm;
211 :
212 : // The parameters of the FSM
213 : std::vector<fsm_parameter> parameters;
214 :
215 : // Maps labels of the FSM to numbers
216 : std::map<std::string, std::size_t> labels;
217 :
218 : // This variable records if the initial state is set explicitly.
219 : // If not it needs to be done while finishing the fsm.
220 : bool m_initial_state_is_set;
221 :
222 61 : void start()
223 : {
224 61 : parameters.clear();
225 61 : labels.clear();
226 61 : labels[action_label_string::tau_action()] = 0; // The label 0 is the tau action by default.
227 61 : fsm.clear();
228 61 : }
229 :
230 841 : std::size_t find_maximal_state_index(const lts_fsm_base::probabilistic_state& distribution)
231 : {
232 841 : std::size_t max = 0;
233 841 : if (distribution.size()>1)
234 : {
235 168 : for (const detail::lts_fsm_base::state_probability_pair& p: distribution)
236 : {
237 112 : max = std::max(max, p.state());
238 : }
239 : }
240 : else
241 : {
242 785 : max=distribution.get();
243 : }
244 841 : return max;
245 : }
246 :
247 837 : void add_transition(const std::string& source, const std::string& target, const std::string& label)
248 : {
249 837 : fsm_transition t(source, target, label);
250 :
251 : // Apply a correction with +1 for the mismatch between numbering in lts_fsm and the fsm file format
252 837 : std::size_t max = std::max(t.source(),find_maximal_state_index(t.target()))+1;
253 :
254 837 : if (fsm.num_states() <= max)
255 : {
256 403 : fsm.set_num_states(max, fsm.has_state_info());
257 : }
258 837 : auto i = labels.find(t.label());
259 837 : lts_fsm_t::labels_size_type label_index = 0;
260 837 : if (i == labels.end())
261 : {
262 458 : assert(t.label() != action_label_string::tau_action());
263 458 : label_index = fsm.add_action(action_label_string(t.label()));
264 458 : labels[t.label()] = label_index;
265 : }
266 : else
267 : {
268 379 : label_index = i->second;
269 : }
270 :
271 837 : const std::size_t probabilistic_state_index = fsm.add_probabilistic_state(detail::lts_fsm_base::probabilistic_state(t.target()));
272 837 : fsm.add_transition(transition(t.source(), label_index, probabilistic_state_index));
273 837 : }
274 :
275 414 : void add_state(const std::vector<std::size_t>& values)
276 : {
277 414 : fsm.add_state(state_label_fsm(values));
278 414 : }
279 :
280 92 : void add_parameter(const std::string& name, const std::string& cardinality, const std::string& sort, const std::vector<std::string>& domain_values)
281 : {
282 92 : parameters.emplace_back(name, cardinality, sort, domain_values);
283 92 : }
284 :
285 4 : void add_initial_distribution(const std::string& distribution)
286 : {
287 4 : const lts_fsm_base::probabilistic_state d=parse_distribution(distribution);
288 4 : std::size_t max=find_maximal_state_index(d)+1; // Add one as state numbers are subtracted by one when parsing.
289 :
290 4 : if (fsm.num_states() <= max)
291 : {
292 2 : fsm.set_num_states(max, fsm.has_state_info());
293 : }
294 4 : fsm.add_probabilistic_state(detail::lts_fsm_base::probabilistic_state(d));
295 :
296 4 : fsm.set_initial_probabilistic_state(d);
297 4 : m_initial_state_is_set = true;
298 4 : }
299 :
300 61 : void write_parameters()
301 : {
302 61 : std::size_t index = 0;
303 153 : for (const fsm_parameter& param: parameters)
304 : {
305 92 : if (param.cardinality() > 0)
306 : {
307 92 : fsm.add_process_parameter(param.name(), param.sort());
308 324 : for (const std::string& value: param.values())
309 : {
310 232 : fsm.add_state_element_value(index, value);
311 : }
312 : }
313 92 : index++;
314 : }
315 61 : }
316 :
317 61 : void finish()
318 : {
319 : // guarantee that the LTS has at least one state
320 61 : if (fsm.num_states() == 0)
321 : {
322 0 : fsm.add_state();
323 : }
324 61 : if (!m_initial_state_is_set)
325 : {
326 57 : fsm.set_initial_probabilistic_state(detail::lts_fsm_base::probabilistic_state(0));
327 : }
328 61 : }
329 : };
330 :
331 : } // namespace mcrl2::lts::detail
332 :
333 : #endif // MCRL2_LTS_DETAIL_FSM_BUILDER_H
|
