normalize.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)
//
 
#ifndef MCRL2_MODAL_FORMULA_NORMALIZE_H
#define MCRL2_MODAL_FORMULA_NORMALIZE_H
 
#include "mcrl2/modal_formula/negate_variables.h"
#include "mcrl2/modal_formula/traverser.h"
 
namespace mcrl2
{
 
namespace state_formulas
{
 
// \brief Visitor for checking if a state formula is normalized.
struct is_normalized_traverser: public state_formula_traverser<is_normalized_traverser>
{
  typedef state_formula_traverser<is_normalized_traverser> super;
  using super::enter;
  using super::leave;
  using super::apply;
 
  bool result;
 
  is_normalized_traverser()
    : result(true)
  {}
 
  void enter(const not_& /* x */)
  {
    result = false;
  }
 
  void enter(const minus& /* x */)
  {
    result = false;
  }
 
  void enter(const imp& /* x */)
  {
    result = false;
  }
};
 
 
// \brief Visitor for normalizing a state formula.
struct normalize_builder: public state_formula_builder<normalize_builder>
{
  typedef state_formula_builder<normalize_builder> super;
  using super::enter;
  using super::leave;
  using super::update;
  using super::apply;
 
  bool m_quantitative;
  bool m_negated;
 
  // negated indicates that the formulas is under a negation.
  // quantitative indicates that the formula yields a real value, 
  // in which case forall, exists and not are replaced by supremum, infimum and minus. 
  normalize_builder(bool quantitative, bool negated)
    : m_quantitative(quantitative),
      m_negated(negated)
  {}
 
  template <class T>
  void apply(T& result, const data::data_expression& x)
  {
    if (m_quantitative)
    {
      if (m_negated)
      {
        if (x.sort()==data::sort_bool::bool_()) 
        {
          result = data::sort_bool::not_(x);
        }
        else
        {
          result = data::sort_real::negate(x);
        }
      }
      else
      {
        result = x;
      }
    }
    else // x is an ordinary modal formula.
    {
      assert(x.sort()==data::sort_bool::bool_());
      result = m_negated ? data::sort_bool::not_(x) : x;
    }
  }
 
  template <class T>
  void apply(T& result, const true_& /*x*/)
  {
    if (m_negated)
    {
      result = false_();
    }
    else
    {
      result = true_();
    }
  }
 
  template <class T>
  void apply(T& result, const false_& /*x*/)
  {
    if (m_negated)
    {
      result = true_();
    }
    else
    {
      result = false_();
    }
  }
 
  template <class T>
  void apply(T& result, const not_& x)
  {
    assert(!m_quantitative);
    m_negated=!m_negated;
    apply(result, x.operand());
    m_negated=!m_negated;
  }
 
  template <class T>
  void apply(T& result, const minus& x)
  {
    assert(m_quantitative);
    m_negated=!m_negated;
    apply(result, x.operand());
    m_negated=!m_negated;
  }
 
  template <class T>
  void apply(T& result, const and_& x)
  {
    state_formula left, right;
    apply(left, x.left());
    apply(right, x.right()); 
    if (m_negated)
    {
      make_or_(result, left, right);
    }
    else
    {
      make_and_(result, left, right);
    }
  }
 
  template <class T>
  void apply(T& result, const or_& x)
  {
    state_formula left, right;
    apply(left, x.left());
    apply(right, x.right()); 
    if (m_negated)
    {
      make_and_(result, left, right);
    }
    else
    {
      make_or_(result, left, right);
    }
  }
 
  template <class T>
  void apply(T& result, const plus& x)
  {
    state_formula left, right;
    apply(left, x.left());
    apply(right, x.right()); 
    if (m_negated)
    {
      // The plus operator can be inverted if for instance the operator eq_mininf(x) is present, being equal to -infinity
      // if x is minus infinity, and being plus infinity otherwise. 
      // The dual plus then is: e1 dual+ e2 = eq_mininf(e1) && eq_mininf(e2) && (e1+e2).
      throw mcrl2::runtime_error("Cannot negate the plus operator in quantitative modal formulas: " + pp(x) + ".");
    }
    else
    {
      make_plus(result, left, right);
    }
  }
 
  template <class T>
  void apply(T& result, const imp& x)
  {
    state_formula y = m_quantitative ?
                        or_(minus(x.left()), x.right()) :
                        or_(not_(x.left()), x.right());
    apply(result, y);
  }
 
  template <class T>
  void apply(T& result, const forall& x)
  {
    state_formula body;
    apply(body, x.body());
    if (m_negated)
    {
      state_formulas::make_exists(result, x.variables(), body); 
    }
    else
    {
      state_formulas::make_forall(result, x.variables(), body);
    }
  }
 
  template <class T>
  void apply(T& result, const exists& x)
  {
    state_formula body;
    apply(body, x.body());
    if (m_negated)
    {
      state_formulas::make_forall(result, x.variables(), body); 
    }
    else
    {
      state_formulas::make_exists(result, x.variables(), body);
    }
  }
 
  template <class T>
  void apply(T& result, const supremum& x)
  {
    state_formula body;
    apply(body, x.body());
    if (m_negated)
    {
      make_infimum(result, x.variables(), body);
    }
    else
    {
      make_supremum(result, x.variables(), body); 
    }
  }
 
  template <class T>
  void apply(T& result, const infimum& x)
  {
    state_formula body;
    apply(body, x.body());
    if (m_negated)
    {
      make_supremum(result, x.variables(), body); 
    }
    else
    {
      make_infimum(result, x.variables(), body);
    }
  }
 
  template <class T>
  void apply(T& result, const sum& x)
  {
    state_formula body;
    apply(body, x.body());
    make_sum(result, x.variables(), body);
  }
 
  template <class T>
  void apply(T& result, const variable& x)
  {
    if (m_negated)
    {
      throw mcrl2::runtime_error(std::string("normalize error: illegal argument ") + pp(x));
    }
    result = x;
  }
 
  template <class T>
  void apply(T& result, const must& x)
  {
    state_formula operand;
    apply(operand, x.operand());
    if (m_negated)
    {
      make_may(result, x.formula(), operand);
    }
    else
    {
      make_must(result, x.formula(), operand);
    }
  }
 
  template <class T>
  void apply(T& result, const may& x)
  {
    state_formula operand;
    apply(operand, x.operand());
    if (m_negated)
    {
      make_must(result, x.formula(), operand);
    }
    else
    {
      make_may(result, x.formula(), operand);
    }
  }
 
  template <class T>
  void apply(T& result, const mu& x)
  {
    state_formula operand;
    if (m_negated)
    {
      apply(operand, negate_variables(x.name(), m_quantitative, x.operand()));
      make_nu(result, x.name(), x.assignments(), operand);
    }
    else
    {
      apply(operand, x.operand());
      make_mu(result, x.name(), x.assignments(), operand);
    }
  }
 
  template <class T>
  void apply(T& result, const nu& x)
  {
    state_formula operand;
    if (m_negated)
    {
      apply(operand, negate_variables(x.name(), m_quantitative, x.operand()));
      make_mu(result, x.name(), x.assignments(), operand);
    }
    else
    {
      apply(operand, x.operand());
      make_nu(result, x.name(), x.assignments(), operand);
    }
  }
 
  template <class T>
  void apply(T& result, const delay& x)
  {
    if (m_negated)
    {
      result=yaled();
    }
    else
    {
      result=x;
    }
  }
 
  template <class T>
  void apply(T& result, const delay_timed& x)
  {
    if (m_negated)
    {
      make_yaled_timed(result, x.time_stamp());
    }
    else
    {
      result=x;
    }
  }
 
  template <class T>
  void apply(T& result, const yaled& x)
  {
    if (m_negated)
    {
      result=delay();
    }
    else
    {
      result=x;
    }
  }
 
  template <class T>
  void apply(T& result,  const yaled_timed& x)
  {
    if (m_negated)
    {
      make_delay_timed(result, x.time_stamp());
    }
    else
    {
      result=x;
    }
  }
};
 
template <typename T>
bool is_normalized(const T& x)
{
  is_normalized_traverser f;
  f.apply(x);
  return f.result;
}
 
template <typename T>
void normalize(T& x, bool quantitative = false, bool negated = false, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr)
{
  normalize_builder f(quantitative, negated);
  f.update(x);
}
 
template <typename T>
T normalize(const T& x, bool quantitative = false, bool negated = false, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr)
{
  T result;
  normalize_builder f(quantitative, negated);
  f.apply(result, x);
  return result;
}
 
} // namespace state_formulas
 
} // namespace mcrl2
 
#endif // MCRL2_MODAL_FORMULA_NORMALIZE_H