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/detail/lps_algorithm.h
      10             : /// \brief Add your file description here.
      11             : 
      12             : #ifndef MCRL2_LPS_DETAIL_LPS_ALGORITHM_H
      13             : #define MCRL2_LPS_DETAIL_LPS_ALGORITHM_H
      14             : 
      15             : #include "mcrl2/data/rewriter.h"
      16             : #include "mcrl2/lps/detail/instantiate_global_variables.h"
      17             : #include "mcrl2/lps/rewrite.h"
      18             : 
      19             : namespace mcrl2
      20             : {
      21             : 
      22             : namespace lps
      23             : {
      24             : 
      25             : namespace detail
      26             : {
      27             : 
      28             : /// \brief Algorithm class for algorithms on linear process specifications.
      29             : /// It can be instantiated with lps::specification and lps::stochastic_specification.
      30             : template <typename Specification = specification>
      31             : class lps_algorithm
      32             : {
      33             :   protected:
      34             :     /// \brief The specification that is processed by the algorithm
      35             :     Specification& m_spec;
      36             : 
      37       14676 :     void sumelm_find_variables(const action_summand& s, std::set<data::variable>& result) const
      38             :     {
      39       14676 :       std::set<data::variable> tmp;
      40             : 
      41       14676 :       tmp = data::find_free_variables(s.condition());
      42       14676 :       result.insert(tmp.begin(), tmp.end());
      43             : 
      44       14676 :       tmp = lps::find_free_variables(s.multi_action());
      45       14676 :       result.insert(tmp.begin(), tmp.end());
      46             : 
      47       14676 :       tmp = data::find_free_variables(s.assignments());
      48       14676 :       result.insert(tmp.begin(), tmp.end());
      49       14676 :     }
      50             : 
      51           2 :     void sumelm_find_variables(const deadlock_summand& s, std::set<data::variable>& result) const
      52             :     {
      53           2 :       std::set<data::variable> tmp;
      54             : 
      55           2 :       tmp = data::find_free_variables(s.condition());
      56           2 :       result.insert(tmp.begin(), tmp.end());
      57             : 
      58           2 :       tmp = lps::find_free_variables(s.deadlock());
      59           2 :       result.insert(tmp.begin(), tmp.end());
      60           2 :     }
      61             : 
      62             :     template <typename SummandType>
      63       14678 :     void summand_remove_unused_summand_variables(SummandType& summand_)
      64             :     {
      65       14678 :       data::variable_vector new_summation_variables;
      66             : 
      67       14678 :       std::set<data::variable> occurring_vars;
      68       14678 :       sumelm_find_variables(summand_, occurring_vars);
      69             : 
      70       14678 :       std::set<data::variable> summation_variables(summand_.summation_variables().begin(),summand_.summation_variables().end());
      71       14678 :       std::set_intersection(summation_variables.begin(), summation_variables.end(),
      72             :                             occurring_vars.begin(), occurring_vars.end(),
      73             :                             std::inserter(new_summation_variables, new_summation_variables.end()));
      74             : 
      75       14678 :       summand_.summation_variables() = data::variable_list(new_summation_variables.begin(),new_summation_variables.end());
      76       14678 :     }
      77             : 
      78             :   public:
      79             :     /// \brief Constructor
      80       15433 :     lps_algorithm(Specification& spec)
      81       15433 :       : m_spec(spec)
      82       15433 :     {}
      83             : 
      84             :     /// \brief Flag for verbose output
      85          15 :     bool verbose() const
      86             :     {
      87          15 :       return mCRL2logEnabled(log::verbose);
      88             :     }
      89             : 
      90             :     /// \brief Applies the next state substitution to the variable v.
      91        1359 :     data::data_expression next_state(const action_summand& s, const data::variable& v) const
      92             :     {
      93        3887 :       for (const data::assignment& a: s.assignments())
      94             :       {
      95        2129 :         if (a.lhs() == v)
      96             :         {
      97         960 :           return a.rhs();
      98             :         }
      99             :       }
     100         399 :       return v; // no assignment to v found, so return v itself
     101             :     }
     102             : 
     103             :     /// \brief Attempts to eliminate the free variables of the specification, by substituting
     104             :     /// a constant value for them. If no constant value is found for one of the variables,
     105             :     /// an exception is thrown.
     106           1 :     void instantiate_free_variables()
     107             :     {
     108           1 :       lps::detail::instantiate_global_variables(m_spec);
     109           1 :     }
     110             : 
     111             :     /// \brief Removes formal parameters from the specification
     112             :     void remove_parameters(const std::set<data::variable>& to_be_removed)
     113             :     {
     114             :       lps::remove_parameters(m_spec, to_be_removed);
     115             :     }
     116             : 
     117             :     /// \brief Removes parameters with a singleton sort
     118           0 :     void remove_singleton_sorts()
     119             :     {
     120           0 :       lps::remove_singleton_sorts(m_spec);
     121           0 :     }
     122             : 
     123             :     /// \brief Removes summands with condition equal to false
     124           4 :     void remove_trivial_summands()
     125             :     {
     126           4 :       lps::remove_trivial_summands(m_spec);
     127           4 :     }
     128             : 
     129             :     /// \brief Removes unused summand variables.
     130           1 :     void remove_unused_summand_variables()
     131             :     {
     132           1 :       auto& v = m_spec.process().action_summands();
     133           1 :       std::for_each(v.begin(), 
     134             :                     v.end(), 
     135          10 :                     [this](action_summand& s){lps_algorithm::summand_remove_unused_summand_variables<typename Specification::process_type::action_summand_type>(s); }); 
     136             : 
     137           1 :       auto& w = m_spec.process().deadlock_summands();
     138           1 :       std::for_each(w.begin(), 
     139             :                     w.end(), 
     140           1 :                     [this](deadlock_summand& s){lps_algorithm::summand_remove_unused_summand_variables<deadlock_summand>(s); }); 
     141           1 :     }
     142             : };
     143             : 
     144             : } // namespace detail
     145             : 
     146             : } // namespace lps
     147             : 
     148             : } // namespace mcrl2
     149             : 
     150             : #endif // MCRL2_LPS_DETAIL_LPS_ALGORITHM_H