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/pbes/gauss_elimination_algorithm.h
      10             : /// \brief Gauss elimination algorithm for pbes equation systems.
      11             : 
      12             : #ifndef MCRL2_PBES_GAUSS_ELIMINATION_ALGORITHM_H
      13             : #define MCRL2_PBES_GAUSS_ELIMINATION_ALGORITHM_H
      14             : 
      15             : #include "mcrl2/pbes/replace.h"
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : 
      20             : namespace pbes_system
      21             : {
      22             : 
      23             : /// \brief Algorithm class for the Gauss elimination algorithm for solving
      24             : /// systems of (P)BES equations.
      25             : 
      26             : template <typename ExpressionTraits>
      27             : class gauss_elimination_algorithm
      28             : {
      29             :   public:
      30             :     typedef typename ExpressionTraits::expression_type expression_type;
      31             :     typedef typename ExpressionTraits::variable_type variable_type;
      32             :     typedef typename ExpressionTraits::equation_type equation_type;
      33             : 
      34             :   protected:
      35             : 
      36           0 :     std::string print_equation(const equation_type& eq) const
      37             :     {
      38           0 :       return ExpressionTraits::print(eq);
      39             :     }
      40             : 
      41             :     template <typename Iter>
      42           0 :     std::string print_equations(Iter first, Iter last) const
      43             :     {
      44           0 :       std::ostringstream out;
      45           0 :       for (Iter i = first; i != last; ++i)
      46             :       {
      47           0 :         out << "  " << print_equation(*i) << std::endl;
      48             :       }
      49           0 :       return out.str();
      50           0 :     }
      51             : 
      52             :   public:
      53             :     /// \brief Runs the algorithm. Applies Gauss elimination to the sequence of pbes equations [first, last).
      54             :     /// \param first Start of a range of pbes equations
      55             :     /// \param last End of a range of pbes equations
      56             :     /// \param solve An equation solver
      57             : 
      58             :     template <typename Iter, typename FixpointEquationSolver>
      59          21 :     void run(Iter first, Iter last, FixpointEquationSolver solve)
      60             :     {
      61          21 :       mCRL2log(log::debug) << "equations before solving\n" << print_equations(first, last);
      62          21 :       if (first == last)
      63             :       {
      64           0 :         return;
      65             :       }
      66             : 
      67          21 :       Iter i = last;
      68          65 :       while (i != first)
      69             :       {
      70          44 :         --i;
      71          44 :         mCRL2log(log::verbose) << "solving equation\n  before: " << print_equation(*i);
      72          44 :         solve(*i);
      73          44 :         mCRL2log(log::verbose) << "   after: " << print_equation(*i) << "\n";
      74          85 :         for (Iter j = first; j != i; ++j)
      75             :         {
      76          41 :           j->formula() = ExpressionTraits::substitute(j->formula(), i->variable(), i->formula());
      77             :         }
      78          44 :         mCRL2log(log::trace) << "equations after substitution\n" << print_equations(first, last);
      79             :       }
      80          21 :       mCRL2log(log::debug) << "equations after solving\n" << print_equations(first, last);
      81             :     }
      82             : };
      83             : 
      84             : /// \brief Approximation algorithm
      85             : 
      86             : template <typename BooleanExpressionTraits, typename Compare>
      87             : struct approximate
      88             : {
      89             :   Compare m_compare;
      90             : 
      91           1 :   approximate(Compare compare)
      92           1 :     : m_compare(compare)
      93             :   {
      94           1 :   }
      95             : 
      96           2 :   void operator()(typename BooleanExpressionTraits::equation_type& eq) const
      97             :   {
      98             :     typedef BooleanExpressionTraits tr;
      99             :     typedef typename BooleanExpressionTraits::expression_type expression_type;
     100             :     typedef typename BooleanExpressionTraits::variable_type variable_type;
     101             : 
     102           2 :     const expression_type& phi = eq.formula();
     103           2 :     const variable_type& X = eq.variable();
     104           2 :     expression_type next = eq.symbol() == tr::nu() ? tr::true_() : tr::false_();
     105           2 :     expression_type prev;
     106             :     do
     107             :     {
     108           3 :       prev = next;
     109           3 :       next = tr::substitute(phi, X, prev);
     110             :     }
     111           3 :     while (!m_compare(prev, next));
     112           2 :     eq.formula() = prev;
     113           2 :   }
     114             : };
     115             : 
     116             : } // namespace pbes_system
     117             : 
     118             : } // namespace mcrl2
     119             : 
     120             : #endif // MCRL2_PBES_GAUSS_ELIMINATION_ALGORITHM_H