Line data Source code
1 : // Author(s): Jan Friso Groote
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 :
10 : /** \file mcrl2/lts/detail/lts_convert.h
11 : *
12 : * \brief This file contains lts_convert routines that translate different lts formats into each other.
13 : * \details For each pair of lts formats there is a translation of one format into the other,
14 : if such a translation is possible.
15 : * \author Jan Friso Groote, Muck van Weerdenburg
16 : */
17 :
18 :
19 : #ifndef MCRL2_LTS_DETAIL_LTS_CONVERT_H
20 : #define MCRL2_LTS_DETAIL_LTS_CONVERT_H
21 :
22 : #include "mcrl2/lts/lts_lts.h"
23 : #include "mcrl2/lts/lts_aut.h"
24 : #include "mcrl2/lts/lts_fsm.h"
25 : #include "mcrl2/lts/lts_dot.h"
26 :
27 : namespace mcrl2
28 : {
29 : namespace lts
30 : {
31 : namespace detail
32 : {
33 :
34 : /** \brief Translate a fraction given as a data_expression to a representation
35 : * with an arbitrary size fraction */
36 :
37 : inline probabilistic_arbitrary_precision_fraction translate_probability_data_to_arbitrary_size_probability(const data::data_expression& d)
38 : {
39 : const data::application& da=atermpp::down_cast<data::application>(d);
40 : if (!(data::sort_int::is_integer_constant(da[0]) &&
41 : data::sort_pos::is_positive_constant(da[1]) &&
42 : da.head()==data::sort_real::creal()))
43 : {
44 : throw mcrl2::runtime_error("Cannot convert the probability " + pp(d) + " to an arbitrary size denominator/enumerator pair.");
45 : }
46 : return probabilistic_arbitrary_precision_fraction(pp(da[0]),pp(da[1]));
47 : }
48 :
49 : template <class PROBABILISTIC_STATE1, class PROBABILISTIC_STATE2>
50 : inline PROBABILISTIC_STATE2 lts_convert_probabilistic_state(const PROBABILISTIC_STATE1& )
51 : {
52 : throw mcrl2::runtime_error("Translation of probabilistic states is not defined");
53 : }
54 :
55 : template <>
56 : inline probabilistic_state<std::size_t, lps::probabilistic_data_expression>
57 : lts_convert_probabilistic_state<probabilistic_state<std::size_t, lps::probabilistic_data_expression>,
58 : probabilistic_state<std::size_t, lps::probabilistic_data_expression> >(
59 : const probabilistic_state<std::size_t, lps::probabilistic_data_expression>& state_in)
60 : {
61 : return state_in;
62 : }
63 :
64 : template <>
65 : inline probabilistic_state<std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction>
66 : lts_convert_probabilistic_state<probabilistic_state<std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction>,
67 : probabilistic_state<std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction> >(
68 : const probabilistic_state<std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction>& state_in)
69 : {
70 : return state_in;
71 : }
72 :
73 : template <>
74 : inline probabilistic_state<std::size_t, lps::probabilistic_data_expression>
75 : lts_convert_probabilistic_state<probabilistic_state<std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction>,
76 : probabilistic_state<std::size_t, lps::probabilistic_data_expression> >(
77 : const probabilistic_state<std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction>& state_in)
78 : {
79 : if (state_in.size()<=1) // There is only one state with probability 1.
80 : {
81 : return probabilistic_state<std::size_t, lps::probabilistic_data_expression>(state_in.get());
82 : }
83 : // There are more than one target states all with their own probabilities.
84 : std::vector<lps::state_probability_pair<std::size_t, lps::probabilistic_data_expression> > result;
85 : for(const lps::state_probability_pair<std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction>& p: state_in)
86 : {
87 : result.emplace_back(p.state(), lps::probabilistic_data_expression(pp(p.probability().enumerator()), pp(p.probability().denominator())));
88 : }
89 : return probabilistic_state<std::size_t, lps::probabilistic_data_expression>(result.begin(), result.end());
90 : }
91 :
92 112 : inline mcrl2::lts::probabilistic_arbitrary_precision_fraction translate_probability_data_prob(const data::data_expression& d)
93 : {
94 112 : const data::application& da=atermpp::down_cast<data::application>(d);
95 224 : if (!(data::sort_int::is_integer_constant(da[0]) &&
96 112 : data::sort_pos::is_positive_constant(da[1]) &&
97 112 : da.head()==data::sort_real::creal()))
98 : {
99 0 : throw mcrl2::runtime_error("Cannot convert the probability " + pp(d) + " to an explicit denominator/enumerator pair.");
100 : }
101 224 : return mcrl2::lts::probabilistic_arbitrary_precision_fraction(pp(da[0]),pp(da[1]));
102 : }
103 :
104 : template <>
105 : inline probabilistic_state<std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction>
106 58 : lts_convert_probabilistic_state<probabilistic_state<std::size_t, lps::probabilistic_data_expression>,
107 : probabilistic_state<std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction> >(
108 : const probabilistic_state<std::size_t, lps::probabilistic_data_expression>& state_in)
109 : {
110 58 : if (state_in.size()<=1) // There is only one state with probability 1.
111 : {
112 2 : return probabilistic_state<std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction>(state_in.get());
113 : }
114 : // There are more than one target states all with their own probabilities.
115 56 : std::vector<lps::state_probability_pair<std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction> > result;
116 168 : for(const lps::state_probability_pair<std::size_t, mcrl2::lps::probabilistic_data_expression>& p: state_in)
117 : {
118 112 : result.push_back(lps::state_probability_pair<std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction>(
119 : p.state(),
120 224 : translate_probability_data_prob(p.probability())));
121 : }
122 56 : return probabilistic_state<std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction>(result.begin(), result.end());
123 56 : }
124 :
125 :
126 :
127 : // ================================================================
128 : //
129 : // Below the translations for labelled transition system formats
130 : // to each other are provided. If a translation is not given,
131 : // the routines above are used to indicate at runtime that a
132 : // required translation does not exist.
133 : //
134 : // ================================================================
135 :
136 : // Default convertor, not doing anything.
137 : template <class BASE_LTS_IN, class BASE_LTS_OUT>
138 : class convertor
139 : {
140 : public:
141 : // Constructor
142 : convertor(const BASE_LTS_IN& , const BASE_LTS_OUT& )
143 : {}
144 :
145 : };
146 :
147 : // ====================== convert_core_lts =============================
148 :
149 : /* template <class CONVERTOR, class LTS_IN_TYPE, class LTS_OUT_TYPE>
150 : inline void convert_core_lts(CONVERTOR& c,
151 : const LTS_IN_TYPE& lts_in,
152 : LTS_OUT_TYPE& lts_out)
153 : {
154 : if (lts_in.has_state_info())
155 : {
156 : for (std::size_t i=0; i<lts_in.num_states(); ++i)
157 : {
158 : lts_out.add_state(c.translate_state(lts_in.state_label(i)));
159 : }
160 : }
161 : else
162 : {
163 : lts_out.set_num_states(lts_in.num_states(),false);
164 : }
165 :
166 : for (std::size_t i=0; i<lts_in.num_action_labels(); ++i)
167 : {
168 : lts_out.add_action(c.translate_label(lts_in.action_label(i)));
169 : if (lts_in.is_tau(i))
170 : {
171 : lts_out.set_tau(i);
172 : }
173 : }
174 :
175 : / * for (std::size_t i=0; i<lts_in.num_probabilistic_labels(); ++i)
176 : {
177 : lts_out.add_probabilistic_label(c.translate_probability_label(lts_in.probabilistic_label(i)));
178 : }
179 :
180 : for (std::size_t i=0; i<lts_in.num_states(); ++i)
181 : {
182 : if (lts_in.is_probabilistic(i))
183 : {
184 : lts_out.set_is_probabilistic(i,true);
185 : }
186 : } * /
187 :
188 : const std::vector<transition>& trans=lts_in.get_transitions();
189 : for (std::vector<transition>::const_iterator r=trans.begin(); r!=trans.end(); ++r)
190 : {
191 : lts_out.add_transition(*r);
192 : }
193 : lts_out.set_initial_state(lts_in.initial_state());
194 : } */
195 :
196 : // ========================================================================= REWRITTEN CODE ==============
197 :
198 12 : inline action_label_lts translate_label_aux(const action_label_string& l1,
199 : const data::data_specification& data,
200 : lps::multi_action_type_checker& typechecker)
201 : {
202 12 : std::string l(l1);
203 :
204 : // Remove quotes, if present in the action label string.
205 4 : if ((l.size()>=2) &&
206 28 : (l.substr(0,1)=="\"") &&
207 12 : (l.substr(l.size()-1,l.size())=="\""))
208 : {
209 0 : l=l.substr(1,l.size()-1);
210 : }
211 :
212 : try
213 : {
214 12 : const action_label_lts al=parse_lts_action(l,data,typechecker);
215 24 : return al;
216 12 : }
217 0 : catch (mcrl2::runtime_error& e)
218 : {
219 0 : throw mcrl2::runtime_error("Parse error in action label " + l1 + ".\n" + e.what());
220 0 : }
221 12 : }
222 :
223 : // ====================== lts -> lts =============================
224 :
225 : inline void lts_convert_base_class(const lts_lts_base& base_in, lts_lts_base& base_out)
226 : {
227 : base_out=base_in;
228 : }
229 :
230 : inline void lts_convert_base_class(const lts_lts_base& base_in,
231 : lts_lts_base& base_out,
232 : const data::data_specification& ,
233 : const process::action_label_list& ,
234 : const data::variable_list& ,
235 : const bool extra_data_is_defined=true)
236 : {
237 : if (extra_data_is_defined)
238 : {
239 : mCRL2log(log::warning) << "While translating .lts to .lts, additional information (data specification, action declarations and process parameters) is ignored.\n";
240 : }
241 : lts_convert_base_class(base_in, base_out);
242 : }
243 :
244 : inline action_label_lts lts_convert_translate_label(const action_label_lts& l_in, convertor<lts_lts_base, lts_lts_base>& )
245 : {
246 : return l_in;
247 : }
248 :
249 : inline void lts_convert_translate_state(const state_label_lts& state_label_in, state_label_lts& state_label_out, convertor<lts_lts_base, lts_lts_base>& /* c */)
250 : {
251 : state_label_out=state_label_in;
252 : }
253 :
254 : // ====================== lts -> fsm =============================
255 :
256 : template<>
257 : class convertor<lts_lts_base, lts_fsm_base>
258 : {
259 : public:
260 : std::vector < std::map <data::data_expression , std::size_t > > state_element_values_sets;
261 : lts_fsm_base& lts_out;
262 :
263 58 : convertor(const lts_lts_base& lts_base_in, lts_fsm_base& lts_base_out):
264 116 : state_element_values_sets(std::vector < std::map <data::data_expression , std::size_t > >
265 116 : (lts_base_in.process_parameters().size(), std::map <data::data_expression , std::size_t >())),
266 58 : lts_out(lts_base_out)
267 : {
268 58 : }
269 : };
270 :
271 58 : inline void lts_convert_base_class(const lts_lts_base& base_in, lts_fsm_base& base_out)
272 : {
273 58 : base_out.clear_process_parameters();
274 :
275 146 : for (const data::variable& v: base_in.process_parameters())
276 : {
277 88 : base_out.add_process_parameter(data::pp(v),data::pp(v.sort()));
278 : }
279 58 : }
280 :
281 508 : inline action_label_string lts_convert_translate_label(const action_label_lts& l_in, convertor<lts_lts_base, lts_fsm_base>& )
282 : {
283 1016 : return action_label_string(pp(l_in));
284 : }
285 :
286 : inline void lts_convert_base_class(const lts_lts_base& base_in,
287 : lts_fsm_base& base_out,
288 : const data::data_specification& ,
289 : const process::action_label_list& ,
290 : const data::variable_list& ,
291 : const bool extra_data_is_defined=true)
292 : {
293 : if (extra_data_is_defined)
294 : {
295 : mCRL2log(log::warning) << "While translating .lts to .fsm, additional information (data specification, action declarations and process parameters) are ignored.\n";
296 : }
297 : lts_convert_base_class(base_in, base_out);
298 : }
299 :
300 432 : inline void lts_convert_translate_state(const state_label_lts& state_label_in, state_label_fsm& state_label_out, convertor<lts_lts_base, lts_fsm_base>& c)
301 : {
302 432 : state_label_out.clear();
303 432 : std::size_t i=0;
304 432 : state_label_lts local_state_label_in;
305 432 : if (state_label_in.size()!=1)
306 : {
307 0 : assert(state_label_in.size()>1);
308 : // In this case the state label consists of a list of labels. However, the .fsm format cannot deal
309 : // with this, and we take only one of the labels in this list in the translation.
310 0 : local_state_label_in=state_label_lts(state_label_in.front());
311 : static bool warning_is_already_printed=false;
312 0 : if (!warning_is_already_printed)
313 : {
314 0 : mCRL2log(log::warning) << "The state label " + pp(state_label_in) + " consists of " + std::to_string(state_label_in.size()) +
315 0 : " state vectors and all but the first label are ignored. This warning is only printed once. ";
316 0 : warning_is_already_printed=true;
317 : }
318 : }
319 : else
320 : {
321 432 : local_state_label_in=state_label_in;
322 : }
323 4034 : for (const data::data_expression& t: *local_state_label_in.begin())
324 : {
325 3602 : std::map <data::data_expression , std::size_t >::const_iterator index=c.state_element_values_sets[i].find(t);
326 3602 : if (index==c.state_element_values_sets[i].end())
327 : {
328 224 : const std::size_t element_index=c.state_element_values_sets[i].size();
329 224 : state_label_out.push_back(element_index);
330 224 : c.lts_out.add_state_element_value(i,data::pp(t));
331 224 : c.state_element_values_sets[i][t]=element_index;
332 : }
333 : else
334 : {
335 3378 : state_label_out.push_back(index->second);
336 : }
337 3602 : ++i;
338 : }
339 432 : }
340 :
341 : // ====================== lts -> aut =============================
342 :
343 : inline void lts_convert_base_class(const lts_lts_base& /* base_in */, lts_aut_base& /* base_out */)
344 : {
345 : // Nothing needs to be done.
346 : }
347 :
348 : inline void lts_convert_base_class(const lts_lts_base& base_in,
349 : lts_aut_base& base_out,
350 : const data::data_specification& ,
351 : const process::action_label_list& ,
352 : const data::variable_list& ,
353 : const bool extra_data_is_defined=true)
354 : {
355 : if (extra_data_is_defined)
356 : {
357 : mCRL2log(log::warning) << "While translating .lts to .aut, additional information (data specification, action declarations and process parameters) are ignored.\n";
358 : }
359 : lts_convert_base_class(base_in, base_out);
360 : }
361 :
362 : inline action_label_string lts_convert_translate_label(const action_label_lts& l_in, convertor<lts_lts_base, lts_aut_base>& )
363 : {
364 : return action_label_string(pp(l_in));
365 : }
366 :
367 : inline void lts_convert_translate_state(const state_label_lts& /* state_label_in */, state_label_empty& state_label_out, convertor<lts_lts_base, lts_aut_base>& /* c */)
368 : {
369 : state_label_out=state_label_empty();
370 : }
371 :
372 : // ====================== lts -> dot =============================
373 :
374 : template<>
375 : class convertor<lts_lts_base, lts_dot_base>
376 : {
377 : public:
378 : std::size_t m_state_count;
379 :
380 0 : convertor(const lts_lts_base& /* lts_base_in */, lts_dot_base& /* lts_base_out */):
381 0 : m_state_count(0)
382 : {
383 0 : }
384 : };
385 :
386 0 : inline void lts_convert_base_class(const lts_lts_base& /* base_in */, lts_dot_base& /* base_out */)
387 : {
388 : // Nothing needs to be done.
389 0 : }
390 :
391 : inline void lts_convert_base_class(const lts_lts_base& base_in,
392 : lts_dot_base& base_out,
393 : const data::data_specification& ,
394 : const process::action_label_list& ,
395 : const data::variable_list& ,
396 : const bool extra_data_is_defined=true)
397 : {
398 : if (extra_data_is_defined)
399 : {
400 : mCRL2log(log::warning) << "While translating .lts to .dot, additional information (data specification, action declarations and process parameters) are ignored.\n";
401 : }
402 : lts_convert_base_class(base_in, base_out);
403 : }
404 :
405 0 : inline action_label_string lts_convert_translate_label(const action_label_lts& l_in, convertor<lts_lts_base, lts_dot_base>& )
406 : {
407 0 : return action_label_string(pp(l_in));
408 : }
409 :
410 0 : inline void lts_convert_translate_state(const state_label_lts& state_label_in, state_label_dot& state_label_out, convertor<lts_lts_base, lts_dot_base>& c)
411 : {
412 0 : std::stringstream state_name;
413 0 : state_name << "s" << c.m_state_count;
414 0 : c.m_state_count++;
415 0 : state_label_out=state_label_dot(state_name.str(),pp(state_label_in));
416 0 : }
417 :
418 : // ====================== fsm -> lts =============================
419 :
420 : template<>
421 : class convertor<lts_fsm_base, lts_lts_base>
422 :
423 : {
424 : public:
425 : const lts_fsm_base& m_lts_in;
426 : const lts_lts_base& m_lts_out;
427 : lps::multi_action_type_checker m_typechecker;
428 :
429 : convertor(const lts_fsm_base& lts_base_in, lts_lts_base& lts_base_out):
430 : m_lts_in(lts_base_in), m_lts_out(lts_base_out),
431 : m_typechecker(lts_base_out.data(), data::variable_list(), lts_base_out.action_label_declarations())
432 : {
433 : }
434 : };
435 :
436 : inline void lts_convert_base_class(const lts_fsm_base& /* base_in */, lts_lts_base& /* base_out */)
437 : {
438 : throw mcrl2::runtime_error("Cannot translate .fsm into .lts format without additional LPS information (data, action declarations and process parameters).");
439 : }
440 :
441 : inline void lts_convert_base_class(const lts_fsm_base& base_in,
442 : lts_lts_base& base_out,
443 : const data::data_specification& data,
444 : const process::action_label_list& action_labels,
445 : const data::variable_list& process_parameters,
446 : const bool extra_data_is_defined=true)
447 : {
448 : if (extra_data_is_defined)
449 : {
450 : base_out.set_data(data);
451 : base_out.set_action_label_declarations(action_labels);
452 : base_out.set_process_parameters(process_parameters);
453 : }
454 : else
455 : {
456 : lts_convert_base_class(base_in,base_out);
457 : }
458 : }
459 :
460 : inline action_label_lts lts_convert_translate_label(const action_label_string& l1, convertor<lts_fsm_base, lts_lts_base>& c)
461 : {
462 : return translate_label_aux(l1, c.m_lts_out.data(), c.m_typechecker);
463 : }
464 :
465 : inline void lts_convert_translate_state(const state_label_fsm& state_label_in,
466 : state_label_lts& state_label_out,
467 : convertor<lts_fsm_base, lts_lts_base>& c)
468 : {
469 : // If process_parameters are not empty, we use them to check that the sorts of its variables match.
470 : std::vector < data::data_expression > state_label;
471 : std::size_t idx=0;
472 : const data::variable_list& parameters=c.m_lts_out.process_parameters();
473 : data::variable_list::const_iterator parameter_iterator=parameters.begin();
474 : for (state_label_fsm::const_iterator i=state_label_in.begin(); i!=state_label_in.end(); ++i, ++idx)
475 : {
476 : assert(parameters.empty() || parameter_iterator!=parameters.end());
477 : data::data_expression d=data::parse_data_expression(c.m_lts_in.state_element_value(idx,*i),c.m_lts_out.data());
478 : if (!parameters.empty() && (d.sort()!=parameter_iterator->sort()))
479 : {
480 : try
481 : {
482 : /* The type of the parsed expression may not exactly match the expected type.
483 : Attempt to match exactly below.
484 : TODO: replace this with a function parse_data_expression_with_expected_type when it exists */
485 : data::data_type_checker typechecker(c.m_lts_out.data());
486 : data::detail::variable_context variable_context;
487 : variable_context.add_context_variables(data::variable_list(), typechecker);
488 : d=typechecker.typecheck_data_expression(d, parameter_iterator->sort(), variable_context);
489 : }
490 : catch (mcrl2::runtime_error& e)
491 : {
492 : throw mcrl2::runtime_error("Sort of parameter " + pp(*parameter_iterator) + ":" +
493 : pp(parameter_iterator->sort()) + " does not match with the sort " + pp(d.sort()) +
494 : " of actual value " + pp(d) + ".\n" + e.what());
495 : }
496 : }
497 : state_label.push_back(d);
498 : if (!parameters.empty())
499 : {
500 : ++parameter_iterator;
501 : }
502 : }
503 : assert(parameter_iterator==parameters.end());
504 :
505 : state_label_out=state_label_lts(state_label);
506 : }
507 :
508 : // ====================== fsm -> fsm =============================
509 :
510 : inline void lts_convert_base_class(const lts_fsm_base& base_in, lts_fsm_base& base_out)
511 : {
512 : base_out=base_in;
513 : }
514 :
515 : inline void lts_convert_base_class(const lts_fsm_base& base_in,
516 : lts_fsm_base& base_out,
517 : const data::data_specification& ,
518 : const process::action_label_list& ,
519 : const data::variable_list& ,
520 : const bool extra_data_is_defined=true)
521 : {
522 : if (extra_data_is_defined)
523 : {
524 : mCRL2log(log::warning) << "While translating .fsm to .fsm, additional information (data specification, action declarations and process parameters) are ignored.\n";
525 : }
526 : lts_convert_base_class(base_in,base_out);
527 : }
528 :
529 : inline void lts_convert_translate_state(const state_label_fsm& state_label_in, state_label_fsm& state_label_out, convertor<lts_fsm_base, lts_fsm_base>& /* c */)
530 : {
531 : state_label_out=state_label_in;
532 : }
533 :
534 : inline action_label_string lts_convert_translate_label(const action_label_string& l_in, convertor<lts_fsm_base, lts_fsm_base>& )
535 : {
536 : return l_in;
537 : }
538 :
539 : // ====================== fsm -> aut =============================
540 :
541 : inline void lts_convert_base_class(const lts_fsm_base& /* base_in */, lts_aut_base& /* base_out */)
542 : {
543 : // Nothing needs to be done.
544 : }
545 :
546 : inline void lts_convert_base_class(const lts_fsm_base& base_in,
547 : lts_aut_base& base_out,
548 : const data::data_specification& ,
549 : const process::action_label_list& ,
550 : const data::variable_list& ,
551 : const bool extra_data_is_defined=true)
552 : {
553 : if (extra_data_is_defined)
554 : {
555 : mCRL2log(log::warning) << "While translating .fsm to .aut, additional information (data specification, action declarations and process parameters) are ignored.\n";
556 : }
557 : lts_convert_base_class(base_in,base_out);
558 : }
559 :
560 : inline void lts_convert_translate_state(const state_label_fsm&, state_label_empty& state_label_out, convertor<lts_fsm_base, lts_aut_base>& /* c */)
561 : {
562 : state_label_out=state_label_empty();
563 : }
564 :
565 : inline action_label_string lts_convert_translate_label(const action_label_string& l_in, convertor<lts_fsm_base, lts_aut_base>& )
566 : {
567 : return l_in;
568 : }
569 :
570 :
571 : // ====================== fsm -> dot =============================
572 :
573 : template<>
574 : class convertor<lts_fsm_base, lts_dot_base>
575 : {
576 : public:
577 : std::size_t m_state_count;
578 : const lts_fsm_base& m_lts_in;
579 :
580 : convertor(const lts_fsm_base& lts_base_in, const lts_dot_base& /* lts_base_out */)
581 : : m_state_count(0), m_lts_in(lts_base_in)
582 : {
583 : }
584 : };
585 :
586 : inline void lts_convert_base_class(const lts_fsm_base& /* base_in */, lts_dot_base& /* base_out */)
587 : {
588 : // Nothing needs to be done.
589 : }
590 :
591 : inline void lts_convert_base_class(const lts_fsm_base& base_in,
592 : lts_dot_base& base_out,
593 : const data::data_specification& ,
594 : const process::action_label_list& ,
595 : const data::variable_list& ,
596 : const bool extra_data_is_defined=true)
597 : {
598 : if (extra_data_is_defined)
599 : {
600 : mCRL2log(log::warning) << "While translating .fsm to .aut, additional information (data specification, action declarations and process parameters) are ignored.\n";
601 : }
602 : lts_convert_base_class(base_in,base_out);
603 : }
604 :
605 : inline void lts_convert_translate_state(const state_label_fsm& state_label_in, state_label_dot& state_label_out, convertor<lts_fsm_base, lts_dot_base>& c)
606 : {
607 : std::stringstream state_name;
608 : state_name << "s" << c.m_state_count;
609 : c.m_state_count++;
610 :
611 : std::string state_label;
612 : if (!state_label_in.empty())
613 : {
614 : state_label="(";
615 : for (std::size_t i=0; i<state_label_in.size(); ++i)
616 : {
617 : state_label=state_label + c.m_lts_in.state_element_value(i,state_label_in[i])+(i+1==state_label_in.size()?")":",");
618 : }
619 : }
620 :
621 : state_label_out=state_label_dot(state_name.str(),state_label);
622 : }
623 :
624 : inline action_label_string lts_convert_translate_label(const action_label_string& l_in, convertor<lts_fsm_base, lts_dot_base>& )
625 : {
626 : return l_in;
627 : }
628 :
629 :
630 : // ====================== aut -> lts =============================
631 :
632 : template<>
633 : class convertor<lts_aut_base, lts_lts_base>
634 : {
635 : public:
636 : const data::data_specification& m_data;
637 : lps::multi_action_type_checker m_typechecker;
638 :
639 4 : convertor(const lts_aut_base& /* lts_base_in*/, const lts_lts_base& lts_base_out)
640 4 : : m_data(lts_base_out.data()),
641 4 : m_typechecker(m_data, data::variable_list(), lts_base_out.action_label_declarations())
642 : {
643 4 : }
644 : };
645 :
646 0 : inline void lts_convert_base_class(const lts_aut_base& /* base_in */, lts_lts_base& /* base_out */)
647 : {
648 0 : throw mcrl2::runtime_error("Cannot translate .aut into .lts format without additional information (data, action declarations and process parameters)");
649 : }
650 :
651 4 : inline void lts_convert_base_class(const lts_aut_base& base_in,
652 : lts_lts_base& base_out,
653 : const data::data_specification& data,
654 : const process::action_label_list& action_labels,
655 : const data::variable_list& process_parameters,
656 : const bool extra_data_is_defined=true)
657 : {
658 4 : if (extra_data_is_defined)
659 : {
660 4 : base_out.set_data(data);
661 4 : base_out.set_action_label_declarations(action_labels);
662 4 : base_out.set_process_parameters(process_parameters);
663 : }
664 : else
665 : {
666 0 : lts_convert_base_class(base_in,base_out);
667 : }
668 4 : }
669 :
670 12 : inline action_label_lts lts_convert_translate_label(const action_label_string& l_in, convertor<lts_aut_base, lts_lts_base>& c)
671 : {
672 12 : return translate_label_aux(l_in, c.m_data, c.m_typechecker);
673 : }
674 :
675 0 : inline void lts_convert_translate_state(const state_label_empty& /* state_label_in */, state_label_lts& state_label_out, convertor<lts_aut_base, lts_lts_base>& /* c */)
676 : {
677 : // There is no state label. Use the default.
678 0 : state_label_out=state_label_lts();
679 0 : }
680 :
681 : /* data::data_expression translate_probability_label(const probabilistic_arbitrary_precision_fraction& d)
682 : {
683 : return detail::translate_probability_prob_data_arbitrary_size(d);
684 : } */
685 :
686 : // ====================== aut -> fsm =============================
687 :
688 : inline void lts_convert_base_class(const lts_aut_base& /* base_in */, lts_fsm_base& base_out)
689 : {
690 : //Reset lts_out
691 : base_out=lts_fsm_base();
692 : }
693 :
694 : inline void lts_convert_base_class(const lts_aut_base& base_in,
695 : lts_fsm_base& base_out,
696 : const data::data_specification& ,
697 : const process::action_label_list& ,
698 : const data::variable_list& ,
699 : const bool extra_data_is_defined=true)
700 : {
701 : if (extra_data_is_defined)
702 : {
703 : mCRL2log(log::warning) << "While translating .aut to .fsm, additional information (data specification, action declarations and process parameters) are ignored.\n";
704 : }
705 : lts_convert_base_class(base_in,base_out);
706 : }
707 :
708 : inline action_label_string lts_convert_translate_label(const action_label_string& l_in, convertor<lts_aut_base, lts_fsm_base>& )
709 : {
710 : return l_in;
711 : }
712 :
713 : inline void lts_convert_translate_state(const state_label_empty& /* state_label_in */, state_label_fsm& state_label_out, convertor<lts_aut_base, lts_fsm_base>& /* c */)
714 : {
715 : state_label_out=state_label_fsm();
716 : }
717 :
718 : // ====================== aut -> aut =============================
719 :
720 : inline void lts_convert_base_class(const lts_aut_base& base_in, lts_aut_base& base_out)
721 : {
722 : base_out=base_in;
723 : }
724 :
725 : inline void lts_convert_base_class(const lts_aut_base& base_in,
726 : lts_aut_base& base_out,
727 : const data::data_specification& ,
728 : const process::action_label_list& ,
729 : const data::variable_list& ,
730 : const bool extra_data_is_defined=true)
731 : {
732 : if (extra_data_is_defined)
733 : {
734 : mCRL2log(log::warning) << "While translating .aut to .aut, additional information (data specification, action declarations and process parameters) are ignored.\n";
735 : }
736 : lts_convert_base_class(base_in,base_out);
737 : }
738 :
739 : inline void lts_convert_translate_state(const state_label_empty& state_label_in, state_label_empty& state_label_out, convertor<lts_aut_base, lts_aut_base>& /* c */)
740 : {
741 : state_label_out=state_label_in;
742 : }
743 :
744 : inline action_label_string lts_convert_translate_label(const action_label_string& l_in, convertor<lts_aut_base, lts_aut_base>& )
745 : {
746 : return l_in;
747 : }
748 :
749 : // ====================== aut -> dot =============================
750 :
751 : inline void lts_convert_base_class(const lts_aut_base& /* base_in */, lts_dot_base& /* base_out */)
752 : {
753 : // Nothing needs to be done.
754 : }
755 :
756 : inline void lts_convert_base_class(const lts_aut_base& base_in,
757 : lts_dot_base& base_out,
758 : const data::data_specification& ,
759 : const process::action_label_list& ,
760 : const data::variable_list& ,
761 : const bool extra_data_is_defined=true)
762 : {
763 : if (extra_data_is_defined)
764 : {
765 : mCRL2log(log::warning) << "While translating .aut to .dot, additional information (data specification, action declarations and process parameters) are ignored.\n";
766 : }
767 : lts_convert_base_class(base_in,base_out);
768 : }
769 :
770 : inline void lts_convert_translate_state(const state_label_empty& /* state_label_in */, state_label_dot& state_label_out, convertor<lts_aut_base, lts_dot_base>& /* c */)
771 : {
772 : state_label_out=state_label_dot();
773 : }
774 :
775 : inline action_label_string lts_convert_translate_label(const action_label_string& l_in, convertor<lts_aut_base, lts_dot_base>& )
776 : {
777 : return l_in;
778 : }
779 :
780 :
781 : // ====================== END CONCRETE LTS FORMAT CONVERSIONS =============================
782 :
783 :
784 : // ====================== BEGIN ACTUAL CONVERSIONS =============================
785 :
786 :
787 : // Actual conversion without base class conversion.
788 : template < class STATE_LABEL1, class ACTION_LABEL1, class LTS_BASE1, class STATE_LABEL2, class ACTION_LABEL2, class LTS_BASE2>
789 62 : inline void lts_convert_aux(const lts<STATE_LABEL1, ACTION_LABEL1, LTS_BASE1>& lts_in,
790 : lts<STATE_LABEL2, ACTION_LABEL2, LTS_BASE2>& lts_out)
791 : {
792 62 : convertor<LTS_BASE1, LTS_BASE2> c(lts_in, lts_out);
793 :
794 62 : if (lts_in.has_state_info())
795 : {
796 490 : for (std::size_t i=0; i<lts_in.num_states(); ++i)
797 : {
798 432 : STATE_LABEL2 s;
799 432 : lts_convert_translate_state(lts_in.state_label(i), s, c);
800 432 : lts_out.add_state(s);
801 : }
802 : }
803 : else
804 : {
805 4 : lts_out.set_num_states(lts_in.num_states(),false);
806 : }
807 :
808 582 : for (std::size_t i=0; i<lts_in.num_action_labels(); ++i)
809 : {
810 520 : lts_out.add_action(lts_convert_translate_label(lts_in.action_label(i),c));
811 : }
812 :
813 62 : const std::vector<transition>& trans=lts_in.get_transitions();
814 907 : for (const transition& t: trans)
815 : {
816 845 : lts_out.add_transition(t);
817 : }
818 62 : lts_out.set_initial_state(lts_in.initial_state());
819 :
820 62 : lts_out.set_hidden_label_set(lts_in.hidden_label_set());
821 62 : }
822 :
823 : // ====================== lts -> lts =============================
824 :
825 : template < class STATE_LABEL1, class ACTION_LABEL1, class LTS_BASE1, class STATE_LABEL2, class ACTION_LABEL2, class LTS_BASE2>
826 58 : inline void lts_convert(const lts<STATE_LABEL1, ACTION_LABEL1, LTS_BASE1>& lts_in,
827 : lts<STATE_LABEL2, ACTION_LABEL2, LTS_BASE2>& lts_out)
828 : {
829 58 : lts_convert_base_class(static_cast<const LTS_BASE1&>(lts_in), static_cast<LTS_BASE2&>(lts_out));
830 58 : lts_convert_aux<STATE_LABEL1, ACTION_LABEL1, LTS_BASE1,STATE_LABEL2, ACTION_LABEL2, LTS_BASE2>(lts_in,lts_out);
831 58 : }
832 :
833 : template < class STATE_LABEL1, class ACTION_LABEL1, class LTS_BASE1,
834 : class STATE_LABEL2, class ACTION_LABEL2, class LTS_BASE2>
835 4 : inline void lts_convert(const lts<STATE_LABEL1, ACTION_LABEL1, LTS_BASE1>& lts_in,
836 : lts<STATE_LABEL2, ACTION_LABEL2, LTS_BASE2>& lts_out,
837 : const data::data_specification& ds,
838 : const process::action_label_list& all,
839 : const data::variable_list& vl,
840 : const bool extra_data_is_defined=true)
841 : {
842 4 : lts_convert_base_class(static_cast<const LTS_BASE1&>(lts_in), static_cast<LTS_BASE2&>(lts_out), ds, all, vl, extra_data_is_defined);
843 4 : lts_convert_aux<STATE_LABEL1, ACTION_LABEL1, LTS_BASE1,STATE_LABEL2, ACTION_LABEL2, LTS_BASE2>(lts_in,lts_out);
844 4 : }
845 :
846 : // ====================== probabilistic_lts -> lts =============================
847 :
848 : template < class STATE_LABEL1, class ACTION_LABEL1, class PROBABILISTIC_STATE1, class LTS_BASE1, class STATE_LABEL2, class ACTION_LABEL2, class LTS_BASE2>
849 : void remove_probabilities(const probabilistic_lts<STATE_LABEL1, ACTION_LABEL1, PROBABILISTIC_STATE1, LTS_BASE1>& lts_in,
850 : lts<STATE_LABEL2, ACTION_LABEL2, LTS_BASE2>& lts_out)
851 : {
852 : if (lts_in.initial_probabilistic_state().size()<=1)
853 : {
854 : lts_out.set_initial_state(lts_in.initial_probabilistic_state().get());
855 : }
856 : else
857 : {
858 : throw mcrl2::runtime_error("Initial state is probabilistic and cannot be transformed into a non probabilistic state.");
859 : }
860 :
861 : // Adapt the probabilistic target states to non probabilistic target states.
862 : std::size_t transition_number=1;
863 : for(transition& t: lts_out.get_transitions())
864 : {
865 : std::size_t probabilistic_target_state_number=t.to();
866 : if (lts_in.probabilistic_state(probabilistic_target_state_number).size()>1)
867 : {
868 : throw mcrl2::runtime_error("Transition " + std::to_string(transition_number) + " is probabilistic.");
869 : }
870 : else
871 : {
872 : t=transition(t.from(), t.label(), lts_in.probabilistic_state(probabilistic_target_state_number).get());
873 : }
874 : transition_number++;
875 : }
876 : }
877 :
878 : template < class STATE_LABEL1, class ACTION_LABEL1, class LTS_BASE1, class PROBABILISTIC_STATE1, class STATE_LABEL2, class ACTION_LABEL2, class LTS_BASE2>
879 : inline void lts_convert(const probabilistic_lts<STATE_LABEL1, ACTION_LABEL1, PROBABILISTIC_STATE1, LTS_BASE1>& lts_in,
880 : lts<STATE_LABEL2, ACTION_LABEL2, LTS_BASE2>& lts_out)
881 : {
882 : lts_convert<STATE_LABEL1, ACTION_LABEL1, LTS_BASE1, STATE_LABEL2, ACTION_LABEL2, LTS_BASE2>(lts_in,lts_out);
883 : remove_probabilities(lts_in,lts_out);
884 :
885 : }
886 :
887 :
888 :
889 : template < class STATE_LABEL1, class ACTION_LABEL1, class PROBABILISTIC_STATE1, class LTS_BASE1,
890 : class STATE_LABEL2, class ACTION_LABEL2, class LTS_BASE2>
891 : inline void lts_convert(const probabilistic_lts<STATE_LABEL1, ACTION_LABEL1, PROBABILISTIC_STATE1, LTS_BASE1>& lts_in,
892 : lts<STATE_LABEL2, ACTION_LABEL2, LTS_BASE2>& lts_out,
893 : const data::data_specification& data,
894 : const process::action_label_list& action_label_list,
895 : const data::variable_list& process_parameters,
896 : const bool extra_data_is_defined=true)
897 : {
898 : lts_convert<STATE_LABEL1, ACTION_LABEL1, LTS_BASE1,STATE_LABEL2, ACTION_LABEL2, LTS_BASE2>(lts_in,lts_out,data,action_label_list,process_parameters,extra_data_is_defined);
899 : remove_probabilities(lts_in,lts_out);
900 : }
901 :
902 : // ====================== lts -> probabilistic_lts =============================
903 :
904 : template < class STATE_LABEL1, class ACTION_LABEL1, class LTS_BASE1,
905 : class STATE_LABEL2, class ACTION_LABEL2, class PROBABILISTIC_STATE2, class LTS_BASE2>
906 : inline void add_probabilities(const lts<STATE_LABEL1, ACTION_LABEL1, LTS_BASE1>& lts_in,
907 : probabilistic_lts<STATE_LABEL2, ACTION_LABEL2, PROBABILISTIC_STATE2, LTS_BASE2>& lts_out)
908 : {
909 : lts_out.set_initial_probabilistic_state(PROBABILISTIC_STATE2(lts_in.initial_state()));
910 : for(std::size_t i=0; i<lts_out.num_states(); ++i)
911 : {
912 : lts_out.add_probabilistic_state(PROBABILISTIC_STATE2(i));
913 : }
914 : }
915 :
916 :
917 : template < class STATE_LABEL1, class ACTION_LABEL1, class LTS_BASE1, class STATE_LABEL2, class ACTION_LABEL2, class PROBABILISTIC_STATE2, class LTS_BASE2>
918 : inline void lts_convert(const lts<STATE_LABEL1, ACTION_LABEL1, LTS_BASE1>& lts_in,
919 : probabilistic_lts<STATE_LABEL2, ACTION_LABEL2, PROBABILISTIC_STATE2, LTS_BASE2>& lts_out)
920 : {
921 : lts_convert<STATE_LABEL1, ACTION_LABEL1, LTS_BASE1, STATE_LABEL2, ACTION_LABEL2, LTS_BASE2>(lts_in,lts_out);
922 : add_probabilities(lts_in,lts_out);
923 : }
924 :
925 : template < class STATE_LABEL1, class ACTION_LABEL1, class LTS_BASE1,
926 : class STATE_LABEL2, class ACTION_LABEL2, class PROBABILISTIC_STATE2, class LTS_BASE2>
927 : inline void lts_convert(const lts<STATE_LABEL1, ACTION_LABEL1, LTS_BASE1>& lts_in,
928 : probabilistic_lts<STATE_LABEL2, ACTION_LABEL2, PROBABILISTIC_STATE2, LTS_BASE2>& lts_out,
929 : const data::data_specification& data,
930 : const process::action_label_list& action_label_list,
931 : const data::variable_list& process_parameters,
932 : const bool extra_data_is_defined=true)
933 : {
934 : lts_convert<STATE_LABEL1, ACTION_LABEL1, LTS_BASE1,STATE_LABEL2, ACTION_LABEL2, LTS_BASE2>(lts_in,lts_out,data,action_label_list,process_parameters,extra_data_is_defined);
935 : add_probabilities(lts_in, lts_out);
936 : }
937 :
938 : // ====================== probabilistic_lts -> probabilistic_lts =============================
939 :
940 : template < class STATE_LABEL1, class ACTION_LABEL1, class PROBABILISTIC_STATE1, class LTS_BASE1,
941 : class STATE_LABEL2, class ACTION_LABEL2, class PROBABILISTIC_STATE2, class LTS_BASE2>
942 4 : inline void translate_probability_labels(const probabilistic_lts<STATE_LABEL1, ACTION_LABEL1, PROBABILISTIC_STATE1, LTS_BASE1>& lts_in,
943 : probabilistic_lts<STATE_LABEL2, ACTION_LABEL2, PROBABILISTIC_STATE2, LTS_BASE2>& lts_out)
944 : {
945 4 : lts_out.clear_probabilistic_states();
946 58 : for(std::size_t i=0; i< lts_in.num_probabilistic_states(); ++i)
947 : {
948 54 : lts_out.add_probabilistic_state(lts_convert_probabilistic_state<PROBABILISTIC_STATE1,PROBABILISTIC_STATE2>(lts_in.probabilistic_state(i)));
949 : }
950 4 : lts_out.set_initial_probabilistic_state(lts_convert_probabilistic_state<PROBABILISTIC_STATE1,PROBABILISTIC_STATE2>(lts_in.initial_probabilistic_state()));
951 4 : }
952 :
953 :
954 : template < class STATE_LABEL1, class ACTION_LABEL1, class PROBABILISTIC_STATE1, class LTS_BASE1,
955 : class STATE_LABEL2, class ACTION_LABEL2, class PROBABILISTIC_STATE2, class LTS_BASE2>
956 4 : inline void lts_convert(const probabilistic_lts<STATE_LABEL1, ACTION_LABEL1, PROBABILISTIC_STATE1, LTS_BASE1>& lts_in,
957 : probabilistic_lts<STATE_LABEL2, ACTION_LABEL2, PROBABILISTIC_STATE2, LTS_BASE2>& lts_out)
958 : {
959 4 : lts_convert(static_cast<const lts<STATE_LABEL1, ACTION_LABEL1, LTS_BASE1>& >(lts_in),
960 : static_cast<lts<STATE_LABEL2, ACTION_LABEL2, LTS_BASE2>& >(lts_out));
961 4 : translate_probability_labels(lts_in,lts_out);
962 4 : }
963 :
964 : template < class STATE_LABEL1, class ACTION_LABEL1, class PROBABILISTIC_STATE1, class LTS_BASE1,
965 : class STATE_LABEL2, class ACTION_LABEL2, class PROBABILISTIC_STATE2, class LTS_BASE2>
966 : inline void lts_convert(const probabilistic_lts<STATE_LABEL1, ACTION_LABEL1, PROBABILISTIC_STATE1, LTS_BASE1>& lts_in,
967 : probabilistic_lts<STATE_LABEL2, ACTION_LABEL2, PROBABILISTIC_STATE2, LTS_BASE2>& lts_out,
968 : const data::data_specification& data,
969 : const process::action_label_list& action_label_list,
970 : const data::variable_list& process_parameters,
971 : const bool extra_data_is_defined=true)
972 : {
973 : lts_convert(static_cast<const lts<STATE_LABEL1, ACTION_LABEL1, LTS_BASE1>& >(lts_in),
974 : static_cast<lts<STATE_LABEL2, ACTION_LABEL2, LTS_BASE2>& >(lts_out),
975 : data, action_label_list, process_parameters, extra_data_is_defined);
976 : translate_probability_labels(lts_in,lts_out);
977 : }
978 :
979 : // ====================== END ACTUAL CONVERSIONS =============================
980 :
981 : } // namespace detail
982 : } // namespace lts
983 : } // namespace mcrl2
984 :
985 : #endif
|
