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/pbes_gauss_elimination.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_PBES_GAUSS_ELIMINATION_H
      13             : #define MCRL2_PBES_PBES_GAUSS_ELIMINATION_H
      14             : 
      15             : #include "mcrl2/pbes/gauss_elimination_algorithm.h"
      16             : #include "mcrl2/pbes/rewriters/enumerate_quantifiers_rewriter.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : 
      21             : namespace pbes_system
      22             : {
      23             : 
      24             : /// \brief Traits class for pbes expressions
      25             : struct pbes_traits
      26             : {
      27             :   public:
      28             :     typedef pbes_expression expression_type;
      29             :     typedef propositional_variable variable_type;
      30             :     typedef pbes_equation equation_type;
      31             :     typedef fixpoint_symbol symbol_type;
      32             : 
      33             :     /// \brief Applies the substitution X := phi to the PBES expression t.
      34             :     /// \param t A PBES expression
      35             :     /// \param X A propositional variable
      36             :     /// \param phi A PBES expression
      37             :     /// \return The substition result
      38             :     static inline
      39          84 :     expression_type substitute(const expression_type& t, const variable_type& X, const expression_type& phi)
      40             :     {
      41         168 :       return replace_propositional_variables(t, propositional_variable_substitution(X, phi));
      42             :     }
      43             : 
      44             :     /// \brief Returns the value true
      45             :     static inline
      46           1 :     expression_type true_()
      47             :     {
      48           1 :       return core::term_traits<expression_type>::true_();
      49             :     }
      50             : 
      51             :     /// \brief Returns the value false
      52             :     static inline
      53           1 :     expression_type false_()
      54             :     {
      55           1 :       return core::term_traits<expression_type>::false_();
      56             :     }
      57             : 
      58             :     /// \brief Returns the fixpoint symbol mu
      59             :     static inline
      60             :     symbol_type mu()
      61             :     {
      62             :       return fixpoint_symbol::mu();
      63             :     }
      64             : 
      65             :     /// \brief Returns the fixpoint symbol nu
      66             :     static inline
      67           2 :     symbol_type nu()
      68             :     {
      69           2 :       return fixpoint_symbol::nu();
      70             :     }
      71             : 
      72             :     /// \brief Pretty print an equation without generating a newline after the equal sign
      73             :     /// \param eq An equation
      74             :     /// \return A pretty printed string
      75             :     static inline
      76           0 :     std::string print(const equation_type& eq)
      77             :     {
      78           0 :       return pbes_system::pp(eq.symbol()) + " " + pbes_system::pp(eq.variable()) + " = " + pbes_system::pp(eq.formula());
      79             :     }
      80             : };
      81             : 
      82             : /// \brief Solves an equation
      83             : /// \param e A pbes equation
      84             : template <typename Rewriter>
      85             : struct pbes_equation_solver
      86             : {
      87             :   const Rewriter& m_rewriter;
      88             : 
      89          19 :   pbes_equation_solver(const Rewriter& rewriter)
      90          19 :     : m_rewriter(rewriter)
      91          19 :   {}
      92             : 
      93             :   /// \brief Returns true if e.symbol() == nu(), else false.
      94             :   /// \param e A pbes equation
      95             :   /// \return True if e.symbol() == nu(), else false.
      96          40 :   pbes_expression sigma(const pbes_equation& e)
      97             :   {
      98             :     typedef typename core::term_traits<pbes_expression> tr;
      99          40 :     return e.symbol().is_nu() ? tr::true_() : tr::false_();
     100             :   }
     101             : 
     102             :   /// \brief Solves the equation e
     103          40 :   void operator()(pbes_equation& e)
     104             :   {
     105          40 :     e.formula() = pbes_traits::substitute(e.formula(), e.variable(), sigma(e));
     106          40 :     e.formula() = m_rewriter(e.formula());
     107          40 :   }
     108             : };
     109             : 
     110             : /// \brief Utility function for creating a pbes_equation_solver
     111             : template <typename Rewriter>
     112             : pbes_equation_solver<Rewriter> make_pbes_equation_solver(const Rewriter& rewriter)
     113             : {
     114             :   return pbes_equation_solver<Rewriter>(rewriter);
     115             : }
     116             : 
     117             : /// \brief Solves a PBES equation system using Gauss elimination.
     118             : /// \pre The pbes \p p is a bes.
     119             : /// \param p A pbes
     120             : /// \return 0 if the solution is false, 1 if the solution is true, 2 if the solution is unknown
     121             : inline
     122          19 : int gauss_elimination(pbes& p)
     123             : {
     124             :   typedef core::term_traits<pbes_expression> tr;
     125             : 
     126          19 :   data::rewriter datar(p.data());
     127          19 :   enumerate_quantifiers_rewriter pbesr(datar, p.data());
     128             : 
     129             :   gauss_elimination_algorithm<pbes_traits> algorithm;
     130          19 :   algorithm.run(p.equations().begin(), p.equations().end(), pbes_equation_solver<enumerate_quantifiers_rewriter>(pbesr));
     131             : 
     132          19 :   if (tr::is_false(p.equations().front().formula()))
     133             :   {
     134          11 :     return 0;
     135             :   }
     136           8 :   else if (tr::is_true(p.equations().front().formula()))
     137             :   {
     138           8 :     return 1;
     139             :   }
     140             :   else
     141             :   {
     142           0 :     return 2;
     143             :   }
     144          19 : }
     145             : 
     146             : } // namespace pbes_system
     147             : 
     148             : } // namespace mcrl2
     149             : 
     150             : #endif // MCRL2_PBES_PBES_GAUSS_ELIMINATION_H