pbes_gauss_elimination.h

Go to the documentation of this file.

// Author(s): Wieger Wesselink
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
/// \file mcrl2/pbes/pbes_gauss_elimination.h
/// \brief add your file description here.
 
#ifndef MCRL2_PBES_PBES_GAUSS_ELIMINATION_H
#define MCRL2_PBES_PBES_GAUSS_ELIMINATION_H
 
#include "mcrl2/pbes/gauss_elimination_algorithm.h"
#include "mcrl2/pbes/rewriters/enumerate_quantifiers_rewriter.h"
 
namespace mcrl2::pbes_system
{
 
/// \brief Traits class for pbes expressions
struct pbes_traits
{
  public:
    using expression_type = pbes_expression;
    using variable_type = propositional_variable;
    using equation_type = pbes_equation;
    using symbol_type = fixpoint_symbol;
 
    /// \brief Applies the substitution X := phi to the PBES expression t.
    /// \param t A PBES expression
    /// \param X A propositional variable
    /// \param phi A PBES expression
    /// \return The substition result
    static inline
    expression_type substitute(const expression_type& t, const variable_type& X, const expression_type& phi)
    {
      return replace_propositional_variables(t, propositional_variable_substitution(X, phi));
    }
 
    /// \brief Returns the value true
    static inline
    expression_type true_()
    {
      return core::term_traits<expression_type>::true_();
    }
 
    /// \brief Returns the value false
    static inline
    expression_type false_()
    {
      return core::term_traits<expression_type>::false_();
    }
 
    /// \brief Returns the fixpoint symbol mu
    static inline
    symbol_type mu()
    {
      return fixpoint_symbol::mu();
    }
 
    /// \brief Returns the fixpoint symbol nu
    static inline
    symbol_type nu()
    {
      return fixpoint_symbol::nu();
    }
 
    /// \brief Pretty print an equation without generating a newline after the equal sign
    /// \param eq An equation
    /// \return A pretty printed string
    static inline
    std::string print(const equation_type& eq)
    {
      return pbes_system::pp(eq.symbol()) + " " + pbes_system::pp(eq.variable()) + " = " + pbes_system::pp(eq.formula());
    }
};
 
/// \brief Solves an equation
/// \param e A pbes equation
template <typename Rewriter>
struct pbes_equation_solver
{
  const Rewriter& m_rewriter;
 
  pbes_equation_solver(const Rewriter& rewriter)
    : m_rewriter(rewriter)
  {}
 
  /// \brief Returns true if e.symbol() == nu(), else false.
  /// \param e A pbes equation
  /// \return True if e.symbol() == nu(), else false.
  pbes_expression sigma(const pbes_equation& e)
  {
    using tr = typename core::term_traits<pbes_expression>;
    return e.symbol().is_nu() ? tr::true_() : tr::false_();
  }
 
  /// \brief Solves the equation e
  void operator()(pbes_equation& e)
  {
    e.formula() = pbes_traits::substitute(e.formula(), e.variable(), sigma(e));
    e.formula() = m_rewriter(e.formula());
  }
};
 
/// \brief Utility function for creating a pbes_equation_solver
template <typename Rewriter>
pbes_equation_solver<Rewriter> make_pbes_equation_solver(const Rewriter& rewriter)
{
  return pbes_equation_solver<Rewriter>(rewriter);
}
 
/// \brief Solves a PBES equation system using Gauss elimination.
/// \pre The pbes \p p is a bes.
/// \param p A pbes
/// \return 0 if the solution is false, 1 if the solution is true, 2 if the solution is unknown
inline
int gauss_elimination(pbes& p)
{
  using tr = core::term_traits<pbes_expression>;
 
  data::rewriter datar(p.data());
  enumerate_quantifiers_rewriter pbesr(datar, p.data());
 
  gauss_elimination_algorithm<pbes_traits> algorithm;
  algorithm.run(p.equations().begin(), p.equations().end(), pbes_equation_solver<enumerate_quantifiers_rewriter>(pbesr));
 
  if (tr::is_false(p.equations().front().formula()))
  {
    return 0;
  }
  else if (tr::is_true(p.equations().front().formula()))
  {
    return 1;
  }
  else
  {
    return 2;
  }
}
 
} // namespace mcrl2::pbes_system
 
#endif // MCRL2_PBES_PBES_GAUSS_ELIMINATION_H