Line data    Source code

       1             : // Author(s): Jeroen Keiren
       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 decluster.h
      10             : /// \brief Split summands with disjuncts as conditions
      11             : 
      12             : #ifndef MCRL2_LPS_DECLUSTER_H
      13             : #define MCRL2_LPS_DECLUSTER_H
      14             : 
      15             : #include "mcrl2/data/join.h"
      16             : #include "mcrl2/lps/detail/lps_algorithm.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : namespace lps
      21             : {
      22             : 
      23             : template <typename Specification>
      24             : class decluster_algorithm: public detail::lps_algorithm<Specification>
      25             : {
      26             :   typedef typename detail::lps_algorithm<Specification> super;
      27             :   typedef typename Specification::process_type process_type;
      28             :   typedef typename process_type::action_summand_type action_summand_type;
      29             :   typedef std::vector<action_summand_type> action_summand_vector_type;
      30             :   using super::m_spec;
      31             : 
      32             :   protected:
      33             : 
      34             :     template <typename SummandType, typename OutIter>
      35           0 :     void decluster_summand(const SummandType& summand, OutIter& out)
      36             :     {
      37           0 :       for(const data::data_expression& disjunct: data::split_or(summand.condition()))
      38             :       {
      39           0 :         SummandType s(summand);
      40           0 :         s.condition() = disjunct;
      41           0 :         *out++ = s;
      42             :       }
      43           0 :     }
      44             : 
      45             :   public:
      46           0 :     decluster_algorithm(Specification& spec)
      47           0 :       : detail::lps_algorithm<Specification>(spec)
      48           0 :     {}
      49             : 
      50           0 :     void run()
      51             :     {
      52           0 :       action_summand_vector_type declustered_action_summands;
      53           0 :       std::back_insert_iterator<action_summand_vector_type> act_it(declustered_action_summands);
      54           0 :       auto const& action_summands = m_spec.process().action_summands();
      55           0 :       for (auto i = action_summands.begin(); i != action_summands.end(); ++i)
      56             :       {
      57           0 :         decluster_summand(*i, act_it);
      58             :       }
      59             : 
      60           0 :       deadlock_summand_vector declustered_deadlock_summands;
      61           0 :       std::back_insert_iterator<deadlock_summand_vector> dl_it (declustered_deadlock_summands);
      62           0 :       auto const& deadlock_summands = m_spec.process().deadlock_summands();
      63           0 :       for (auto i = deadlock_summands.begin(); i != deadlock_summands.end(); ++i)
      64             :       {
      65           0 :         decluster_summand(*i, dl_it);
      66             :       }
      67             : 
      68           0 :       m_spec.process().action_summands() = declustered_action_summands;
      69           0 :       m_spec.process().deadlock_summands() = declustered_deadlock_summands;
      70           0 :     }
      71             : 
      72             : }; // decluster_algorithm
      73             : 
      74             : } // namespace lps
      75             : } // namespace mcrl2
      76             : 
      77             : #endif // MCRL2_LPS_DECLUSTER_H
      78             :