mCRL2
Loading...
Searching...
No Matches
lts_convert.h
Go to the documentation of this file.
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
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
27namespace mcrl2
28{
29namespace lts
30{
31namespace detail
32{
33
38{
39 const data::application& da=atermpp::down_cast<data::application>(d);
43 {
44 throw mcrl2::runtime_error("Cannot convert the probability " + pp(d) + " to an arbitrary size denominator/enumerator pair.");
45 }
47}
48
49template <class PROBABILISTIC_STATE1, class PROBABILISTIC_STATE2>
50inline PROBABILISTIC_STATE2 lts_convert_probabilistic_state(const PROBABILISTIC_STATE1& )
51{
52 throw mcrl2::runtime_error("Translation of probabilistic states is not defined");
53}
54
55template <>
57lts_convert_probabilistic_state<probabilistic_state<std::size_t, lps::probabilistic_data_expression>,
60{
61 return state_in;
62}
63
64template <>
65inline probabilistic_state<std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction>
66lts_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
73template <>
74inline probabilistic_state<std::size_t, lps::probabilistic_data_expression>
75lts_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
93{
94 const data::application& da=atermpp::down_cast<data::application>(d);
98 {
99 throw mcrl2::runtime_error("Cannot convert the probability " + pp(d) + " to an explicit denominator/enumerator pair.");
100 }
102}
103
104template <>
106lts_convert_probabilistic_state<probabilistic_state<std::size_t, lps::probabilistic_data_expression>,
109{
110 if (state_in.size()<=1) // There is only one state with probability 1.
111 {
113 }
114 // There are more than one target states all with their own probabilities.
115 std::vector<lps::state_probability_pair<std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction> > result;
117 {
119 p.state(),
120 translate_probability_data_prob(p.probability())));
121 }
122 return probabilistic_state<std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction>(result.begin(), result.end());
123}
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.
137template <class BASE_LTS_IN, class BASE_LTS_OUT>
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>
150inline 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
199 const data::data_specification& data,
201{
202 std::string l(l1);
203
204 // Remove quotes, if present in the action label string.
205 if ((l.size()>=2) &&
206 (l.substr(0,1)=="\"") &&
207 (l.substr(l.size()-1,l.size())=="\""))
208 {
209 l=l.substr(1,l.size()-1);
210 }
211
212 try
213 {
214 const action_label_lts al=parse_lts_action(l,data,typechecker);
215 return al;
216 }
217 catch (mcrl2::runtime_error& e)
218 {
219 throw mcrl2::runtime_error("Parse error in action label " + l1 + ".\n" + e.what());
220 }
221}
222
223// ====================== lts -> lts =============================
224
225inline void lts_convert_base_class(const lts_lts_base& base_in, lts_lts_base& base_out)
226{
227 base_out=base_in;
228}
229
230inline void lts_convert_base_class(const lts_lts_base& base_in,
231 lts_lts_base& base_out,
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
245{
246 return l_in;
247}
248
249inline 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
256template<>
258{
259 public:
260 std::vector < std::map <data::data_expression , std::size_t > > state_element_values_sets;
262
263 convertor(const lts_lts_base& lts_base_in, lts_fsm_base& lts_base_out):
264 state_element_values_sets(std::vector < std::map <data::data_expression , std::size_t > >
265 (lts_base_in.process_parameters().size(), std::map <data::data_expression , std::size_t >())),
266 lts_out(lts_base_out)
267 {
268 }
269};
270
271inline void lts_convert_base_class(const lts_lts_base& base_in, lts_fsm_base& base_out)
272{
273 base_out.clear_process_parameters();
274
275 for (const data::variable& v: base_in.process_parameters())
276 {
277 base_out.add_process_parameter(data::pp(v),data::pp(v.sort()));
278 }
279}
280
282{
283 return action_label_string(pp(l_in));
284}
285
286inline void lts_convert_base_class(const lts_lts_base& base_in,
287 lts_fsm_base& base_out,
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
301{
302 state_label_out.clear();
303 std::size_t i=0;
304 state_label_lts local_state_label_in;
305 if (state_label_in.size()!=1)
306 {
307 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 local_state_label_in=state_label_lts(state_label_in.front());
311 static bool warning_is_already_printed=false;
312 if (!warning_is_already_printed)
313 {
314 mCRL2log(log::warning) << "The state label " + pp(state_label_in) + " consists of " + std::to_string(state_label_in.size()) +
315 " state vectors and all but the first label are ignored. This warning is only printed once. ";
316 warning_is_already_printed=true;
317 }
318 }
319 else
320 {
321 local_state_label_in=state_label_in;
322 }
323 for (const data::data_expression& t: *local_state_label_in.begin())
324 {
325 std::map <data::data_expression , std::size_t >::const_iterator index=c.state_element_values_sets[i].find(t);
326 if (index==c.state_element_values_sets[i].end())
327 {
328 const std::size_t element_index=c.state_element_values_sets[i].size();
329 state_label_out.push_back(element_index);
330 c.lts_out.add_state_element_value(i,data::pp(t));
331 c.state_element_values_sets[i][t]=element_index;
332 }
333 else
334 {
335 state_label_out.push_back(index->second);
336 }
337 ++i;
338 }
339}
340
341// ====================== lts -> aut =============================
342
343inline 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
348inline void lts_convert_base_class(const lts_lts_base& base_in,
349 lts_aut_base& base_out,
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
363{
364 return action_label_string(pp(l_in));
365}
366
367inline 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
374template<>
376{
377 public:
378 std::size_t m_state_count;
379
380 convertor(const lts_lts_base& /* lts_base_in */, lts_dot_base& /* lts_base_out */):
381 m_state_count(0)
382 {
383 }
384};
385
386inline void lts_convert_base_class(const lts_lts_base& /* base_in */, lts_dot_base& /* base_out */)
387{
388 // Nothing needs to be done.
389}
390
391inline void lts_convert_base_class(const lts_lts_base& base_in,
392 lts_dot_base& base_out,
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
406{
407 return action_label_string(pp(l_in));
408}
409
411{
412 std::stringstream state_name;
413 state_name << "s" << c.m_state_count;
414 c.m_state_count++;
415 state_label_out=state_label_dot(state_name.str(),pp(state_label_in));
416}
417
418// ====================== fsm -> lts =============================
419
420template<>
422
423{
424 public:
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
436inline 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
441inline 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
461{
462 return translate_label_aux(l1, c.m_lts_out.data(), c.m_typechecker);
463}
464
465inline void lts_convert_translate_state(const state_label_fsm& state_label_in,
466 state_label_lts& state_label_out,
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
510inline void lts_convert_base_class(const lts_fsm_base& base_in, lts_fsm_base& base_out)
511{
512 base_out=base_in;
513}
514
515inline void lts_convert_base_class(const lts_fsm_base& base_in,
516 lts_fsm_base& base_out,
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
529inline 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
535{
536 return l_in;
537}
538
539// ====================== fsm -> aut =============================
540
541inline 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
546inline void lts_convert_base_class(const lts_fsm_base& base_in,
547 lts_aut_base& base_out,
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
561{
562 state_label_out=state_label_empty();
563}
564
566{
567 return l_in;
568}
569
570
571// ====================== fsm -> dot =============================
572
573template<>
575{
576 public:
577 std::size_t m_state_count;
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
586inline 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
591inline void lts_convert_base_class(const lts_fsm_base& base_in,
592 lts_dot_base& base_out,
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
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
625{
626 return l_in;
627}
628
629
630// ====================== aut -> lts =============================
631
632template<>
634{
635 public:
638
639 convertor(const lts_aut_base& /* lts_base_in*/, const lts_lts_base& lts_base_out)
640 : m_data(lts_base_out.data()),
641 m_typechecker(m_data, data::variable_list(), lts_base_out.action_label_declarations())
642 {
643 }
644};
645
646inline void lts_convert_base_class(const lts_aut_base& /* base_in */, lts_lts_base& /* base_out */)
647{
648 throw mcrl2::runtime_error("Cannot translate .aut into .lts format without additional information (data, action declarations and process parameters)");
649}
650
651inline 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 if (extra_data_is_defined)
659 {
660 base_out.set_data(data);
661 base_out.set_action_label_declarations(action_labels);
662 base_out.set_process_parameters(process_parameters);
663 }
664 else
665 {
666 lts_convert_base_class(base_in,base_out);
667 }
668}
669
671{
672 return translate_label_aux(l_in, c.m_data, c.m_typechecker);
673}
674
675inline 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 state_label_out=state_label_lts();
679}
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
688inline 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
694inline void lts_convert_base_class(const lts_aut_base& base_in,
695 lts_fsm_base& base_out,
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
709{
710 return l_in;
711}
712
713inline 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
720inline void lts_convert_base_class(const lts_aut_base& base_in, lts_aut_base& base_out)
721{
722 base_out=base_in;
723}
724
725inline void lts_convert_base_class(const lts_aut_base& base_in,
726 lts_aut_base& base_out,
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
740{
741 state_label_out=state_label_in;
742}
743
745{
746 return l_in;
747}
748
749// ====================== aut -> dot =============================
750
751inline 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
756inline void lts_convert_base_class(const lts_aut_base& base_in,
757 lts_dot_base& base_out,
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
770inline 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
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.
788template < class STATE_LABEL1, class ACTION_LABEL1, class LTS_BASE1, class STATE_LABEL2, class ACTION_LABEL2, class LTS_BASE2>
791{
792 convertor<LTS_BASE1, LTS_BASE2> c(lts_in, lts_out);
793
794 if (lts_in.has_state_info())
795 {
796 for (std::size_t i=0; i<lts_in.num_states(); ++i)
797 {
798 STATE_LABEL2 s;
799 lts_convert_translate_state(lts_in.state_label(i), s, c);
800 lts_out.add_state(s);
801 }
802 }
803 else
804 {
805 lts_out.set_num_states(lts_in.num_states(),false);
806 }
807
808 for (std::size_t i=0; i<lts_in.num_action_labels(); ++i)
809 {
810 lts_out.add_action(lts_convert_translate_label(lts_in.action_label(i),c));
811 }
812
813 const std::vector<transition>& trans=lts_in.get_transitions();
814 for (const transition& t: trans)
815 {
816 lts_out.add_transition(t);
817 }
818 lts_out.set_initial_state(lts_in.initial_state());
819
820 lts_out.set_hidden_label_set(lts_in.hidden_label_set());
821}
822
823// ====================== lts -> lts =============================
824
825template < class STATE_LABEL1, class ACTION_LABEL1, class LTS_BASE1, class STATE_LABEL2, class ACTION_LABEL2, class LTS_BASE2>
828{
829 lts_convert_base_class(static_cast<const LTS_BASE1&>(lts_in), static_cast<LTS_BASE2&>(lts_out));
830 lts_convert_aux<STATE_LABEL1, ACTION_LABEL1, LTS_BASE1,STATE_LABEL2, ACTION_LABEL2, LTS_BASE2>(lts_in,lts_out);
831}
832
833template < class STATE_LABEL1, class ACTION_LABEL1, class LTS_BASE1,
834 class STATE_LABEL2, class ACTION_LABEL2, class LTS_BASE2>
837 const data::data_specification& ds,
839 const data::variable_list& vl,
840 const bool extra_data_is_defined=true)
841{
842 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 lts_convert_aux<STATE_LABEL1, ACTION_LABEL1, LTS_BASE1,STATE_LABEL2, ACTION_LABEL2, LTS_BASE2>(lts_in,lts_out);
844}
845
846// ====================== probabilistic_lts -> lts =============================
847
848template < class STATE_LABEL1, class ACTION_LABEL1, class PROBABILISTIC_STATE1, class LTS_BASE1, class STATE_LABEL2, class ACTION_LABEL2, class LTS_BASE2>
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
878template < class STATE_LABEL1, class ACTION_LABEL1, class LTS_BASE1, class PROBABILISTIC_STATE1, class STATE_LABEL2, class ACTION_LABEL2, class LTS_BASE2>
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
889template < class STATE_LABEL1, class ACTION_LABEL1, class PROBABILISTIC_STATE1, class LTS_BASE1,
890 class STATE_LABEL2, class ACTION_LABEL2, class LTS_BASE2>
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
904template < class STATE_LABEL1, class ACTION_LABEL1, class LTS_BASE1,
905 class STATE_LABEL2, class ACTION_LABEL2, class PROBABILISTIC_STATE2, class LTS_BASE2>
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
917template < class STATE_LABEL1, class ACTION_LABEL1, class LTS_BASE1, class STATE_LABEL2, class ACTION_LABEL2, class PROBABILISTIC_STATE2, class LTS_BASE2>
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
925template < class STATE_LABEL1, class ACTION_LABEL1, class LTS_BASE1,
926 class STATE_LABEL2, class ACTION_LABEL2, class PROBABILISTIC_STATE2, class LTS_BASE2>
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
940template < 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>
944{
946 for(std::size_t i=0; i< lts_in.num_probabilistic_states(); ++i)
947 {
948 lts_out.add_probabilistic_state(lts_convert_probabilistic_state<PROBABILISTIC_STATE1,PROBABILISTIC_STATE2>(lts_in.probabilistic_state(i)));
949 }
950 lts_out.set_initial_probabilistic_state(lts_convert_probabilistic_state<PROBABILISTIC_STATE1,PROBABILISTIC_STATE2>(lts_in.initial_probabilistic_state()));
951}
952
953
954template < 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>
958{
959 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 translate_probability_labels(lts_in,lts_out);
962}
963
964template < 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>
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
Iterator for term_list.
size_type size() const
Returns the size of the term_list.
Definition aterm_list.h:255
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
Definition aterm_list.h:281
const Term & front() const
Returns the first element of the list.
Definition aterm_list.h:238
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Definition aterm_list.h:274
bool empty() const
Returns true if the list's size is 0.
Definition aterm_list.h:267
A vector class in which aterms can be stored.
Definition vector.h:34
An application of a data expression to a number of arguments.
const data_expression & head() const
Get the function at the head of this expression.
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:107
data_expression typecheck_data_expression(const data_expression &x, const sort_expression &expected_sort, const detail::variable_context &variable_context)
Definition typecheck.h:75
void add_context_variables(const VariableContainer &variables)
\brief A data variable
Definition variable.h:28
A class containing the values for action labels for the .lts format.
Definition lts_lts.h:137
This class contains strings to be used as values for action labels in lts's.
convertor(const lts_aut_base &, const lts_lts_base &lts_base_out)
convertor(const lts_fsm_base &lts_base_in, const lts_dot_base &)
convertor(const lts_fsm_base &lts_base_in, lts_lts_base &lts_base_out)
convertor(const lts_lts_base &, lts_dot_base &)
std::vector< std::map< data::data_expression, std::size_t > > state_element_values_sets
convertor(const lts_lts_base &lts_base_in, lts_fsm_base &lts_base_out)
convertor(const BASE_LTS_IN &, const BASE_LTS_OUT &)
void clear_process_parameters()
Clear the state parameters for this LTS.
Definition lts_fsm.h:219
void add_process_parameter(const std::string &name, const std::string &sort)
Set the state parameters for this LTS.
Definition lts_fsm.h:229
a base class for lts_lts_t and probabilistic_lts_t.
Definition lts_lts.h:271
void set_process_parameters(const data::variable_list &params)
Set the state parameters for this LTS.
Definition lts_lts.h:358
void set_action_label_declarations(const process::action_label_list &decls)
Set the action label information for this LTS.
Definition lts_lts.h:322
const data::variable_list & process_parameters() const
Return the process parameters stored in this LTS.
Definition lts_lts.h:337
void set_data(const data::data_specification &spec)
Set the mCRL2 data specification of this LTS.
Definition lts_lts.h:330
A class that contains a labelled transition system.
Definition lts.h:83
states_size_type num_states() const
Gets the number of states of this LTS.
Definition lts.h:245
This class contains labels for probabilistic transistions, consisting of a numerator and a denominato...
A class that contains a labelled transition system.
void set_initial_probabilistic_state(const PROBABILISTIC_STATE_T &state)
Sets the probabilistic initial state number of this LTS.
const PROBABILISTIC_STATE_T & initial_probabilistic_state() const
Gets the initial state number of this LTS.
labels_size_type num_probabilistic_states() const
Gets the number of probabilistic states of this LTS.
void clear_probabilistic_states()
Clear the probabilistic states in this probabilistic transitions system.
states_size_type add_probabilistic_state(const PROBABILISTIC_STATE_T &s)
Adds a probabilistic state to this LTS.
const PROBABILISTIC_STATE_T & probabilistic_state(const states_size_type index) const
Gets the probabilistic label of an index.
A class that contains a probabilistic state.
This class contains labels for states in dot format.
Definition lts_dot.h:37
Contains empty state values, used for lts's without state valued.
This class contains state labels for the fsm format.
Definition lts_fsm.h:38
This class contains state labels for an labelled transition system in .lts format.
Definition lts_lts.h:40
A class containing triples, source label and target representing transitions.
Definition transition.h:43
Standard exception class for reporting runtime errors.
Definition exception.h:27
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
This file contains a class that contains labelled transition systems in aut format.
This file contains a class that contains labelled transition systems in dot format.
This file contains a class that contains labelled transition systems in fsm format.
This file contains a class that contains labelled transition systems in lts (mcrl2) format.
std::string pp(const detail::lhs_t &lhs)
bool is_integer_constant(const data_expression &n)
Determines whether n is an integer constant.
bool is_positive_constant(const data_expression &n)
Determines whether n is a positive constant.
const function_symbol & creal()
Constructor for function symbol @cReal.
Definition real.h:107
data_expression parse_data_expression(std::istream &in, const VariableContainer &variables, const data_specification &dataspec=detail::default_specification(), bool type_check=true, bool translate_user_notation=true, bool normalize_sorts=true)
Parses and type checks a data expression.
Definition parse.h:276
std::string pp(const abstraction &x)
Definition data.cpp:39
@ warning
Definition logger.h:32
void translate_probability_labels(const probabilistic_lts< STATE_LABEL1, ACTION_LABEL1, PROBABILISTIC_STATE1, LTS_BASE1 > &lts_in, probabilistic_lts< STATE_LABEL2, ACTION_LABEL2, PROBABILISTIC_STATE2, LTS_BASE2 > &lts_out)
void lts_convert(const lts< STATE_LABEL1, ACTION_LABEL1, LTS_BASE1 > &lts_in, lts< STATE_LABEL2, ACTION_LABEL2, LTS_BASE2 > &lts_out)
void lts_convert_aux(const lts< STATE_LABEL1, ACTION_LABEL1, LTS_BASE1 > &lts_in, lts< STATE_LABEL2, ACTION_LABEL2, LTS_BASE2 > &lts_out)
probabilistic_arbitrary_precision_fraction translate_probability_data_to_arbitrary_size_probability(const data::data_expression &d)
Translate a fraction given as a data_expression to a representation with an arbitrary size fraction.
Definition lts_convert.h:37
void lts_convert_base_class(const lts_lts_base &base_in, lts_lts_base &base_out)
void remove_probabilities(const probabilistic_lts< STATE_LABEL1, ACTION_LABEL1, PROBABILISTIC_STATE1, LTS_BASE1 > &lts_in, lts< STATE_LABEL2, ACTION_LABEL2, LTS_BASE2 > &lts_out)
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 > &)
mcrl2::lts::probabilistic_arbitrary_precision_fraction translate_probability_data_prob(const data::data_expression &d)
Definition lts_convert.h:92
PROBABILISTIC_STATE2 lts_convert_probabilistic_state(const PROBABILISTIC_STATE1 &)
Definition lts_convert.h:50
action_label_lts translate_label_aux(const action_label_string &l1, const data::data_specification &data, lps::multi_action_type_checker &typechecker)
void add_probabilities(const lts< STATE_LABEL1, ACTION_LABEL1, LTS_BASE1 > &lts_in, probabilistic_lts< STATE_LABEL2, ACTION_LABEL2, PROBABILISTIC_STATE2, LTS_BASE2 > &lts_out)
action_label_lts lts_convert_translate_label(const action_label_lts &l_in, convertor< lts_lts_base, lts_lts_base > &)
action_label_lts parse_lts_action(const std::string &multi_action_string, const data::data_specification &data_spec, lps::multi_action_type_checker &typechecker)
Parse a string into an action label.
Definition lts_lts.h:208
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
STL namespace.