Line data    Source code

       1             : // Author(s): Jeroen Keiren, Thomas Neele
       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 sumelm.h
      10             : /// \brief Provides an implementation of the sum elimination lemma,
      11             : ///        as well as the removal of unused summation variables.
      12             : ///        The sum elimination lemma is the following:
      13             : ///          sum d:D . d == e -> X(d) = X(e).
      14             : ///        Removal of unused summation variables is according to the
      15             : ///        following lemma:
      16             : ///          d not in x implies sum d:D . x = x
      17             : 
      18             : #ifndef MCRL2_LPS_SUMELM_H
      19             : #define MCRL2_LPS_SUMELM_H
      20             : 
      21             : #include "mcrl2/data/equality_one_point_substitution.h"
      22             : #include "mcrl2/data/find_equalities.h"
      23             : #include "mcrl2/lps/decluster.h"
      24             : 
      25             : namespace mcrl2
      26             : {
      27             : namespace lps
      28             : {
      29             : 
      30             : /// \brief Class implementing the sum elimination lemma.
      31             : template <typename Specification = specification>
      32             : class sumelm_algorithm: public detail::lps_algorithm<Specification>
      33             : {
      34             :   typedef typename detail::lps_algorithm<Specification> super;
      35             :   using super::m_spec;
      36             : 
      37             :   protected:
      38             :     /// Stores the number of summation variables that has been removed.
      39             :     std::size_t m_removed;
      40             : 
      41             :     /// Whether to decluster disjunctive conditions first.
      42             :     bool m_decluster;
      43             : 
      44             :   public:
      45             :     /// \brief Constructor.
      46             :     /// \param spec The specification to which sum elimination should be
      47             :     ///             applied.
      48             :     /// \param decluster Control whether disjunctive conditions need to be split
      49             :     ///        into multiple summands.
      50       14665 :     sumelm_algorithm(Specification& spec, bool decluster = false)
      51             :       : lps::detail::lps_algorithm<Specification>(spec),
      52       14665 :         m_removed(0),
      53       14665 :         m_decluster(decluster)
      54       14665 :     {}
      55             : 
      56             :     /// \brief Apply the sum elimination lemma to all summands in the
      57             :     ///        specification.
      58          11 :     void run()
      59             :     {
      60          11 :       if (m_decluster)
      61             :       {
      62             :         // First decluster specification
      63           0 :         decluster_algorithm<Specification>(m_spec).run();
      64             :       }
      65             : 
      66          11 :       m_removed = 0; // Re-initialise number of removed variables for a fresh run.
      67             : 
      68          23 :       for (action_summand& s: m_spec.process().action_summands())
      69             :       {
      70          12 :         (*this)(s);
      71             :       }
      72             : 
      73          12 :       for (deadlock_summand& s: m_spec.process().deadlock_summands())
      74             :       {
      75           1 :         (*this)(s);
      76             :       }
      77             : 
      78          11 :       mCRL2log(log::verbose) << "Removed " << m_removed << " summation variables" << std::endl;
      79          11 :     }
      80             : 
      81             :     /// \brief Apply the sum elimination lemma to summand s.
      82             :     /// \param s an action_summand.
      83             :     template <class Summand>
      84       14667 :     void operator()(Summand& s)
      85             :     {
      86       14667 :       std::map<data::variable, std::set<data::data_expression> > equalities = data::find_equalities(s.condition());
      87       14667 :       auto [sigma,remaining_variables] = data::make_one_point_rule_substitution(equalities, s.summation_variables());
      88             : 
      89       14667 :       std::size_t original_num_vars = s.summation_variables().size();
      90       14667 :       if (remaining_variables.size() != original_num_vars)
      91             :       {
      92             :         // A substitution was found
      93             :         // Temporarily remove sumvars, otherwise the capture avoiding substitution will modify them
      94        1490 :         s.summation_variables() = data::variable_list();
      95        1490 :         lps::replace_variables_capture_avoiding(s, sigma);
      96        1490 :         s.summation_variables() = data::variable_list(remaining_variables.begin(), remaining_variables.end());
      97             :       }
      98             : 
      99       14667 :       super::summand_remove_unused_summand_variables(s);
     100       14667 :       m_removed += original_num_vars - s.summation_variables().size();
     101       14667 :     }
     102             : 
     103             :     /// \brief Returns the amount of removed summation variables.
     104       14654 :     std::size_t removed() const
     105             :     {
     106       14654 :       return m_removed;
     107             :     }
     108             : };
     109             : 
     110             : /// \brief Apply the sum elimination lemma to summand s.
     111             : /// \param s an action summand
     112             : /// \return \c true if any summation variables have been removed, or \c false otherwise.
     113             : inline
     114             : bool sumelm(action_summand& s)
     115             : {
     116             :   specification spec;
     117             :   sumelm_algorithm<specification> algorithm(spec);
     118             :   algorithm(s);
     119             :   return algorithm.removed() > 0;
     120             : }
     121             : 
     122             : /// \brief Apply the sum elimination lemma to summand s.
     123             : /// \param s a stochastic action summand
     124             : /// \return \c true if any summation variables have been removed, or \c false otherwise.
     125             : inline
     126       14654 : bool sumelm(stochastic_action_summand& s)
     127             : {
     128       14654 :   stochastic_specification spec;
     129       14654 :   sumelm_algorithm<stochastic_specification> algorithm(spec);
     130       14654 :   algorithm(s);
     131       29308 :   return algorithm.removed() > 0;
     132       14654 : }
     133             : 
     134             : /// \brief Apply the sum elimination lemma to summand s.
     135             : /// \param s a deadlock summand
     136             : /// \return \c true if any summation variables have been removed, or \c false otherwise.
     137             : inline
     138             : bool sumelm(deadlock_summand& s)
     139             : {
     140             :   specification spec;
     141             :   sumelm_algorithm<specification> algorithm(spec);
     142             :   algorithm(s);
     143             :   return algorithm.removed() > 0;
     144             : }
     145             : 
     146             : } // namespace lps
     147             : } // namespace mcrl2
     148             : 
     149             : #endif // MCRL2_LPS_SUMELM_H
     150             :