parelm.h

Go to the documentation of this file.

// Author(s): Wieger Wesselink
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
 
#ifndef MCRL2_LPS_PARELM_H
#define MCRL2_LPS_PARELM_H
 
#include "mcrl2/lps/detail/lps_algorithm.h"
#include "mcrl2/utilities/detail/iota.h"
#include "mcrl2/utilities/reachable_nodes.h"
#include <boost/integer.hpp>
 
namespace mcrl2
{
 
namespace lps
{
 
namespace detail
{
  inline
  void collect_transition_variables(const action_summand& s, std::set<data::variable>& result)
  {
    std::set<data::variable> tmp;
 
    tmp = data::find_all_variables(s.condition());
    result.insert(tmp.begin(), tmp.end());
 
    tmp = lps::find_all_variables(s.multi_action());
    result.insert(tmp.begin(), tmp.end());
  }
 
  inline
  void collect_transition_variables(const stochastic_action_summand& s, std::set<data::variable>& result)
  {
    collect_transition_variables(static_cast<const action_summand&>(s), result);
    std::set<data::variable> tmp = lps::find_all_variables(s.distribution());
    result.insert(tmp.begin(), tmp.end());
  }
 
  inline
  void collect_transition_variables(const deadlock_summand& s, std::set<data::variable>& result)
  {
    std::set<data::variable> tmp;
 
    tmp = data::find_all_variables(s.condition());
    result.insert(tmp.begin(), tmp.end());
 
    tmp = lps::find_all_variables(s.deadlock());
    result.insert(tmp.begin(), tmp.end());
  }
 
} // namespace detail
 
template <typename Specification>
class parelm_algorithm: public lps::detail::lps_algorithm<Specification>
{
  typedef typename lps::detail::lps_algorithm<Specification> super;
  using super::m_spec;
  using super::verbose;
 
  protected:
 
    std::set<data::variable> transition_variables()
    {
      std::set<data::variable> result;
 
      auto const& action_summands = m_spec.process().action_summands();
      for (auto i = action_summands.begin(); i != action_summands.end(); ++i)
      {
        detail::collect_transition_variables(*i, result);
      }
 
      auto const& deadlock_summands = m_spec.process().deadlock_summands();
      for (auto i = deadlock_summands.begin(); i != deadlock_summands.end(); ++i)
      {
        detail::collect_transition_variables(*i, result);
      }
      return result;
    }
 
    void report_results(const std::set<data::variable>& to_be_removed) const
    {
      if (verbose())
      {
        std::clog << "parelm removed " << to_be_removed.size() << " process parameters: " <<std::endl;
        for (const data::variable& v: to_be_removed)
        {
          std::clog << v << ":" << v.sort() << std::endl;
        }
      }
    }
 
    void parelm1()
    {
#ifdef MCRL2_LPS_PARELM_DEBUG
      std::clog << "--- parelm 1 ---" << std::endl;
#endif
      const data::variable_list& pars = m_spec.process().process_parameters();
      std::set<data::variable> process_parameters(pars.begin(),pars.end());
 
      // significant variables may not be removed by parelm
      std::set<data::variable> significant_variables = transition_variables();
 
#ifdef MCRL2_LPS_PARELM_DEBUG
      std::clog << "initial significant variables: ";
      for (auto i = significant_variables.begin(); i != significant_variables.end(); ++i)
      {
        std::clog << *i << " ";
      }
      std::clog << std::endl;
#endif
 
      // recursively extend the set of significant variables
      std::set<data::variable> todo = significant_variables;
      while (!todo.empty())
      {
        data::variable x = *todo.begin();
        todo.erase(todo.begin());
 
        for (auto i = m_spec.process().action_summands().begin(); i != m_spec.process().action_summands().end(); ++i)
        {
          const data::assignment_list& assignments = i->assignments();
          auto j = std::find_if(assignments.begin(), assignments.end(), [&](const data::assignment& a) { return a.lhs() == x; });
          if (j != assignments.end())
          {
            std::set<data::variable> vars;
            data::find_all_variables(j->rhs(), std::inserter(vars, vars.end()));
            std::set<data::variable> new_variables = utilities::detail::set_difference(vars, significant_variables);
            todo.insert(new_variables.begin(), new_variables.end());
            significant_variables.insert(new_variables.begin(), new_variables.end());
#ifdef MCRL2_LPS_PARELM_DEBUG
            for (auto k = new_variables.begin(); k != new_variables.end(); ++k)
            {
              std::clog << "found dependency " << x << " -> " << *k << std::endl;
            }
#endif
          }
        }
      }
      std::set<data::variable> to_be_removed = utilities::detail::set_difference(process_parameters, significant_variables);
#ifdef MCRL2_LPS_PARELM_DEBUG
      std::clog << "to be removed: " << data::pp(data::variable_list(to_be_removed.begin(), to_be_removed.end())) << std::endl;
#endif
      report_results(to_be_removed);
      lps::remove_parameters(m_spec, to_be_removed);
      assert(check_well_typedness(m_spec));
    }
 
    void parelm2()
    {
#ifdef MCRL2_LPS_PARELM_DEBUG
      std::clog << "--- parelm 2 ---" << std::endl;
#endif
      const data::variable_list& pars = m_spec.process().process_parameters();
      std::set<data::variable> process_parameters(pars.begin(),pars.end());
 
      // create a mapping m from process parameters to integers
      std::map<data::variable, std::size_t> m;
      int index = 0;
      for (const data::variable& process_parameter: process_parameters)
      {
#ifdef MCRL2_LPS_PARELM_DEBUG
        std::clog << "vertex " << index << " = " << data::pp(*i) << std::endl;
#endif
        m[process_parameter] = index++;
      }
 
      // compute the initial set v of significant variables
      std::set<data::variable> significant_variables = transition_variables();
      std::vector<std::size_t> v;
      for (const data::variable& significant_variable: significant_variables)
      {
        v.push_back(m[significant_variable]);
      }
 
      // compute the dependency graph G
      typedef boost::adjacency_list<boost::vecS, boost::vecS, boost::directedS> graph;
      graph G(process_parameters.size());
      for (auto i = m_spec.process().action_summands().begin(); i != m_spec.process().action_summands().end(); ++i)
      {
        for (const data::assignment& a: i->assignments())
        {
          std::size_t j0 = m[a.lhs()];
          std::set<data::variable> vars;
          data::find_all_variables(a.rhs(), std::inserter(vars, vars.end()));
          for (const data::variable& var: vars)
          {
            std::size_t k0 = m[var];
#ifdef MCRL2_LPS_PARELM_DEBUG
            std::clog << "edge " << j0 << " -> " << k0 << std::endl;
#endif
            boost::add_edge(j0, k0, G);
          }
        }
      }
 
#ifdef MCRL2_LPS_PARELM_DEBUG
      std::clog << "initial significant variables: ";
      for (auto k = v.begin(); k != v.end(); ++k)
      {
        std::clog << *k << " ";
      }
      std::clog << std::endl;
#endif
 
      // compute the reachable nodes (i.e. the significant parameters)
      std::vector<std::size_t> r1 = mcrl2::utilities::reachable_nodes(G, v.begin(), v.end());
#ifdef MCRL2_LPS_PARELM_DEBUG
      std::clog << "reachable nodes: ";
      for (auto k = r1.begin(); k != r1.end(); ++k)
      {
        std::clog << *k << " ";
      }
      std::clog << std::endl;
#endif
      std::set<std::size_t> r2(r1.begin(), r1.end());
      std::set<data::variable> to_be_removed;
      for (const data::variable& process_parameter: process_parameters)
      {
        if (r2.find(m[process_parameter]) == r2.end())
        {
          to_be_removed.insert(process_parameter);
        }
      }
#ifdef MCRL2_LPS_PARELM_DEBUG
      std::clog << "to be removed: " << data::pp(data::variable_list(to_be_removed.begin(), to_be_removed.end())) << std::endl;
#endif
      report_results(to_be_removed);
      lps::remove_parameters(m_spec, to_be_removed);
      assert(check_well_typedness(m_spec));
    }
 
  public:
 
    parelm_algorithm(Specification& spec )
      : lps::detail::lps_algorithm<Specification>(spec)
    {}
 
    void run(bool variant1 = true)
    {
      if (variant1)
      {
        parelm1();
      }
      else
      {
        parelm2();
      }
    }
};
 
template <typename Specification>
void parelm(Specification& spec, bool variant1 = true)
{
  parelm_algorithm<Specification> algorithm(spec);
  algorithm.run(variant1);
}
 
} // namespace lps
 
} // namespace mcrl2
 
#endif // MCRL2_LPS_PARELM_H