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/parelm.h
      10             : /// \brief The parelm algorithm.
      11             : 
      12             : #ifndef MCRL2_LPS_PARELM_H
      13             : #define MCRL2_LPS_PARELM_H
      14             : 
      15             : #include "mcrl2/lps/detail/lps_algorithm.h"
      16             : #include "mcrl2/utilities/detail/iota.h"
      17             : #include "mcrl2/utilities/reachable_nodes.h"
      18             : #include <boost/integer.hpp>
      19             : 
      20             : namespace mcrl2
      21             : {
      22             : 
      23             : namespace lps
      24             : {
      25             : 
      26             : namespace detail
      27             : {
      28             :   inline
      29          26 :   void collect_transition_variables(const action_summand& s, std::set<data::variable>& result)
      30             :   {
      31          26 :     std::set<data::variable> tmp;
      32             : 
      33          26 :     tmp = data::find_all_variables(s.condition());
      34          26 :     result.insert(tmp.begin(), tmp.end());
      35             : 
      36          26 :     tmp = lps::find_all_variables(s.multi_action());
      37          26 :     result.insert(tmp.begin(), tmp.end());
      38          26 :   }
      39             : 
      40             :   inline
      41          10 :   void collect_transition_variables(const stochastic_action_summand& s, std::set<data::variable>& result)
      42             :   {
      43          10 :     collect_transition_variables(static_cast<const action_summand&>(s), result);
      44          10 :     std::set<data::variable> tmp = lps::find_all_variables(s.distribution());
      45          10 :     result.insert(tmp.begin(), tmp.end());
      46          10 :   }
      47             : 
      48             :   inline
      49           3 :   void collect_transition_variables(const deadlock_summand& s, std::set<data::variable>& result)
      50             :   {
      51           3 :     std::set<data::variable> tmp;
      52             : 
      53           3 :     tmp = data::find_all_variables(s.condition());
      54           3 :     result.insert(tmp.begin(), tmp.end());
      55             : 
      56           3 :     tmp = lps::find_all_variables(s.deadlock());
      57           3 :     result.insert(tmp.begin(), tmp.end());
      58           3 :   }
      59             : 
      60             : } // namespace detail
      61             : 
      62             : /// \brief Algorithm class for elimination of unused parameters from a linear
      63             : /// process specification
      64             : template <typename Specification>
      65             : class parelm_algorithm: public lps::detail::lps_algorithm<Specification>
      66             : {
      67             :   typedef typename lps::detail::lps_algorithm<Specification> super;
      68             :   using super::m_spec;
      69             :   using super::verbose;
      70             : 
      71             :   protected:
      72             : 
      73             :     /// \brief Returns the data variables that are considered in the parelm algorithm.
      74             :     /// \return The data variables that appear in the condition, action or time of the summands
      75          15 :     std::set<data::variable> transition_variables()
      76             :     {
      77          15 :       std::set<data::variable> result;
      78             : 
      79          15 :       auto const& action_summands = m_spec.process().action_summands();
      80          41 :       for (auto i = action_summands.begin(); i != action_summands.end(); ++i)
      81             :       {
      82          26 :         detail::collect_transition_variables(*i, result);
      83             :       }
      84             : 
      85          15 :       auto const& deadlock_summands = m_spec.process().deadlock_summands();
      86          18 :       for (auto i = deadlock_summands.begin(); i != deadlock_summands.end(); ++i)
      87             :       {
      88           3 :         detail::collect_transition_variables(*i, result);
      89             :       }
      90          15 :       return result;
      91           0 :     }
      92             : 
      93          15 :     void report_results(const std::set<data::variable>& to_be_removed) const
      94             :     {
      95          15 :       if (verbose())
      96             :       {
      97           0 :         std::clog << "parelm removed " << to_be_removed.size() << " process parameters: " <<std::endl;
      98           0 :         for (const data::variable& v: to_be_removed)
      99             :         {
     100           0 :           std::clog << v << ":" << v.sort() << std::endl;
     101             :         }
     102             :       }
     103          15 :     }
     104             : 
     105             :     /// \brief First version of parelm1
     106           8 :     void parelm1()
     107             :     {
     108             : #ifdef MCRL2_LPS_PARELM_DEBUG
     109             :       std::clog << "--- parelm 1 ---" << std::endl;
     110             : #endif
     111           8 :       const data::variable_list& pars = m_spec.process().process_parameters();
     112           8 :       std::set<data::variable> process_parameters(pars.begin(),pars.end());
     113             : 
     114             :       // significant variables may not be removed by parelm
     115           8 :       std::set<data::variable> significant_variables = transition_variables();
     116             : 
     117             : #ifdef MCRL2_LPS_PARELM_DEBUG
     118             :       std::clog << "initial significant variables: ";
     119             :       for (auto i = significant_variables.begin(); i != significant_variables.end(); ++i)
     120             :       {
     121             :         std::clog << *i << " ";
     122             :       }
     123             :       std::clog << std::endl;
     124             : #endif
     125             : 
     126             :       // recursively extend the set of significant variables
     127           8 :       std::set<data::variable> todo = significant_variables;
     128          98 :       while (!todo.empty())
     129             :       {
     130          45 :         data::variable x = *todo.begin();
     131          45 :         todo.erase(todo.begin());
     132             : 
     133         370 :         for (auto i = m_spec.process().action_summands().begin(); i != m_spec.process().action_summands().end(); ++i)
     134             :         {
     135         325 :           const data::assignment_list& assignments = i->assignments();
     136        1439 :           auto j = std::find_if(assignments.begin(), assignments.end(), [&](const data::assignment& a) { return a.lhs() == x; });
     137         325 :           if (j != assignments.end())
     138             :           {
     139          52 :             std::set<data::variable> vars;
     140          52 :             data::find_all_variables(j->rhs(), std::inserter(vars, vars.end()));
     141          52 :             std::set<data::variable> new_variables = utilities::detail::set_difference(vars, significant_variables);
     142          52 :             todo.insert(new_variables.begin(), new_variables.end());
     143          52 :             significant_variables.insert(new_variables.begin(), new_variables.end());
     144             : #ifdef MCRL2_LPS_PARELM_DEBUG
     145             :             for (auto k = new_variables.begin(); k != new_variables.end(); ++k)
     146             :             {
     147             :               std::clog << "found dependency " << x << " -> " << *k << std::endl;
     148             :             }
     149             : #endif
     150          52 :           }
     151             :         }
     152             :       }
     153           8 :       std::set<data::variable> to_be_removed = utilities::detail::set_difference(process_parameters, significant_variables);
     154             : #ifdef MCRL2_LPS_PARELM_DEBUG
     155             :       std::clog << "to be removed: " << data::pp(data::variable_list(to_be_removed.begin(), to_be_removed.end())) << std::endl;
     156             : #endif
     157           8 :       report_results(to_be_removed);
     158           8 :       lps::remove_parameters(m_spec, to_be_removed);
     159           8 :       assert(check_well_typedness(m_spec));
     160           8 :     }
     161             : 
     162             :     /// \brief Second version of parelm that builds a dependency graph
     163           7 :     void parelm2()
     164             :     {
     165             : #ifdef MCRL2_LPS_PARELM_DEBUG
     166             :       std::clog << "--- parelm 2 ---" << std::endl;
     167             : #endif
     168           7 :       const data::variable_list& pars = m_spec.process().process_parameters();
     169           7 :       std::set<data::variable> process_parameters(pars.begin(),pars.end());
     170             : 
     171             :       // create a mapping m from process parameters to integers
     172           7 :       std::map<data::variable, std::size_t> m;
     173           7 :       int index = 0;
     174          33 :       for (const data::variable& process_parameter: process_parameters)
     175             :       {
     176             : #ifdef MCRL2_LPS_PARELM_DEBUG
     177             :         std::clog << "vertex " << index << " = " << data::pp(*i) << std::endl;
     178             : #endif
     179          26 :         m[process_parameter] = index++;
     180             :       }
     181             : 
     182             :       // compute the initial set v of significant variables
     183           7 :       std::set<data::variable> significant_variables = transition_variables();
     184           7 :       std::vector<std::size_t> v;
     185          18 :       for (const data::variable& significant_variable: significant_variables)
     186             :       {
     187          11 :         v.push_back(m[significant_variable]);
     188             :       }
     189             : 
     190             :       // compute the dependency graph G
     191             :       typedef boost::adjacency_list<boost::vecS, boost::vecS, boost::directedS> graph;
     192           7 :       graph G(process_parameters.size());
     193          15 :       for (auto i = m_spec.process().action_summands().begin(); i != m_spec.process().action_summands().end(); ++i)
     194             :       {
     195          35 :         for (const data::assignment& a: i->assignments())
     196             :         {
     197          19 :           std::size_t j0 = m[a.lhs()];
     198          19 :           std::set<data::variable> vars;
     199          19 :           data::find_all_variables(a.rhs(), std::inserter(vars, vars.end()));
     200          37 :           for (const data::variable& var: vars)
     201             :           {
     202          18 :             std::size_t k0 = m[var];
     203             : #ifdef MCRL2_LPS_PARELM_DEBUG
     204             :             std::clog << "edge " << j0 << " -> " << k0 << std::endl;
     205             : #endif
     206          18 :             boost::add_edge(j0, k0, G);
     207             :           }
     208             :         }
     209             :       }
     210             : 
     211             : #ifdef MCRL2_LPS_PARELM_DEBUG
     212             :       std::clog << "initial significant variables: ";
     213             :       for (auto k = v.begin(); k != v.end(); ++k)
     214             :       {
     215             :         std::clog << *k << " ";
     216             :       }
     217             :       std::clog << std::endl;
     218             : #endif
     219             : 
     220             :       // compute the reachable nodes (i.e. the significant parameters)
     221           7 :       std::vector<std::size_t> r1 = mcrl2::utilities::reachable_nodes(G, v.begin(), v.end());
     222             : #ifdef MCRL2_LPS_PARELM_DEBUG
     223             :       std::clog << "reachable nodes: ";
     224             :       for (auto k = r1.begin(); k != r1.end(); ++k)
     225             :       {
     226             :         std::clog << *k << " ";
     227             :       }
     228             :       std::clog << std::endl;
     229             : #endif
     230           7 :       std::set<std::size_t> r2(r1.begin(), r1.end());
     231           7 :       std::set<data::variable> to_be_removed;
     232          33 :       for (const data::variable& process_parameter: process_parameters)
     233             :       {
     234          26 :         if (r2.find(m[process_parameter]) == r2.end())
     235             :         {
     236          12 :           to_be_removed.insert(process_parameter);
     237             :         }
     238             :       }
     239             : #ifdef MCRL2_LPS_PARELM_DEBUG
     240             :       std::clog << "to be removed: " << data::pp(data::variable_list(to_be_removed.begin(), to_be_removed.end())) << std::endl;
     241             : #endif
     242           7 :       report_results(to_be_removed);
     243           7 :       lps::remove_parameters(m_spec, to_be_removed);
     244           7 :       assert(check_well_typedness(m_spec));
     245           7 :     }
     246             : 
     247             :   public:
     248             : 
     249             :     /// \brief Constructor
     250          15 :     parelm_algorithm(Specification& spec )
     251          15 :       : lps::detail::lps_algorithm<Specification>(spec)
     252          15 :     {}
     253             : 
     254             :     /// \brief Runs the parelm algorithm
     255          15 :     void run(bool variant1 = true)
     256             :     {
     257          15 :       if (variant1)
     258             :       {
     259           8 :         parelm1();
     260             :       }
     261             :       else
     262             :       {
     263           7 :         parelm2();
     264             :       }
     265          15 :     }
     266             : };
     267             : 
     268             : /// \brief Removes unused parameters from a linear process specification.
     269             : /// \param spec A linear process specification
     270             : /// \param variant1 If true the default variant of parelm is used, otherwise an
     271             : ///        alternative implementation is chosen.
     272             : template <typename Specification>
     273          15 : void parelm(Specification& spec, bool variant1 = true)
     274             : {
     275          15 :   parelm_algorithm<Specification> algorithm(spec);
     276          15 :   algorithm.run(variant1);
     277          15 : }
     278             : 
     279             : } // namespace lps
     280             : 
     281             : } // namespace mcrl2
     282             : 
     283             : #endif // MCRL2_LPS_PARELM_H