LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts/detail - lts_convert.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 69 90 76.7 %
Date: 2020-07-11 00:44:39 Functions: 11 19 57.9 %
Legend: Lines: hit not hit

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

Generated by: LCOV version 1.13