LCOV - code coverage report
Current view: top level - bes/include/mcrl2/bes - small_progress_measures.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 126 158 79.7 %
Date: 2020-10-20 00:45:57 Functions: 20 25 80.0 %
Legend: Lines: hit not hit

          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/bes/small_progress_measures.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_BES_SMALL_PROGRESS_MEASURES_H
      13             : #define MCRL2_BES_SMALL_PROGRESS_MEASURES_H
      14             : 
      15             : // TODO: Make it possible to undefine this flag
      16             : #define MCRL2_SMALL_PROGRESS_MEASURES_DEBUG
      17             : 
      18             : #include "mcrl2/bes/find.h"
      19             : #include "mcrl2/bes/normal_forms.h"
      20             : #include "mcrl2/bes/print.h"
      21             : #include "mcrl2/core/detail/print_utility.h"
      22             : #include <iomanip>
      23             : 
      24             : namespace mcrl2
      25             : {
      26             : 
      27             : namespace bes
      28             : {
      29             : 
      30             : template <typename T>
      31          19 : bool is_odd(T t)
      32             : {
      33          19 :   return t % 2 != 0;
      34             : }
      35             : 
      36             : template <typename T>
      37           9 : bool is_even(T t)
      38             : {
      39           9 :   return t % 2 == 0;
      40             : }
      41             : 
      42             : template <typename InputIterator1, typename InputIterator2>
      43           9 : int lexicographical_compare_3way(InputIterator1 first1, InputIterator1 last1,
      44             :                                  InputIterator2 first2, InputIterator2 last2)
      45             : {
      46          14 :   while (first1 != last1 && first2 != last2)
      47             :   {
      48           8 :     if (*first1 < *first2)
      49             :     {
      50           2 :       return -1;
      51             :     }
      52           6 :     if (*first2 < *first1)
      53             :     {
      54           1 :       return 1;
      55             :     }
      56           5 :     ++first1;
      57           5 :     ++first2;
      58             :   }
      59           1 :   if (first2 == last2)
      60             :   {
      61           1 :     return !(first1 == last1);
      62             :   }
      63             :   else
      64             :   {
      65           0 :     return -1;
      66             :   }
      67             : }
      68             : 
      69             : inline
      70           7 : bool is_disjunctive(const boolean_expression& x)
      71             : {
      72           7 :   return is_or(x);
      73             : }
      74             : 
      75             : //inline
      76             : //unsigned int mu_block_count(const boolean_equation_system& b)
      77             : //{
      78             : //  unsigned int result = 0;
      79             : //  fixpoint_symbol last_symbol = fixpoint_symbol::nu();
      80             : //  for (const boolean_equation& eqn: b.equations())
      81             : //  {
      82             : //    if (eqn.symbol().is_mu() && last_symbol.is_nu())
      83             : //    {
      84             : //      result++;
      85             : //    }
      86             : //    last_symbol = eqn.symbol();
      87             : //  }
      88             : //  return result;
      89             : //}
      90             : //
      91             : //inline
      92             : //unsigned int block_count(const boolean_equation_system& b)
      93             : //{
      94             : //  unsigned int result = 0;
      95             : //  fixpoint_symbol last_symbol;
      96             : //  for (auto i = b.equations().begin(); i != b.equations().end(); ++i)
      97             : //  {
      98             : //    if (i == b.equations().begin() || (i->symbol() != last_symbol))
      99             : //    {
     100             : //      result++;
     101             : //    }
     102             : //    last_symbol = i->symbol();
     103             : //  }
     104             : //  return result;
     105             : //}
     106             : 
     107             : inline
     108           3 : int maximum_rank(const boolean_equation_system& b)
     109             : {
     110           3 :   int result = 0;
     111           6 :   fixpoint_symbol last_symbol;
     112          10 :   for (auto i = b.equations().begin(); i != b.equations().end(); ++i)
     113             :   {
     114           7 :     if (i == b.equations().begin())
     115             :     {
     116           3 :       result = i->symbol().is_nu() ? 0 : 1;
     117             :     }
     118           4 :     else if (i->symbol() != last_symbol)
     119             :     {
     120           4 :       result++;
     121             :     }
     122           7 :     last_symbol = i->symbol();
     123             :   }
     124           6 :   return result;
     125             : }
     126             : 
     127          21 : struct progress_measure
     128             : {
     129          14 :   explicit progress_measure(std::size_t d)
     130          14 :     : v(d, 0)
     131          14 :   {}
     132             : 
     133             :   // N.B. The special value top is represented by alpha[0] == -1
     134             :   std::vector<int> v;
     135             : 
     136          20 :   bool is_top() const
     137             :   {
     138          20 :     return v[0] == -1;
     139             :   }
     140             : };
     141             : 
     142             : inline
     143           0 : std::ostream& operator<<(std::ostream& out, const progress_measure& pm)
     144             : {
     145           0 :   if (pm.is_top())
     146             :   {
     147           0 :     out << "top";
     148             :   }
     149             :   else
     150             :   {
     151           0 :     out << core::detail::print_list(pm.v);
     152             :   }
     153           0 :   return out;
     154             : }
     155             : 
     156             : // increment position m of vector alpha
     157             : inline
     158          15 : void inc(std::vector<int>& alpha, int m, const std::vector<int>& beta)
     159             : {
     160          15 :   if (alpha[0] == -1)
     161             :   {
     162           2 :     return;
     163             :   }
     164          13 :   else if (m == -1)
     165             :   {
     166           2 :     alpha[0] = -1;
     167           2 :     return;
     168             :   }
     169          11 :   else if (alpha[m] == beta[m])
     170             :   {
     171           4 :     alpha[m] = 0;
     172           4 :     inc(alpha, m - 1, beta);
     173             :   }
     174             :   else
     175             :   {
     176           7 :     alpha[m]++;
     177             :   }
     178             : }
     179             : 
     180             : /// \brief Vertex of the progress measures graph
     181          21 : struct progress_measures_vertex
     182             : {
     183          14 :   explicit progress_measures_vertex(bool even_ = false, int rank_ = 0, unsigned int d = 1)
     184          14 :     : even(even_),
     185             :       rank(rank_),
     186          14 :       alpha(d)
     187          14 :   {}
     188             : 
     189             :   std::vector<progress_measures_vertex*> successors;
     190             :   bool even;
     191             :   int rank;
     192             :   progress_measure alpha;
     193             : 
     194             : #ifdef MCRL2_SMALL_PROGRESS_MEASURES_DEBUG
     195             :   std::string name;
     196             : #endif
     197             : };
     198             : 
     199             : // compare the positions with index in [0, ... ,m]
     200             : struct compare_progress_measures_vertex
     201             : {
     202             :   unsigned int m;
     203             : 
     204          19 :   explicit compare_progress_measures_vertex(unsigned int m_)
     205          19 :     : m(m_)
     206          19 :   {}
     207             : 
     208           9 :   bool operator()(const progress_measures_vertex* x, const progress_measures_vertex* y) const
     209             :   {
     210           9 :     if (x->alpha.is_top())
     211             :     {
     212           1 :       return false;
     213             :     }
     214           8 :     else if (y->alpha.is_top())
     215             :     {
     216           4 :       return true;
     217             :     }
     218           4 :     int n = lexicographical_compare_3way(x->alpha.v.begin(), x->alpha.v.begin() + m + 1, y->alpha.v.begin(), y->alpha.v.begin() + m + 1);
     219             :     //if (n == 0)
     220             :     //{
     221             :     //  return is_even(x->rank) && is_odd(y->rank);
     222             :     //}
     223           4 :     return n < 0;
     224             :   }
     225             : };
     226             : 
     227             : inline
     228           0 : std::ostream& operator<<(std::ostream& out, const progress_measures_vertex& v)
     229             : {
     230           0 :   out << " alpha = " << v.alpha;
     231           0 :   out << " successors = {";
     232           0 :   for (auto i = v.successors.begin(); i != v.successors.end(); ++i)
     233             :   {
     234           0 :     if (i != v.successors.begin())
     235             :     {
     236           0 :       out << ", ";
     237             :     }
     238           0 :     out << std::string((*i)->name);
     239             :   }
     240           0 :   out << "}";
     241           0 :   out << " rank = " << v.rank;
     242           0 :   out << " disjunctive = " << std::boolalpha << v.even;
     243           0 :   return out;
     244             : }
     245             : 
     246             : /// \brief Algorithm class for the small progress measures algorithm
     247           3 : class small_progress_measures_algorithm
     248             : {
     249             :   protected:
     250             :     typedef progress_measures_vertex vertex;
     251             :     typedef std::map<boolean_variable, vertex> vertex_map;
     252             : 
     253           3 :     void initialize_vertices()
     254             :     {
     255             :       // first build the vertex map without successor information
     256           3 :       m_d = maximum_rank(m_bes) + 1;
     257           3 :       unsigned int block_size = 0;
     258           3 :       int last_rank = 0;
     259           6 :       fixpoint_symbol last_symbol = fixpoint_symbol::nu();
     260          10 :       for (const boolean_equation& eqn: m_bes.equations())
     261             :       {
     262           7 :         if (eqn.symbol() != last_symbol)
     263             :         {
     264           6 :           if (is_even(m_beta.size()))
     265             :           {
     266           4 :             m_beta.push_back(0);
     267             :           }
     268             :           else
     269             :           {
     270           2 :             m_beta.push_back(block_size);
     271             :           }
     272           6 :           block_size = 0;
     273           6 :           last_rank++;
     274           6 :           last_symbol = eqn.symbol();
     275             :         }
     276           7 :         block_size++;
     277           7 :         m_vertices[eqn.variable()] = vertex(is_disjunctive(eqn.formula()), last_rank, m_d);
     278             :       }
     279           3 :       if (is_even(m_beta.size()))
     280             :       {
     281           1 :         m_beta.push_back(0);
     282             :       }
     283             :       else
     284             :       {
     285           2 :         m_beta.push_back(block_size);
     286             :       }
     287             : 
     288             :       // add successor information
     289          10 :       for (const boolean_equation& eqn: m_bes.equations())
     290             :       {
     291          14 :         std::set<boolean_variable> succ = bes::find_boolean_variables(eqn.formula());
     292           7 :         auto k = m_vertices.find(eqn.variable());
     293           7 :         std::vector<vertex*>& k_successors = k->second.successors;
     294          17 :         for (const boolean_variable& v: succ)
     295             :         {
     296          10 :           k_successors.push_back(&m_vertices[v]);
     297             :         }
     298             : 
     299             : #ifdef MCRL2_SMALL_PROGRESS_MEASURES_DEBUG
     300           7 :         k->second.name = std::string(eqn.variable().name());
     301             : #endif
     302             :       }
     303           3 :     }
     304             : 
     305           0 :     std::string print_vertices() const
     306             :     {
     307           0 :       std::ostringstream out;
     308           0 :       for (const boolean_equation& eqn: m_bes.equations())
     309             :       {
     310           0 :         const vertex& v = m_vertices.find(eqn.variable())->second;
     311           0 :         out << v.name << " " << v << std::endl;
     312             :       }
     313           0 :       return out.str();
     314             :     }
     315             : 
     316           0 :     std::string print_vertex(const vertex& v) const
     317             :     {
     318           0 :       std::ostringstream out;
     319           0 :       out << v.name << " (alpha = " << v.alpha << ", rank = " << v.rank << ")";
     320           0 :       return out.str();
     321             :     }
     322             : 
     323             :     /// \brief Logs the neighbors of a vertex
     324           0 :     std::string print_neighbors(const progress_measures_vertex& v) const
     325             :     {
     326           0 :       std::ostringstream out;
     327           0 :       for (progress_measures_vertex* successor: v.successors)
     328             :       {
     329           0 :         out << "\n      " << print_vertex(*successor);
     330             :       }
     331           0 :       return out.str();
     332             :     }
     333             : 
     334             :     vertex_map m_vertices;
     335             :     int m_d = 0;
     336             :     const boolean_equation_system& m_bes;
     337             :     std::vector<int> m_beta;
     338             : 
     339             :   public:
     340           3 :     explicit small_progress_measures_algorithm(const boolean_equation_system& b)
     341           3 :       : m_bes(b)
     342           3 :     {}
     343             : 
     344           3 :     bool run(const boolean_variable& first_variable)
     345             :     {
     346           3 :       mCRL2log(log::verbose) << "Applying small progress measures.\n";
     347           3 :       mCRL2log(log::debug)  << "BES " << bes::pp(m_bes) << "\n\n";
     348           3 :       initialize_vertices();
     349           3 :       mCRL2log(log::debug) << "--- vertices ---\n" << print_vertices();
     350           3 :       mCRL2log(log::debug) << "\nbeta = " << core::detail::print_list(m_beta) << "\n";
     351             :       for (;;) // forever
     352             :       {
     353           8 :         bool changed = false;
     354          27 :         for (auto &i: m_vertices)
     355             :         {
     356          19 :           vertex& v = i.second;
     357          19 :           mCRL2log(log::debug) << "\nchoose vertex " << print_vertex(v);
     358          19 :           int m = v.rank;
     359          19 :           std::vector<progress_measures_vertex*>::const_iterator j;
     360          19 :           mCRL2log(log::debug) << "\n    neighbors:" << print_neighbors(v);
     361          19 :           if (v.even)
     362             :           {
     363           6 :             j = std::min_element(v.successors.begin(), v.successors.end(), compare_progress_measures_vertex(m));
     364           6 :             mCRL2log(log::debug) << "\n    minimum neighbor " << print_vertex(**j);
     365             :           }
     366             :           else
     367             :           {
     368          13 :             j = std::max_element(v.successors.begin(), v.successors.end(), compare_progress_measures_vertex(m));
     369          13 :             mCRL2log(log::debug) << "\n    maximum neighbor " << print_vertex(**j);
     370             :           }
     371          38 :           std::vector<int> alpha(m_d, 0);
     372          19 :           const progress_measures_vertex& w = **j;
     373          19 :           std::copy(w.alpha.v.begin(),  w.alpha.v.begin() + m + 1, alpha.begin());
     374          19 :           if (is_odd(m))
     375             :           {
     376          11 :             mCRL2log(log::debug) << "\n    inc(" << core::detail::print_list(alpha) << ", " << std::to_string(m) << ") = ";
     377          11 :             inc(alpha, m, m_beta);
     378          11 :             mCRL2log(log::debug) << (alpha[0] < 0 ? "top" : core::detail::print_list(alpha));
     379             :           }
     380             : 
     381          19 :           if (!std::equal(alpha.begin(), alpha.end(), v.alpha.v.begin()))
     382             :           {
     383           8 :             changed = true;
     384           8 :             v.alpha.v = alpha;
     385           8 :             mCRL2log(log::debug) << "\nupdate vertex " << print_vertex(v);
     386             :           }
     387             :         }
     388           8 :         if (!changed)
     389             :         {
     390           3 :           break;
     391             :         }
     392           5 :       }
     393           3 :       mCRL2log(log::debug) << "\n--- vertices ---\n" << print_vertices();
     394           3 :       return !m_vertices[first_variable].alpha.is_top();
     395             :     }
     396             : };
     397             : 
     398             : inline
     399           3 : bool small_progress_measures(boolean_equation_system& b)
     400             : {
     401           6 :   boolean_variable first = b.equations().front().variable();
     402           3 :   make_standard_form(b, true);
     403           6 :   small_progress_measures_algorithm algorithm(b);
     404           6 :   return algorithm.run(first);
     405             : }
     406             : 
     407             : } // namespace bes
     408             : 
     409             : } // namespace mcrl2
     410             : 
     411             : #endif // MCRL2_BES_SMALL_PROGRESS_MEASURES_H

Generated by: LCOV version 1.13