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/lps/remove.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_LPS_REMOVE_H
      13             : #define MCRL2_LPS_REMOVE_H
      14             : 
      15             : #include "mcrl2/lps/replace.h"
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : 
      20             : namespace lps
      21             : {
      22             : 
      23             : namespace detail
      24             : {
      25             : 
      26             : /// \brief Function object that checks if a summand has a false condition
      27             : struct is_trivial_summand
      28             : {
      29          39 :   bool operator()(const summand_base& s) const
      30             :   {
      31          39 :     return s.condition() == data::sort_bool::false_();
      32             :   }
      33             : };
      34             : 
      35             : /// \brief Function object that checks if a sort is a singleton sort.
      36             : /// Note that it is an approximation, meaning that in some cases it
      37             : /// may return false whereas in reality the answer is true.
      38             : struct is_singleton_sort
      39             : {
      40             :   const data::data_specification& m_data_spec;
      41             : 
      42           0 :   is_singleton_sort(const data::data_specification& data_spec)
      43           0 :     : m_data_spec(data_spec)
      44           0 :   {}
      45             : 
      46           0 :   bool operator()(const data::sort_expression& s) const
      47             :   {
      48           0 :     auto const& constructors = m_data_spec.constructors(s);
      49           0 :     if (constructors.size() != 1)
      50             :     {
      51           0 :       return false;
      52             :     }
      53           0 :     return !is_function_sort(constructors.front().sort());
      54             :   }
      55             : };
      56             : 
      57             : /// \brief Traverser for removing parameters from LPS data types.
      58             : /// These parameters can be either process parameters or free variables.
      59             : /// Assignments to these parameters are removed as well.
      60             : struct remove_parameters_builder: public data_expression_builder<remove_parameters_builder>
      61             : {
      62             :   typedef data_expression_builder<remove_parameters_builder> super;
      63             :   using super::enter;
      64             :   using super::leave;
      65             :   using super::apply;
      66             :   using super::update;
      67             : 
      68             :   const std::set<data::variable>& to_be_removed;
      69             :   data::variable_list process_parameters;
      70             : 
      71         743 :   remove_parameters_builder(const std::set<data::variable>& to_be_removed_)
      72         743 :     : to_be_removed(to_be_removed_)
      73         743 :   {}
      74             : 
      75             :   /// \brief Removes parameters from a set container.
      76         743 :   void update(std::set<data::variable>& x)
      77             :   {
      78        1133 :     for (const data::variable& v: to_be_removed)
      79             :     {
      80         390 :       x.erase(v);
      81             :     }
      82         743 :   }
      83             : 
      84             :   /// \brief Removes parameters from a list of variables.
      85             :   template <class T>
      86         743 :   void apply(atermpp::term_list<T>& result, const data::variable_list& x)
      87             :   {
      88             :     using utilities::detail::contains;
      89             : 
      90         743 :     std::vector<data::variable> result_vec;
      91        2493 :     for (const data::variable& v: x)
      92             :     {
      93        1007 :       if (!contains(to_be_removed, v))
      94             :       {
      95         758 :         result_vec.push_back(v);
      96             :       }
      97             :     }
      98         743 :     result = data::variable_list(result_vec.begin(), result_vec.end());
      99         743 :   }
     100             : 
     101             :   /// \brief Removes parameters from a list of assignments.
     102             :   /// Assignments to removed parameters are removed.
     103             :   template <class T>
     104        1268 :   void apply(atermpp::term_list<T>& result, const data::assignment_list& x)
     105             :   {
     106             :     using utilities::detail::contains;
     107        1268 :     std::vector<data::assignment> a(x.begin(), x.end());
     108        3221 :     a.erase(std::remove_if(a.begin(), a.end(), [&](const data::assignment& y) { return contains(to_be_removed, y.lhs()); }), a.end());
     109        1268 :     result = data::assignment_list(a.begin(), a.end());
     110        1268 :   }
     111             : 
     112             :   /// \brief Removes parameters from a linear_process
     113             :   /// \param x A linear_process
     114          25 :   void update(linear_process& x)
     115             :   {
     116          25 :     super::update(x);
     117          25 :     data::variable_list parameters;
     118          25 :     apply(parameters, x.process_parameters());
     119          25 :     x.process_parameters() = parameters;
     120          25 :   }
     121             : 
     122             :   /// \brief Removes parameters from a linear_process
     123             :   /// \param x A linear_process
     124         718 :   void update(stochastic_linear_process& x)
     125             :   {
     126         718 :     super::update(x);
     127         718 :     data::variable_list parameters;
     128         718 :     apply(parameters, x.process_parameters());
     129         718 :     x.process_parameters() = parameters;
     130         718 :   }
     131             : 
     132             :   /// \brief Removes expressions from e at the corresponding positions of process_parameters
     133         743 :   data::data_expression_list remove_expressions(const data::data_expression_list& e)
     134             :   {
     135             :     using utilities::detail::contains;
     136             : 
     137         743 :     assert(e.size() == process_parameters.size());
     138         743 :     std::vector<data::data_expression> result;
     139         743 :     auto pi = process_parameters.begin();
     140         743 :     auto ei = e.begin();
     141        1750 :     for (; pi != process_parameters.end(); ++pi, ++ei)
     142             :     {
     143        1007 :       if (!contains(to_be_removed, *pi))
     144             :       {
     145         758 :         result.push_back(*ei);
     146             :       }
     147             :     }
     148        1486 :     return data::data_expression_list(result.begin(), result.end());
     149         743 :   }
     150             : 
     151             :   template <class T>
     152          25 :   void apply(T& result, const process_initializer& x)
     153             :   {
     154          25 :     auto expressions = remove_expressions(x.expressions());
     155          25 :     result = process_initializer(expressions);
     156          25 :   }
     157             : 
     158             :   template <class T>
     159         718 :   void apply(T& result,  const stochastic_process_initializer& x)
     160             :   {
     161         718 :     auto expressions = remove_expressions(x.expressions());
     162         718 :     lps::stochastic_distribution distribution;
     163         718 :     super::apply(distribution, x.distribution());
     164         718 :     result = stochastic_process_initializer(expressions, distribution);
     165         718 :   }
     166             : 
     167             :   /// \brief Removes parameters from a linear process specification
     168             :   /// \param x A linear process specification
     169          25 :   void update(specification& x)
     170             :   {
     171          25 :     process_parameters = x.process().process_parameters();
     172          25 :     super::update(x);
     173          25 :     update(x.global_variables());
     174          25 :   }
     175             : 
     176             :   /// \brief Removes parameters from a linear process specification
     177             :   /// \param x A linear process specification
     178         718 :   void update(stochastic_specification& x)
     179             :   {
     180         718 :     process_parameters = x.process().process_parameters();
     181         718 :     super::update(x);
     182         718 :     update(x.global_variables());
     183         718 :   }
     184             : };
     185             : 
     186             : } // namespace detail
     187             : 
     188             : /// \brief Rewrites an LPS data type.
     189             : template <typename Object>
     190         743 : void remove_parameters(Object& x, const std::set<data::variable>& to_be_removed)
     191             : {
     192         743 :   detail::remove_parameters_builder f(to_be_removed);
     193         743 :   f.update(x);
     194         743 : }
     195             : 
     196             : /// \brief Removes summands with condition equal to false from a linear process specification
     197             : /// \param spec A linear process specification
     198             : template <typename Specification>
     199           7 : void remove_trivial_summands(Specification& spec)
     200             : {
     201           7 :   auto& v = spec.process().action_summands();
     202           7 :   v.erase(std::remove_if(v.begin(), v.end(), lps::detail::is_trivial_summand()), v.end());
     203             : 
     204           7 :   deadlock_summand_vector& w = spec.process().deadlock_summands();
     205           7 :   w.erase(std::remove_if(w.begin(), w.end(), lps::detail::is_trivial_summand()), w.end());
     206           7 : }
     207             : 
     208             : /// \brief Removes parameters with a singleton sort from a linear process specification
     209             : /// \param spec A linear process specification
     210             : template <typename Specification>
     211           0 : void remove_singleton_sorts(Specification& spec)
     212             : {
     213           0 :   data::mutable_map_substitution<> sigma;
     214           0 :   std::set<data::variable> to_be_removed;
     215           0 :   for (const data::variable& v: spec.process().process_parameters())
     216             :   {
     217           0 :     if (lps::detail::is_singleton_sort(spec.data())(v.sort()))
     218             :     {
     219           0 :       sigma[v] = *spec.data().constructors(v.sort()).begin();
     220           0 :       to_be_removed.insert(v);
     221             :     }
     222             :   }
     223           0 :   lps::replace_variables(spec, sigma);
     224           0 :   lps::remove_parameters(spec, to_be_removed);
     225           0 : }
     226             : 
     227             : /// \brief Removes assignments of the form x := x from v for variables x that are not contained in do_not_remove.
     228             : inline
     229           2 : data::assignment_list remove_redundant_assignments(const data::assignment_list& assignments, const data::variable_list& do_not_remove)
     230             : {
     231             :   using utilities::detail::contains;
     232             : 
     233           2 :   std::vector<data::assignment> result;
     234           4 :   for (const data::assignment& a: assignments)
     235             :   {
     236           2 :     if (a.lhs() != a.rhs() || contains(do_not_remove, a.lhs()))
     237             :     {
     238           1 :       result.push_back(a);
     239             :     }
     240             :   }
     241           4 :   return data::assignment_list(result.begin(), result.end());
     242           2 : }
     243             : 
     244             : /// \brief Removes redundant assignments of the form x = x from an LPS specification
     245             : /// \param lpsspec A linear process specification
     246             : template <typename Specification>
     247           2 : void remove_redundant_assignments(Specification& lpsspec)
     248             : {
     249           2 :   auto& summands = lpsspec.process().action_summands();
     250           4 :   for (auto i = summands.begin(); i != summands.end(); ++i)
     251             :   {
     252           2 :     i->assignments() = remove_redundant_assignments(i->assignments(), i->summation_variables());
     253             :   }
     254           2 : }
     255             : 
     256             : } // namespace lps
     257             : 
     258             : } // namespace mcrl2
     259             : 
     260             : #endif // MCRL2_LPS_REMOVE_H