LCOV - code coverage report
Current view: top level - bes/include/mcrl2/bes - gauss_elimination.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 17 20 85.0 %
Date: 2020-10-20 00:45:57 Functions: 5 6 83.3 %
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/gauss_elimination.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_BES_GAUSS_ELIMINATION_H
      13             : #define MCRL2_BES_GAUSS_ELIMINATION_H
      14             : 
      15             : #include "mcrl2/bes/print.h"
      16             : #include "mcrl2/bes/replace.h"
      17             : #include "mcrl2/bes/simplify_rewriter.h"
      18             : #include "mcrl2/pbes/gauss_elimination.h"
      19             : 
      20             : namespace mcrl2
      21             : {
      22             : 
      23             : namespace bes
      24             : {
      25             : 
      26             : /// \brief Traits class for pbes expressions
      27             : struct bes_traits
      28             : {
      29             :   public:
      30             :     typedef boolean_expression expression_type;
      31             :     typedef boolean_variable variable_type;
      32             :     typedef boolean_equation equation_type;
      33             :     typedef bes::fixpoint_symbol symbol_type;
      34             : 
      35             :     /// \brief Applies the substitution X := phi to the boolean expression t.
      36             :     /// \param t A boolean expression
      37             :     /// \param X A boolean variable
      38             :     /// \param phi A boolean expression
      39             :     /// \return The substition result
      40             :     static inline
      41          20 :     expression_type substitute(const expression_type& t, const variable_type& X, const expression_type& phi)
      42             :     {
      43          20 :       expression_type result=bes::replace_boolean_variables(t, boolean_variable_substitution(X, phi));
      44          20 :       return result;
      45             :     }
      46             : 
      47             :     /// \brief Returns the value true
      48             :     static inline
      49             :     expression_type true_()
      50             :     {
      51             :       return core::term_traits<expression_type>::true_();
      52             :     }
      53             : 
      54             :     /// \brief Returns the value false
      55             :     static inline
      56             :     expression_type false_()
      57             :     {
      58             :       return core::term_traits<expression_type>::false_();
      59             :     }
      60             : 
      61             :     /// \brief Returns the fixpoint symbol mu
      62             :     static inline
      63             :     symbol_type mu()
      64             :     {
      65             :       return fixpoint_symbol::mu();
      66             :     }
      67             : 
      68             :     /// \brief Returns the fixpoint symbol nu
      69             :     static inline
      70             :     symbol_type nu()
      71             :     {
      72             :       return fixpoint_symbol::nu();
      73             :     }
      74             : 
      75             :     /// \brief Pretty print an equation without generating a newline after the equal sign
      76             :     /// \param eq An equation
      77             :     /// \return A pretty printed string
      78             :     static inline
      79           0 :     std::string print(const equation_type& eq)
      80             :     {
      81           0 :       return bes::pp(eq);
      82             :     }
      83             : };
      84             : 
      85             : /// \brief Solves an equation
      86             : /// \param e A bes equation
      87             : template <typename Rewriter>
      88             : struct boolean_equation_solver
      89             : {
      90             :   const Rewriter& m_rewriter;
      91             : 
      92           7 :   boolean_equation_solver(const Rewriter& rewriter)
      93           7 :     : m_rewriter(rewriter)
      94           7 :   {}
      95             : 
      96             :   /// \brief Returns true if e.symbol() == nu(), else false.
      97             :   /// \param e A pbes equation
      98             :   /// \return True if e.symbol() == nu(), else false.
      99          13 :   boolean_expression sigma(const boolean_equation& e)
     100             :   {
     101             :     typedef typename core::term_traits<boolean_expression> tr;
     102          13 :     return e.symbol().is_nu() ? tr::true_() : tr::false_();
     103             :   }
     104             : 
     105             :   /// \brief Solves the equation e
     106          13 :   void operator()(boolean_equation& e)
     107             :   {
     108          13 :     e.formula() = m_rewriter(bes_traits::substitute(e.formula(), e.variable(), sigma(e)));
     109          13 :   }
     110             : };
     111             : 
     112             : /// \brief Utility function for creating a boolean_equation_solver
     113             : template <typename Rewriter>
     114             : boolean_equation_solver<Rewriter> make_boolean_equation_solver(const Rewriter& rewriter)
     115             : {
     116             :   return boolean_equation_solver<Rewriter>(rewriter);
     117             : }
     118             : 
     119             : /// \brief Solves a boolean equation system using Gauss elimination.
     120             : /// \param p A bes
     121             : /// \return The solution of the system
     122             : inline
     123           7 : bool gauss_elimination(boolean_equation_system& p)
     124             : {
     125             :   typedef core::term_traits<boolean_expression> tr;
     126             :   typedef simplify_rewriter bes_rewriter;
     127             : 
     128             :   pbes_system::gauss_elimination_algorithm<bes_traits> algorithm;
     129             :   bes_rewriter besr;
     130           7 :   algorithm.run(p.equations().begin(), p.equations().end(), boolean_equation_solver<bes_rewriter>(besr));
     131           7 :   if (tr::is_false(p.equations().front().formula()))
     132             :   {
     133           4 :     return false;
     134             :   }
     135           3 :   else if (tr::is_true(p.equations().front().formula()))
     136             :   {
     137           3 :     return true;
     138             :   }
     139             :   else
     140             :   {
     141           0 :     throw std::runtime_error("fatal error in bes::gauss_elimination");
     142             :   }
     143             :   return false;
     144             : }
     145             : 
     146             : } // namespace bes
     147             : 
     148             : } // namespace mcrl2
     149             : 
     150             : #endif // MCRL2_BES_GAUSS_ELIMINATION_H

Generated by: LCOV version 1.13