LCOV - code coverage report
Current view: top level - lps/source - lpsparunfoldlib.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 358 443 80.8 %
Date: 2020-02-28 00:44:21 Functions: 22 23 95.7 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Frank Stappers, Jeroen Keiren
       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 lpsparunfoldlib.cpp
      11             : *
      12             : * \brief This file contains the code for the tool lpsparunfold that allows to replace
      13             : *        complex data types by simpler ones.
      14             : */
      15             : 
      16             : #include "mcrl2/lps/lpsparunfoldlib.h"
      17             : #include "mcrl2/lps/replace.h"
      18             : 
      19             : using namespace std;
      20             : using namespace mcrl2;
      21             : using namespace mcrl2::core;
      22             : using namespace mcrl2::data;
      23             : using namespace mcrl2::log;
      24             : 
      25             : /* Remarks
      26             : - replace on vectors does not work
      27             : - vector pretty print does not work
      28             : - alias::name() [basic_sort] results in a basic sort, differs form basic_sort::name() [string]
      29             : */
      30             : 
      31           1 : lpsparunfold::lpsparunfold(mcrl2::lps::stochastic_specification spec,
      32             :     std::map< mcrl2::data::sort_expression , lspparunfold::unfold_cache_element > *cache,
      33             :     bool add_distribution_laws
      34           1 : )
      35             :   : 
      36             :     m_cache(cache),
      37           1 :     m_data_specification(spec.data()),
      38             :     m_representative_generator(m_data_specification),
      39           1 :     m_lps(spec.process()),
      40           1 :     m_glob_vars(spec.global_variables()),
      41           1 :     m_init_process(spec.initial_process()),
      42           1 :     m_action_label_list(spec.action_labels()),
      43           6 :     m_add_distribution_laws(add_distribution_laws)
      44             : {
      45           1 :   mCRL2log(debug) << "Processing" << std::endl;
      46             : 
      47           1 :   m_identifier_generator.add_identifiers(mcrl2::lps::find_identifiers(spec));
      48             : 
      49           3 :   for (const sort_expression& s:  m_data_specification.sorts())
      50             :   {
      51           2 :     if (is_basic_sort(s))
      52             :     {
      53           2 :       sort_names.insert((basic_sort(s)).name());
      54             :     }
      55             :   };
      56             : 
      57           1 :   m_identifier_generator.add_identifiers(sort_names);
      58             : 
      59             :   {
      60           1 :     std::size_t size = mapping_and_constructor_names.size();
      61           5 :     for (const function_symbol& f: m_data_specification.constructors()) 
      62             :     {
      63           4 :       mapping_and_constructor_names.insert(f.name());
      64             :     };
      65           1 :     mCRL2log(debug) << "- Specification has " <<   mapping_and_constructor_names.size() - size << " constructors" << std::endl;
      66             :   }
      67             : 
      68             :   {
      69           1 :     std::size_t size = mapping_and_constructor_names.size();
      70          27 :     for (const function_symbol& f: m_data_specification.mappings())
      71             :     {
      72          26 :       mapping_and_constructor_names.insert(f.name());
      73             :     };
      74           1 :     mCRL2log(debug) << "- Specification has " <<  mapping_and_constructor_names.size() - size << " mappings " << std::endl;
      75             :   }
      76             : 
      77           1 :   m_identifier_generator.add_identifiers(mapping_and_constructor_names);
      78           1 : }
      79             : 
      80           1 : mcrl2::data::basic_sort lpsparunfold::generate_fresh_basic_sort(const std::string& str)
      81             : {
      82             :   //Generate a fresh Basic Sort
      83           2 :   mcrl2::core::identifier_string nstr = m_identifier_generator(str);
      84           1 :   mCRL2log(verbose) << "Generated fresh sort \"" <<  string(nstr) << "\" for \"" <<  str << "\"" << std::endl;
      85           1 :   sort_names.insert(nstr);
      86           2 :   return basic_sort(std::string(nstr));
      87             : }
      88             : 
      89           6 : mcrl2::core::identifier_string lpsparunfold::generate_fresh_constructor_and_mapping_name(std::string str)
      90             : {
      91             :   //Generate a fresh name for a constructor of mapping
      92             : 
      93           6 :   str.resize(std::remove_if(str.begin(), str.end(), &char_filter) - str.begin());
      94             : 
      95           6 :   mcrl2::core::identifier_string nstr = m_identifier_generator(str);
      96           6 :   mCRL2log(debug) << "Generated a fresh mapping: " <<  string(nstr) << std::endl;
      97           6 :   mapping_and_constructor_names.insert(nstr);
      98           6 :   return nstr;
      99             : }
     100             : 
     101           1 : function_symbol_vector lpsparunfold::determine_affected_constructors()
     102             : {
     103           2 :   function_symbol_vector t = m_data_specification.constructors(m_unfold_process_parameter);
     104           1 :   function_symbol_vector k = function_symbol_vector(t.begin(), t.end());
     105             : 
     106           1 :   mCRL2log(debug) << "k:\t";
     107           1 :   mCRL2log(verbose) << "" <<  unfold_parameter_name  << " has " <<  k.size() << " constructor function(s)" << std::endl;
     108             : 
     109           3 :   for (const function_symbol& f: k)
     110             :   {
     111           2 :     mCRL2log(debug) << "\t" <<  f << std::endl;
     112             :   }
     113           2 :   return k;
     114             : }
     115             : 
     116             : 
     117           1 : function_symbol_vector lpsparunfold::new_constructors(mcrl2::data::function_symbol_vector affected_constructors)
     118             : {
     119             :   using namespace mcrl2::data;
     120             : 
     121           1 :   function_symbol_vector elements_of_new_sorts;
     122             : 
     123           3 :   for (const function_symbol& func: affected_constructors)
     124             :   {
     125             : 
     126           4 :     std::string prefix = "c_";
     127           4 :     mcrl2::core::identifier_string fresh_name = generate_fresh_constructor_and_mapping_name(prefix.append(func.name()));
     128           4 :     const data::function_symbol f(fresh_name , fresh_basic_sort);
     129           2 :     elements_of_new_sorts.push_back(f);
     130           2 :     m_data_specification.add_constructor(f);
     131           2 :     mCRL2log(debug) << "\t" << data::function_symbol(fresh_name , fresh_basic_sort) << std::endl;
     132           2 :     mapping_and_constructor_names.insert(fresh_name);
     133             : 
     134             :   }
     135           1 :   mCRL2log(debug) << "- Created " <<  elements_of_new_sorts.size() << " fresh \" c_ \" constructor(s)" << std::endl;
     136           1 :   return elements_of_new_sorts;
     137             : }
     138             : 
     139           1 : mcrl2::data::function_symbol lpsparunfold::create_case_function(std::size_t k)
     140             : {
     141           1 :   mcrl2::data::function_symbol fs;
     142           2 :   std::string str = "C_";
     143           1 :   str.append(fresh_basic_sort.name()).append("_");
     144           2 :   mcrl2::core::identifier_string idstr = generate_fresh_constructor_and_mapping_name(str);
     145           2 :   mcrl2::data::sort_expression_vector fsl;
     146           1 :   fsl.push_back(fresh_basic_sort);
     147           3 :   for (std::size_t i = 0; i < k; ++i)
     148             :   {
     149           2 :     fsl.push_back(m_unfold_process_parameter);
     150             :   }
     151             : 
     152           1 :   fs = data::function_symbol(idstr , mcrl2::data::function_sort(fsl, m_unfold_process_parameter));
     153             : 
     154           1 :   mCRL2log(debug) << "- Created C map: " << fs << std::endl;
     155             : 
     156           2 :   return fs;
     157             : }
     158             : 
     159           1 : mcrl2::data::function_symbol lpsparunfold::create_determine_function()
     160             : {
     161           1 :   mcrl2::data::function_symbol fs;
     162           2 :   std::string str = "Det_";
     163           1 :   str.append(string(fresh_basic_sort.name()).append("_"));
     164           2 :   mcrl2::core::identifier_string idstr = generate_fresh_constructor_and_mapping_name(str);
     165           2 :   mcrl2::data::sort_expression_list fsl;
     166           1 :   fs = data::function_symbol(idstr , mcrl2::data::make_function_sort(m_unfold_process_parameter , fresh_basic_sort));
     167           1 :   mCRL2log(debug) << "\t" <<  fs << std::endl;
     168             : 
     169           2 :   return fs;
     170             : }
     171             : 
     172           1 : mcrl2::data::function_symbol_vector lpsparunfold::create_projection_functions(function_symbol_vector affected_constructors)
     173             : {
     174           1 :   mcrl2::data::function_symbol_vector sfs;
     175           2 :   std::string str = "pi_";
     176           1 :   str.append(string(fresh_basic_sort.name()).append("_"));
     177             : 
     178           2 :   std::set<mcrl2::data::sort_expression> processed;
     179           3 :   for (const function_symbol& f: affected_constructors)
     180             :   {
     181           2 :     if (is_function_sort(f.sort()))
     182             :     {
     183           2 :       function_sort fs = function_sort(f.sort());
     184           1 :       const sort_expression_list& sel  = fs.domain();
     185           3 :       for (sort_expression_list::const_iterator j = sel.begin(); j != sel.end(); j++)
     186             :       {
     187           4 :         mcrl2::core::identifier_string idstr = generate_fresh_constructor_and_mapping_name(str);
     188           4 :         data::function_symbol map(idstr , mcrl2::data::make_function_sort(m_unfold_process_parameter , *j));
     189           2 :         m_data_specification.add_mapping(map);
     190           2 :         sfs.push_back(map);
     191           2 :         processed.insert(*j);
     192             :       }
     193             :     }
     194             :   }
     195           3 :   for (const function_symbol& f: sfs)
     196             :   {
     197           2 :     mCRL2log(debug) << "\t" << f << std::endl;
     198             :   }
     199           2 :   return sfs;
     200             : }
     201             : 
     202           9 : void lpsparunfold::add_new_equation(const data_expression& lhs, const data_expression& rhs)
     203             : {
     204           9 :   mCRL2log(verbose) << "- Added equation " <<  data::pp(data_equation(lhs, rhs)) << std::endl;
     205          18 :   set< variable > svars = find_all_variables(lhs);
     206          18 :   set< variable > tmp_var = find_all_variables(rhs);
     207           9 :   svars.insert(tmp_var.begin(), tmp_var.end());
     208           9 :   m_data_specification.add_equation(data_equation(variable_list(svars.begin(), svars.end()), lhs, rhs));
     209           9 : }
     210             : 
     211           1 : std::map<function_symbol, data_expression_vector> lpsparunfold::create_arguments_map(const function_symbol_vector& affected_constructors)
     212             : {
     213           2 :   std::string dstr = "d";
     214           1 :   std::map<function_symbol, data_expression_vector> result;
     215             : 
     216             :   // The two data structures below are used to allow the reuse of variables names.
     217           2 :   std::map< sort_expression, variable_vector > sort_vars;  /* Mapping for Sort |-> [Variable] */
     218           2 :   std::map< sort_expression, std::size_t > sort_index;          /* Mapping for counting the number of unique Sorts of an equation */
     219             : 
     220           3 :   for (const function_symbol& f: affected_constructors)
     221             :   {
     222           4 :     data_expression_vector arguments;
     223           2 :     if (is_function_sort(f.sort()))
     224             :     {
     225           1 :       const function_sort& fs = atermpp::down_cast<function_sort>(f.sort()); 
     226           3 :       for (const sort_expression& sort: fs.domain())
     227             :       {
     228           2 :         if (sort_vars[sort].size() == sort_index[sort])
     229             :         {
     230           4 :           variable v(m_identifier_generator(dstr), sort);
     231           2 :           sort_vars[sort].push_back(v);
     232             :         }
     233           4 :         variable y = sort_vars[sort].at(sort_index[sort]);
     234           2 :         sort_index[sort] = sort_index[sort]+1;
     235           2 :         arguments.push_back(y);
     236             :       }
     237             :     }
     238           2 :     result[f]=arguments;
     239             :   }
     240           2 :   return result;
     241             : }
     242             : 
     243           1 : void lpsparunfold::create_data_equations(
     244             :                 const function_symbol_vector& projection_functions,
     245             :                 const data::function_symbol& case_function,
     246             :                 function_symbol_vector elements_of_new_sorts,
     247             :                 const function_symbol_vector& affected_constructors,
     248             :                 const data::function_symbol& determine_function)
     249             : {
     250           2 :   variable_vector vars;        /* Equation variables  */
     251           2 :   std::set<mcrl2::core::identifier_string> var_names; /* var_names */
     252             : 
     253           2 :   std::string cstr = "c";
     254             : 
     255             :   /* Creating variable for detector function */
     256           2 :   mcrl2::core::identifier_string istr = m_identifier_generator(cstr);
     257           2 :   variable v = variable(istr, fresh_basic_sort);
     258           1 :   vars.push_back(v);
     259             : 
     260             :   /* Create Equations */
     261           1 :   if (m_add_distribution_laws)
     262             :   {
     263           0 :     mCRL2log(verbose) << "Adding equations with additional distribution laws..." << std::endl;
     264             :   }
     265             :   else
     266             :   {
     267           1 :     mCRL2log(verbose) << "Adding equations..." << std::endl;
     268             :   }
     269             : 
     270           1 :   generate_case_functions(elements_of_new_sorts, case_function);
     271             : 
     272           2 :   const std::map<function_symbol, data_expression_vector> constructors_argument_map=create_arguments_map(affected_constructors);
     273             : 
     274           1 :   std::size_t element_of_new_sort_index = 0;
     275           1 :   std::size_t projection_function_index = 0;
     276           3 :   for (const function_symbol& f: affected_constructors)
     277             :   {
     278             :     /* Creating an equation for the detector function */
     279           4 :     data_expression_vector function_arguments=constructors_argument_map.at(f);
     280           5 :     data_expression lhs = (function_arguments.empty()?application(determine_function, f):
     281           7 :                                        application(determine_function , application(f, function_arguments.begin(), function_arguments.end())));
     282           2 :     add_new_equation(lhs, elements_of_new_sorts[element_of_new_sort_index]);
     283             : 
     284           2 :     if (is_function_sort(f.sort()))
     285             :     {
     286           2 :       function_sort fs = function_sort(f.sort());
     287             : 
     288             :       /* Equations for projection functions */
     289           3 :       for(const data_expression& arg: function_arguments)
     290             :       {
     291           4 :         data_expression lhs = application(projection_functions.at(projection_function_index), 
     292           8 :                                           application(f, function_arguments.begin(), function_arguments.end()));
     293           2 :         add_new_equation(lhs,arg);
     294             : 
     295             :         // Add default values if the projection functions are applied to constructors they are not intended for.
     296             :         // The advantage of this is that this simplifies expressions, and it allows to sometimes remove more variables
     297             :         // using constant elimination.
     298           6 :         for(const function_symbol& alternative_f: affected_constructors)
     299             :         {
     300           4 :           if (alternative_f!=f && f.sort().target_sort()==alternative_f.sort().target_sort())
     301             :           {
     302           4 :             data_expression_vector arguments_of_alternative_f = constructors_argument_map.at(alternative_f);
     303           4 :             data_expression lhs;
     304           2 :             if (arguments_of_alternative_f.empty())
     305             :             {
     306           2 :               lhs = application(projection_functions.at(projection_function_index),alternative_f);
     307             :             }
     308             :             else
     309             :             {
     310           0 :               lhs = application(projection_functions.at(projection_function_index), 
     311           0 :                                 application(alternative_f, 
     312             :                                             arguments_of_alternative_f.begin(), 
     313             :                                             arguments_of_alternative_f.end()));
     314             :             }
     315             :             try
     316             :             {
     317           4 :               data_expression rhs = m_representative_generator(lhs.sort());
     318           2 :               add_new_equation(lhs,rhs);
     319             :             }
     320           0 :             catch (mcrl2::runtime_error& e)
     321             :             {
     322           0 :               mCRL2log(debug) << "Failed to generate equation " << lhs << "= ... as no default term of sort " << lhs.sort() << 
     323           0 :                                  " could be generated.\n" << e.what() << "\n";
     324             :             }
     325             :           }
     326             :         }
     327             : 
     328           2 :         if (m_add_distribution_laws)
     329             :         {
     330             :           /* Add additional distribution laws for projection function pi over if
     331             : 
     332             :              pi(if(b,x,y))=if(b,pi(x),pi(y));
     333             :           */
     334           0 :           sort_expression if_arg_sort(function_sort(projection_functions.at(projection_function_index).sort()).domain().front());
     335           0 :           data::function_symbol if_function_symbol("if", make_function_sort(sort_bool::bool_(), if_arg_sort, if_arg_sort , if_arg_sort));
     336           0 :           m_data_specification.add_equation(create_distribution_law_over_case(projection_functions.at(projection_function_index), if_function_symbol, false));
     337             :           /* Add additional distribution laws for projection function pi over case
     338             : 
     339             :              pi(C(projection_function_index,x1,x2,...))=C(projection_function_index,pi(x1),pi(x2),...);
     340             :           */
     341           0 :           const data_equation equation=create_distribution_law_over_case(projection_functions.at(projection_function_index), case_function, true);
     342           0 :           m_data_specification.add_equation(equation);
     343             : 
     344             :           /* Create additional case function */
     345           0 :           generate_case_functions(elements_of_new_sorts, atermpp::down_cast<function_symbol>(application(equation.rhs()).head()));
     346             :         }
     347           2 :         projection_function_index++;
     348             :       }
     349             :     }
     350           2 :     element_of_new_sort_index++;
     351             :   }
     352             : 
     353           1 :   if (m_add_distribution_laws)
     354             :   {
     355             :     /*  Add additional distribution laws for Det over if
     356             : 
     357             :                Det(if(b,x,y))=if(b,Det(x),Det(y));
     358             :     */
     359           0 :     sort_expression if_arg_sort(function_sort(determine_function.sort()).domain().front());
     360           0 :     data::function_symbol if_function_symbol("if", make_function_sort(sort_bool::bool_(), if_arg_sort, if_arg_sort , if_arg_sort));
     361           0 :     m_data_specification.add_equation(create_distribution_law_over_case(determine_function, if_function_symbol, false));
     362             : 
     363             :     /*  Add additional distribution laws for Det over case
     364             : 
     365             :         Det(C(e,x1,x2,...))=C(e,Det(x1),Det(x2),...);
     366             :     */
     367           0 :     m_data_specification.add_equation(create_distribution_law_over_case(determine_function, case_function, true));
     368             :   }
     369           1 : }
     370             : 
     371           3 : mcrl2::core::identifier_string lpsparunfold::generate_fresh_process_parameter_name(std::string str, std::set<mcrl2::core::identifier_string>& process_parameter_names)
     372             : {
     373           3 :   mcrl2::core::identifier_string idstr = m_identifier_generator(str.append("_pp"));
     374           3 :   process_parameter_names.insert(idstr);
     375           3 :   return idstr;
     376             : }
     377             : 
     378           1 : void lpsparunfold::unfold_summands(mcrl2::lps::stochastic_action_summand_vector& summands, const mcrl2::data::function_symbol& determine_function, const mcrl2::data::function_symbol_vector& projection_functions)
     379             : {
     380           2 :   for (mcrl2::lps::stochastic_action_summand& summand: summands)
     381             :   {
     382           2 :     mcrl2::data::assignment_list ass = summand.assignments();
     383             :     //Create new left-hand assignment_list & right-hand assignment_list
     384           2 :     mcrl2::data::variable_vector new_ass_left;
     385           2 :     mcrl2::data::data_expression_vector new_ass_right;
     386           2 :     for (const mcrl2::data::assignment& k: ass)
     387             :     {
     388           1 :       if (proc_par_to_proc_par_inj.find(k.lhs()) != proc_par_to_proc_par_inj.end())
     389             :       {
     390           4 :         for (const mcrl2::data::variable& v: proc_par_to_proc_par_inj[ k . lhs() ])
     391             :         {
     392           3 :           new_ass_left.push_back(v);
     393             :         }
     394             : 
     395           2 :         mcrl2::data::data_expression_vector ins = unfold_constructor(k.rhs(), determine_function, projection_functions);
     396             :         //Replace unfold parameters in affected assignments
     397           1 :         new_ass_right.insert(new_ass_right.end(), ins.begin(), ins.end());
     398             :       }
     399             :       else
     400             :       {
     401           0 :         new_ass_left.push_back(k.lhs());
     402           0 :         new_ass_right.push_back(k.rhs());
     403             :       }
     404             :     }
     405             : 
     406           1 :     assert(new_ass_left.size() == new_ass_right.size());
     407           2 :     mcrl2::data::assignment_vector new_ass;
     408           7 :     while (!new_ass_left.empty())
     409             :     {
     410           3 :       new_ass.push_back(mcrl2::data::assignment(new_ass_left.front(), new_ass_right.front()));
     411           3 :       new_ass_left.erase(new_ass_left.begin());
     412           3 :       new_ass_right.erase(new_ass_right.begin());
     413             :     }
     414           1 :     summand.assignments() = mcrl2::data::assignment_list(new_ass.begin(), new_ass.end());
     415             :   }
     416           1 : }
     417             : 
     418           1 : mcrl2::lps::stochastic_linear_process lpsparunfold::update_linear_process(const function_symbol& case_function , function_symbol_vector affected_constructors, const function_symbol& determine_function, std::size_t parameter_at_index, const function_symbol_vector& projection_functions)
     419             : {
     420             :   /* Get process parameters from lps */
     421           2 :   mcrl2::data::variable_list lps_proc_pars =  m_lps.process_parameters();
     422             : 
     423             :   /* Get process_parameters names from lps */
     424           2 :   std::set<mcrl2::core::identifier_string> process_parameter_names;
     425           2 :   for (const mcrl2::data::variable& v: lps_proc_pars)
     426             :   {
     427           1 :     process_parameter_names.insert(v.name());
     428             :   }
     429             : 
     430           1 :   mCRL2log(verbose) << "Updating LPS..." << std::endl;
     431             :   /* Create new process parameters */
     432           2 :   mcrl2::data::variable_vector new_process_parameters;
     433           2 :   for (mcrl2::data::variable_list::iterator i = lps_proc_pars.begin();
     434           2 :        i != lps_proc_pars.end();
     435             :        ++i)
     436             :   {
     437           1 :     if (static_cast<std::size_t>(std::distance(lps_proc_pars.begin(), i)) == parameter_at_index)
     438             :     {
     439           1 :       mCRL2log(verbose) << "Unfolding parameter " << i->name() << " at index " << std::distance(lps_proc_pars.begin(), i) << "..." << std::endl;
     440           2 :       mcrl2::data::variable_vector process_parameters_injection;
     441             : 
     442             :       /* Generate fresh process parameter for new Sort */
     443           2 :       mcrl2::core::identifier_string idstr = generate_fresh_process_parameter_name(unfold_parameter_name, process_parameter_names);
     444           1 :       process_parameters_injection.push_back(mcrl2::data::variable(idstr , fresh_basic_sort));
     445             : 
     446           1 :       mCRL2log(verbose) << "- Created process parameter " <<  data::pp(process_parameters_injection.back()) << " of type " <<  data::pp(fresh_basic_sort) << "" << std::endl;
     447             : 
     448           3 :       for (mcrl2::data::function_symbol_vector::iterator j = affected_constructors.begin()
     449           3 :            ; j != affected_constructors.end()
     450             :            ; ++j)
     451             :       {
     452           2 :         bool processed = false;
     453           2 :         if (is_function_sort(j -> sort()))
     454             :         {
     455           2 :           sort_expression_list dom = function_sort(j -> sort()).domain();
     456           3 :           for (sort_expression_list::iterator k = dom.begin(); k != dom.end(); ++k)
     457             :           {
     458           4 :             mcrl2::core::identifier_string idstr = generate_fresh_process_parameter_name(unfold_parameter_name, process_parameter_names);
     459           2 :             process_parameters_injection.push_back(mcrl2::data::variable(idstr ,  *k));
     460           2 :             mCRL2log(verbose) << "- Injecting process parameter: " <<  idstr << "::" <<  *k << std::endl;
     461             :           }
     462           1 :           processed = true;
     463             :         }
     464             : 
     465           2 :         if (is_basic_sort(j -> sort()))
     466             :         {
     467           1 :           mCRL2log(debug) << "- No processed parameter are injected for basic sort: " <<  *j << std::endl;
     468           1 :           processed = true;
     469             :         }
     470             : 
     471           2 :         if (is_structured_sort(j -> sort()))
     472             :         {
     473           0 :           processed = true;
     474             :         }
     475             : 
     476           2 :         if (is_container_sort(j -> sort()))
     477             :         {
     478           0 :           processed = true;
     479             :         }
     480           2 :         if (!processed)
     481             :         {
     482           0 :           mCRL2log(mcrl2::log::debug) << *j << " is not processed" << endl;
     483           0 :           mCRL2log(mcrl2::log::debug) << *j << endl;
     484           0 :           abort();
     485             :         }
     486             :       }
     487           1 :       new_process_parameters.insert(new_process_parameters.end(), process_parameters_injection.begin(), process_parameters_injection.end());
     488             : 
     489             :       /* store mapping: process parameter -> process parameter injection:
     490             :          Required for process parameter replacement in summands
     491             :       */
     492           1 :       proc_par_to_proc_par_inj[*i] = process_parameters_injection;
     493             : 
     494             :     }
     495             :     else
     496             :     {
     497           0 :       new_process_parameters.push_back(*i);
     498             :     }
     499             :   }
     500           1 :   mCRL2log(debug) << "- New LPS process parameters: " <<  mcrl2::data::pp(new_process_parameters) << std::endl;
     501             : 
     502             :   //Prepare parameter substitution
     503           2 :   std::map<mcrl2::data::variable, mcrl2::data::data_expression> parsub = parameter_substitution(proc_par_to_proc_par_inj, affected_constructors, case_function);
     504             : 
     505             :   // TODO: avoid unnecessary copies of the LPS
     506           1 :   mcrl2::lps::stochastic_linear_process new_lps;
     507           1 :   new_lps.action_summands() = m_lps.action_summands();
     508           1 :   new_lps.deadlock_summands() = m_lps.deadlock_summands();
     509             : 
     510             :   // update the summands in new_lps
     511           1 :   unfold_summands(new_lps.action_summands(), determine_function, projection_functions);
     512             : 
     513           1 :   new_lps.process_parameters() = mcrl2::data::variable_list(new_process_parameters.begin(), new_process_parameters.end());
     514             : 
     515           2 :   for (auto i = parsub.begin()
     516           2 :        ; i != parsub.end()
     517             :        ; ++i)
     518             :   {
     519           2 :     mutable_map_substitution< std::map< mcrl2::data::variable , mcrl2::data::data_expression > > s;
     520           1 :     s[ i->first ] = i->second;
     521           1 :     mcrl2::lps::replace_variables( new_lps, s );
     522             :   }
     523             : 
     524           1 :   mCRL2log(debug) << "\nNew LPS:\n" <<  lps::pp(new_lps) << std::endl;
     525             : 
     526           1 :   assert(check_well_typedness(new_lps));
     527             : 
     528           2 :   return new_lps;
     529             : }
     530             : 
     531           1 : mcrl2::lps::stochastic_process_initializer lpsparunfold::update_linear_process_initialization(const data::function_symbol& determine_function, std::size_t parameter_at_index, const function_symbol_vector& projection_functions)
     532             : {
     533             :   //
     534             :   //update inital process
     535             :   //
     536           1 :   mCRL2log(verbose) << "Updating initialization...\n" << std::endl;
     537             : 
     538           2 :   data::assignment_list ass = m_init_process.assignments();
     539             :   //Create new left-hand assignment_list
     540           2 :   mcrl2::data::variable_vector new_ass_left;
     541           2 :   for (mcrl2::data::assignment_list::iterator k = ass.begin()
     542           2 :        ; k != ass.end()
     543             :        ; ++k)
     544             :   {
     545           1 :     if (proc_par_to_proc_par_inj.find(k-> lhs()) != proc_par_to_proc_par_inj.end())
     546             :     {
     547           4 :       for (mcrl2::data::variable_vector::iterator l =  proc_par_to_proc_par_inj[ k -> lhs() ].begin()
     548           4 :            ; l != proc_par_to_proc_par_inj[ k -> lhs() ].end()
     549             :            ; ++l)
     550             :       {
     551           3 :         new_ass_left.push_back(*l);
     552             :       }
     553             :     }
     554             :     else
     555             :     {
     556           0 :       new_ass_left.push_back(k-> lhs());
     557             :     }
     558             :   }
     559             :   //Create new right-hand assignment_list
     560             :   //Unfold parameters
     561           2 :   mcrl2::data::data_expression_vector new_ass_right;
     562           2 :   for (mcrl2::data::assignment_list::iterator k = ass.begin()
     563           2 :        ; k != ass.end()
     564             :        ; ++k)
     565             :   {
     566           1 :     if (static_cast<std::size_t>(std::distance(ass.begin(), k)) == parameter_at_index)
     567             :     {
     568             : 
     569           2 :       mcrl2::data::data_expression_vector ins = unfold_constructor(k -> rhs(), determine_function, projection_functions);
     570             :       //Replace unfold parameters in affected assignments
     571           1 :       new_ass_right.insert(new_ass_right.end(), ins.begin(), ins.end());
     572             :     }
     573             :     else
     574             :     {
     575           0 :       new_ass_right.push_back(k-> rhs());
     576             :     }
     577             :   }
     578             : 
     579           1 :   assert(new_ass_left.size() == new_ass_right.size());
     580           2 :   mcrl2::data::assignment_vector new_ass;
     581           7 :   while (!new_ass_left.empty())
     582             :   {
     583           3 :     new_ass.push_back(mcrl2::data::assignment(new_ass_left.front(), new_ass_right.front()));
     584           3 :     new_ass_left.erase(new_ass_left.begin());
     585           3 :     new_ass_right.erase(new_ass_right.begin());
     586             :   }
     587             : 
     588           1 :   const mcrl2::lps::stochastic_process_initializer new_init(mcrl2::data::assignment_list(new_ass.begin(), new_ass.end()), m_init_process.distribution());
     589           1 :   mCRL2log(debug) << lps::pp(new_init) << std::endl;
     590             : 
     591           2 :   return new_init;
     592             : }
     593             : 
     594           1 : std::map<mcrl2::data::variable, mcrl2::data::data_expression> lpsparunfold::parameter_substitution(std::map<mcrl2::data::variable, mcrl2::data::variable_vector > proc_par_to_proc_par_inj, mcrl2::data::function_symbol_vector affected_constructors, const mcrl2::data::function_symbol& case_function)
     595             : {
     596           1 :   std::map<mcrl2::data::variable, mcrl2::data::data_expression> result;
     597           2 :   data_expression_vector dev;
     598             : 
     599           2 :   set<mcrl2::data::variable_vector::iterator> used_iters;
     600             : 
     601           2 :   mcrl2::data::variable prev;
     602           2 :   for (std::map<mcrl2::data::variable, mcrl2::data::variable_vector >::iterator i = proc_par_to_proc_par_inj.begin()
     603           2 :        ; i != proc_par_to_proc_par_inj.end()
     604             :        ; ++i)
     605             :   {
     606           1 :     if (prev != i->first)
     607             :     {
     608           1 :       dev.clear();
     609             :     }
     610             : 
     611           1 :     dev.push_back(data_expression(i->second.front()));
     612             : 
     613           3 :     for (mcrl2::data::function_symbol_vector::iterator m = affected_constructors.begin()
     614           3 :          ; m != affected_constructors.end()
     615             :          ; ++m)
     616             :     {
     617           2 :       if (is_basic_sort(m -> sort()))
     618             :       {
     619           1 :         dev.push_back(*m);
     620             :       }
     621             : 
     622           2 :       if (is_structured_sort(m -> sort()))
     623             :       {
     624           0 :         dev.push_back(*m);
     625             :       }
     626             : 
     627           2 :       if (is_function_sort(m -> sort()))
     628             :       {
     629           2 :         sort_expression_list dom = function_sort(m -> sort()). domain();
     630           2 :         data_expression_vector arg;
     631             : 
     632           3 :         for (sort_expression_list::iterator n = dom.begin(); n != dom.end(); ++n)
     633             :         {
     634           5 :           for (mcrl2::data::variable_vector::iterator o = i->second.begin()
     635           5 :                ; o != i->second.end()
     636             :                ; ++o)
     637             :           {
     638           5 :             if (o -> sort() == *n && used_iters.find(o) == used_iters.end())
     639             :             {
     640           2 :               used_iters.insert(o);
     641           2 :               arg.push_back(*o);
     642           2 :               break;
     643             :             }
     644             :           }
     645             :         }
     646           1 :         dev.push_back(mcrl2::data::application(*m, arg));
     647             :       }
     648             : 
     649           2 :       if (is_container_sort(m -> sort()))
     650             :       {
     651           0 :         dev.push_back(*m);
     652             :       }
     653             : 
     654             :     }
     655             : 
     656           1 :     mCRL2log(verbose) << "Parameter substitution:\t" << data::pp(i->first) << "\t->\t" <<  data::pp(mcrl2::data::application(case_function, dev)) << std::endl;
     657           1 :     result.insert(std::pair<mcrl2::data::variable, mcrl2::data::data_expression>(i -> first,  mcrl2::data::application(case_function, dev)));
     658             :   }
     659           2 :   return result ;
     660             : }
     661             : 
     662           2 : mcrl2::data::data_expression_vector lpsparunfold::unfold_constructor(const data_expression& de, const data::function_symbol& determine_function, function_symbol_vector projection_functions)
     663             : {
     664           2 :   mcrl2::data::data_expression_vector result;
     665             :   {
     666             :     /* Unfold parameter if function symbol occurs  */
     667             :     /* size of unfold parameter must be equal to 1 */
     668           4 :     data_expression_vector new_ass;
     669             : 
     670             :     /* Det function */
     671           2 :     new_ass.push_back(application(determine_function, de)) ;
     672             : 
     673           6 :     for (const function_symbol& f: projection_functions)
     674             :     {
     675           4 :       new_ass.push_back(application(f, de)) ;
     676             :     }
     677             : 
     678           2 :     result = new_ass;
     679             :   }
     680           2 :   return result;
     681             : }
     682             : 
     683           1 : mcrl2::data::sort_expression lpsparunfold::sort_at_process_parameter_index(std::size_t parameter_at_index)
     684             : {
     685           2 :   mcrl2::data::variable_list lps_proc_pars_list =  m_lps.process_parameters();
     686           2 :   mcrl2::data::variable_vector lps_proc_pars = mcrl2::data::variable_vector(lps_proc_pars_list.begin(), lps_proc_pars_list.end());
     687           1 :   mCRL2log(debug) << "- Number of parameters in LPS: " <<  lps_proc_pars.size() << "" << std::endl;
     688           1 :   mCRL2log(verbose) << "Unfolding process parameter at index: " <<  parameter_at_index << "" << std::endl;
     689           1 :   if (lps_proc_pars.size() <= parameter_at_index)
     690             :   {
     691           0 :     mCRL2log(mcrl2::log::error) << "Given index out of bounds. Index value needs to be in the range [0," << lps_proc_pars.size() <<")." << endl;
     692           0 :     abort();
     693             :   }
     694             : 
     695           1 :   if (is_basic_sort(lps_proc_pars[parameter_at_index].sort()))
     696             :   {
     697           1 :     unfold_parameter_name = basic_sort(lps_proc_pars[parameter_at_index].sort()).name();
     698             :   }
     699             : 
     700           1 :   if (is_structured_sort(lps_proc_pars[parameter_at_index].sort()))
     701             :   {
     702           0 :     mcrl2::core::identifier_string nstr;
     703           0 :     nstr = m_identifier_generator("S");
     704           0 :     sort_names.insert(nstr);
     705           0 :     unfold_parameter_name = nstr;
     706             :   }
     707             : 
     708           1 :   if (is_container_sort(lps_proc_pars[parameter_at_index].sort()))
     709             :   {
     710           0 :     mcrl2::core::identifier_string nstr;
     711           0 :     nstr = m_identifier_generator("S");
     712           0 :     sort_names.insert(nstr);
     713           0 :     unfold_parameter_name = nstr;
     714             :   }
     715             : 
     716           2 :   return lps_proc_pars[parameter_at_index].sort();
     717             : }
     718             : 
     719           0 : mcrl2::data::data_equation lpsparunfold::create_distribution_law_over_case(
     720             :   const mcrl2::data::function_symbol& function_for_distribution,
     721             :   const mcrl2::data::function_symbol& case_function,
     722             :   const bool add_case_function_to_data_type)
     723             : {
     724           0 :   assert(function_sort(case_function.sort()).codomain() == function_sort(function_for_distribution.sort()).domain().front());
     725             : 
     726           0 :   variable_vector variables_used;
     727           0 :   mcrl2::core::identifier_string istr;
     728             : 
     729           0 :   sort_expression_list case_function_sort_arguments = function_sort(case_function.sort()).domain();
     730           0 :   for (sort_expression_list::iterator i = case_function_sort_arguments.begin();
     731           0 :        i != case_function_sort_arguments.end();
     732             :        ++i)
     733             :   {
     734           0 :     if (i == case_function_sort_arguments.begin())
     735             :     {
     736           0 :       istr = m_identifier_generator("b");
     737             :     }
     738             :     else
     739             :     {
     740           0 :       istr = m_identifier_generator("d");
     741             :     }
     742           0 :     variable v(istr, *i);
     743           0 :     variables_used.push_back(v);
     744             :   }
     745             : 
     746           0 :   data_expression lhs(application(function_for_distribution, application(case_function, variables_used)));
     747           0 :   data_expression_vector rw_data_expressions;
     748           0 :   sort_expression_vector rw_sort_expressions;
     749           0 :   for (variable_vector::iterator i = variables_used.begin();
     750           0 :        i != variables_used.end();
     751             :        ++i)
     752             :   {
     753           0 :     if (i == variables_used.begin())
     754             :     {
     755           0 :       rw_data_expressions.push_back(*i);
     756           0 :       rw_sort_expressions.push_back(i->sort());
     757             :     }
     758             :     else
     759             :     {
     760           0 :       rw_data_expressions.push_back(application(function_for_distribution, *i));
     761           0 :       rw_sort_expressions.push_back(function_sort(function_for_distribution.sort()).codomain());
     762             :     }
     763             :   }
     764             : 
     765             :   mcrl2::data::function_symbol new_case_function = data::function_symbol(case_function.name(),
     766           0 :                          function_sort(rw_sort_expressions,function_sort(function_for_distribution.sort()).codomain()));
     767           0 :   if (add_case_function_to_data_type)
     768             :   {
     769           0 :     m_data_specification.add_mapping(new_case_function);
     770           0 :     generate_case_functions(m_data_specification.constructors(function_sort(new_case_function.sort()).domain().front()),new_case_function);   //add equations
     771             :   }
     772             : 
     773             :   /* Generate new case functions for laws */
     774           0 :   application rhs(new_case_function , rw_data_expressions);
     775             : 
     776           0 :   mCRL2log(verbose) << "- Added distribution law for \"" << data::pp(function_for_distribution) << "\" over \"" << data::pp(case_function) << "\": " << data::pp(data_equation(lhs,  rhs)) << std::endl;
     777             : 
     778           0 :   return data_equation(variables_used, lhs, rhs);
     779             : }
     780             : 
     781           1 : void lpsparunfold::generate_case_functions(function_symbol_vector elements_of_new_sorts, const data::function_symbol& case_function)
     782             : {
     783           1 :   mCRL2log(verbose) << "- Generating case function for:\t" <<  mcrl2::data::pp(case_function) << ": " <<  mcrl2::data::pp(case_function.sort()) << "" << std::endl;
     784             : 
     785             :   /* Generate variable identifier string for projection */
     786           2 :   std::string fstr = "y";
     787           2 :   mcrl2::core::identifier_string istr = m_identifier_generator(fstr);
     788             : 
     789           2 :   variable_vector vars;
     790           2 :   sort_expression_list dom = function_sort(case_function.sort()).domain();
     791           4 :   for (const sort_expression& s: dom)
     792             :   {
     793           3 :     istr = m_identifier_generator(fstr);
     794           6 :     variable v(istr, s);
     795           3 :     vars.push_back(v);
     796             :   }
     797             : 
     798           1 :   std::size_t e = 1;
     799           2 :   data_expression_vector sub_args(vars.begin(), vars.end());
     800           3 :   for (std::size_t i = 1 ; i < function_sort(case_function.sort()).domain().size() ; ++i)
     801             :   {
     802           2 :     sub_args[0] = data_expression(elements_of_new_sorts[i-1]);
     803           4 :     data_expression lhs = application(case_function , sub_args);
     804           2 :     add_new_equation(lhs,vars[e]);
     805           2 :     ++e;
     806             :   }
     807             : 
     808             :   {
     809           2 :     data_expression_vector eq_args;
     810             : 
     811           1 :     eq_args = data_expression_vector(function_sort(case_function.sort()).domain().size() -1 , vars.back());
     812           1 :     eq_args.insert(eq_args.begin(), vars.front());
     813             : 
     814           2 :     data_expression lhs = application(case_function , eq_args);
     815           1 :     add_new_equation(lhs, vars.back());
     816             :   }
     817           1 : }
     818             : 
     819           1 : mcrl2::lps::stochastic_specification lpsparunfold::algorithm(std::size_t parameter_at_index)
     820             : {
     821           1 :   m_unfold_process_parameter = sort_at_process_parameter_index(parameter_at_index);
     822             : 
     823             :   /* Var Dec */
     824           2 :   mcrl2::lps::stochastic_linear_process new_lps;
     825           2 :   mcrl2::lps::stochastic_process_initializer new_init;
     826           2 :   function_symbol_vector affected_constructors;
     827           2 :   function_symbol_vector elements_of_new_sorts;
     828           2 :   function_symbol_vector projection_functions;
     829           2 :   data::function_symbol case_function;
     830           2 :   data::function_symbol determine_function;
     831             :   // data_equation_vector data_equations;
     832             : 
     833             :   /* Updating cache*/
     834           1 :   if( m_cache->find(m_unfold_process_parameter) == m_cache->end() )
     835             :   {
     836             :     /* Not using cache */
     837             : 
     838             :     /*   Alg */
     839             :     /*     1 */
     840           1 :     fresh_basic_sort = generate_fresh_basic_sort(unfold_parameter_name);
     841             :     /*     2 */
     842           1 :     affected_constructors = determine_affected_constructors();
     843           1 :     if (affected_constructors.empty())
     844             :     {
     845           0 :       mCRL2log(verbose) << "The selected process parameter " <<  unfold_parameter_name << " has no constructors." << std::endl;
     846           0 :       mCRL2log(verbose) << "No need to unfold." << std::endl;
     847           0 :       new_lps = m_lps;
     848           0 :       new_init = m_init_process;
     849             :     }
     850             :     else
     851             :     {
     852             :       /*     4 */
     853           1 :       elements_of_new_sorts = new_constructors(affected_constructors);
     854             :       /*     6 */
     855           1 :       case_function = create_case_function(affected_constructors.size());
     856             :       /*     7 */
     857           1 :       determine_function = create_determine_function();
     858             :       /*  8-12 */
     859           1 :       projection_functions = create_projection_functions(affected_constructors);
     860             :       /* 13-xx */
     861           1 :       create_data_equations(projection_functions, case_function, elements_of_new_sorts, affected_constructors, determine_function);
     862             : 
     863             :       //Reconstruct data specification, where already quite a number of mappings, constructors and functions have been added.
     864           1 :       m_data_specification.add_sort(fresh_basic_sort);
     865           1 :       m_data_specification.add_mapping(determine_function);
     866           1 :       m_data_specification.add_mapping(case_function);
     867             : 
     868             :       /*----------------*/
     869           1 :       new_lps = update_linear_process(case_function, affected_constructors, determine_function, parameter_at_index, projection_functions);
     870           1 :       new_init = update_linear_process_initialization(determine_function, parameter_at_index, projection_functions);
     871             : 
     872             :       /* Updating cache*/
     873           2 :       lspparunfold::unfold_cache_element e;
     874           1 :       e.cached_case_function = case_function;
     875           1 :       e.cached_k = affected_constructors;
     876           1 :       e.cached_determine_function = determine_function;
     877           1 :       e.cached_projection_functions = projection_functions;
     878           1 :       e.cached_fresh_basic_sort = fresh_basic_sort;
     879             : 
     880           1 :       m_cache->insert( pair<mcrl2::data::sort_expression , lspparunfold::unfold_cache_element>( m_unfold_process_parameter , e ));
     881             :     }
     882             :   }
     883             :   else
     884             :   {
     885             :     /* Using cache */
     886           0 :     mCRL2log(verbose) << "Update using cache for sort: \"" <<  mcrl2::data::pp(m_unfold_process_parameter)  << "\"..." << std::endl;
     887             : 
     888           0 :     std::map< mcrl2::data::sort_expression , lspparunfold::unfold_cache_element >::iterator ce = m_cache->find(m_unfold_process_parameter);
     889             : 
     890           0 :     fresh_basic_sort = ce->second.cached_fresh_basic_sort;
     891           0 :     affected_constructors = ce->second.cached_k;
     892           0 :     if (affected_constructors.empty())
     893             :     {
     894           0 :       mCRL2log(verbose) << "The selected process parameter " <<  unfold_parameter_name << " has no constructors." << std::endl;
     895           0 :       mCRL2log(verbose) << "No need to unfold." << std::endl;
     896           0 :       new_lps = m_lps;
     897           0 :       new_init = m_init_process;
     898             :     }
     899             : 
     900           0 :     case_function = ce->second.cached_case_function;
     901           0 :     determine_function = ce->second.cached_determine_function;
     902           0 :     projection_functions = ce->second.cached_projection_functions;
     903             : 
     904           0 :     new_lps = update_linear_process(case_function, affected_constructors, determine_function, parameter_at_index, projection_functions);
     905           0 :     new_init = update_linear_process_initialization(determine_function, parameter_at_index, projection_functions);
     906             :   }
     907             : 
     908           1 :   mcrl2::lps::stochastic_specification new_spec(m_data_specification, m_action_label_list, m_glob_vars, new_lps, new_init);
     909             : 
     910           1 :   assert(check_well_typedness(new_spec));
     911             : 
     912           2 :   return new_spec;
     913         261 : }

Generated by: LCOV version 1.13