Line data    Source code

       1             : // Author(s): Wieger Wesselink
       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             : /// \file mcrl2/pbes/unify_parameters.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_UNIFY_PARAMETERS_H
      13             : #define MCRL2_PBES_UNIFY_PARAMETERS_H
      14             : 
      15             : #include "mcrl2/data/default_expression_generator.h"
      16             : #include "mcrl2/pbes/pbes_equation_index.h"
      17             : #include "mcrl2/pbes/replace.h"
      18             : #include "mcrl2/pbes/srf_pbes.h"
      19             : 
      20             : namespace mcrl2 {
      21             : 
      22             : namespace pbes_system {
      23             : 
      24             : struct unify_parameters_replace_function
      25             : {
      26             :   // maps propositional variable names to the corresponding parameters
      27             :   const std::map<core::identifier_string, data::variable_list>& propositional_variable_parameters;
      28             : 
      29             :   // generates default expressions for sorts
      30             :   mutable data::default_expression_generator generator;
      31             : 
      32             :   // maps parameters to their new positions
      33             :   mutable std::map<data::variable, std::size_t> parameter_positions;
      34             : 
      35             :   // store the 'missing' parameters for each parameter list
      36             :   mutable std::map<data::variable_list, std::vector<data::variable>> missing_parameters;
      37             : 
      38             :   // the new list of parameters
      39             :   data::variable_list parameters;
      40             : 
      41             :   // reuse this vector for constructing new parameters
      42             :   mutable std::vector<data::data_expression> tmp_parameters;
      43             : 
      44             :   // If true then the newly introduced parameters will be reset to a default value instead of copying the value.
      45             :   bool m_reset = true;
      46             : 
      47           0 :   data::variable_list compute_parameters()
      48             :   {
      49           0 :     std::vector<data::variable> parameter_vector;
      50           0 :     for (const auto& p: propositional_variable_parameters)
      51             :     {
      52           0 :       const data::variable_list& eqn_parameters = p.second;
      53           0 :       for (const data::variable& v: eqn_parameters)
      54             :       {
      55           0 :         auto i = parameter_positions.find(v);
      56           0 :         if (i == parameter_positions.end())
      57             :         {
      58           0 :           parameter_positions[v] = parameter_vector.size();
      59           0 :           parameter_vector.push_back(v);
      60             :         }
      61             :       }
      62             :     }
      63           0 :     return data::variable_list(parameter_vector.begin(), parameter_vector.end());
      64           0 :   }
      65             : 
      66           0 :   unify_parameters_replace_function(
      67             :     const std::map<core::identifier_string, data::variable_list>& propositional_variable_parameters_,
      68             :     const data::data_specification& dataspec,
      69             :     bool reset = true
      70             :   )
      71           0 :     : propositional_variable_parameters(propositional_variable_parameters_), generator(dataspec), m_reset(reset)
      72             :   {
      73             :     using utilities::detail::contains;
      74             : 
      75           0 :     parameters = compute_parameters();
      76           0 :     tmp_parameters.resize(parameters.size());
      77             : 
      78             :     // Compute missing parameters for each equation
      79           0 :     for (const auto& p: propositional_variable_parameters_)
      80             :     {
      81           0 :       const data::variable_list& eqn_parameters = p.second;
      82           0 :       auto i = missing_parameters.find(eqn_parameters);
      83           0 :       if (i != missing_parameters.end())
      84             :       {
      85           0 :         continue;
      86             :       }
      87           0 :       std::set<data::variable> eqn_parameter_set(eqn_parameters.begin(), eqn_parameters.end());
      88           0 :       std::vector<data::variable> missing;
      89           0 :       for (const data::variable& v: parameters)
      90             :       {
      91           0 :         if (!contains(eqn_parameter_set, v))
      92             :         {
      93           0 :           missing.push_back(v);
      94             :         }
      95             :       }
      96           0 :       missing_parameters[eqn_parameters] = missing;
      97           0 :     }
      98           0 :   }
      99             : 
     100           0 :   propositional_variable_instantiation operator()(const propositional_variable_instantiation& x) const
     101             :   {
     102           0 :     const data::variable_list& variables = propositional_variable_parameters.at(x.name());
     103           0 :     const data::data_expression_list& values = x.parameters();
     104           0 :     auto i = variables.begin();
     105           0 :     auto j = values.begin();
     106           0 :     for (; i != variables.end(); ++i, ++j)
     107             :     {
     108           0 :       std::size_t pos = parameter_positions[*i];
     109           0 :       tmp_parameters[pos] = *j;
     110             :     }
     111           0 :     for (const data::variable& v: missing_parameters[variables])
     112             :     {
     113           0 :       std::size_t pos = parameter_positions[v];
     114             : 
     115           0 :       if (m_reset)
     116             :       {
     117           0 :         tmp_parameters[pos] = generator(v.sort());
     118             :       }
     119             :       else
     120             :       {
     121           0 :         tmp_parameters[pos] = v;
     122             :       }
     123             :     }
     124           0 :     return propositional_variable_instantiation(x.name(), data::data_expression_list(tmp_parameters.begin(), tmp_parameters.end()));
     125             :   };
     126             : };
     127             : 
     128             : inline
     129           0 : void unify_parameters(pbes& p)
     130             : {
     131           0 :   std::map<core::identifier_string, data::variable_list> propositional_variable_parameters;
     132           0 :   for (const pbes_equation& eqn: p.equations())
     133             :   {
     134           0 :     propositional_variable_parameters[eqn.variable().name()] = eqn.variable().parameters();
     135             :   }
     136             : 
     137           0 :   unify_parameters_replace_function replace(propositional_variable_parameters, p.data());
     138             : 
     139             :   // update the right hand sides of the equations
     140           0 :   replace_propositional_variables(p, replace);
     141             : 
     142             :   // update the initial state
     143           0 :   p.initial_state() = replace(p.initial_state());
     144             : 
     145             :   // update the left hand sides of the equations
     146           0 :   for (pbes_equation& eqn: p.equations())
     147             :   {
     148           0 :     propositional_variable& X = eqn.variable();
     149           0 :     X = propositional_variable(X.name(), replace.parameters);
     150             :   }
     151           0 : }
     152             : 
     153             : inline
     154           0 : void unify_parameters(srf_pbes& p, bool reset = true)
     155             : {
     156           0 :   std::map<core::identifier_string, data::variable_list> propositional_variable_parameters;
     157           0 :   for (const srf_equation& eqn: p.equations())
     158             :   {
     159           0 :     propositional_variable_parameters[eqn.variable().name()] = eqn.variable().parameters();
     160             :   }
     161             : 
     162           0 :   unify_parameters_replace_function replace(propositional_variable_parameters, p.data(), reset);
     163             : 
     164             :   // update the equations
     165           0 :   for (srf_equation& eqn: p.equations())
     166             :   {
     167           0 :     for (srf_summand& summand: eqn.summands())
     168             :     {
     169           0 :       summand.variable() = replace(summand.variable());
     170             :     }
     171           0 :     propositional_variable& X = eqn.variable();
     172           0 :     X = propositional_variable(X.name(), replace.parameters);
     173             :   }
     174             : 
     175             :   // update the initial state
     176           0 :   p.initial_state() = replace(p.initial_state());
     177           0 : }
     178             : 
     179             : } // namespace pbes_system
     180             : 
     181             : } // namespace mcrl2
     182             : 
     183             : #endif // MCRL2_PBES_UNIFY_PARAMETERS_H