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

Generated by: LCOV version 1.13