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_PBES_NORMALIZE_H
#define MCRL2_PBES_NORMALIZE_H
 
#include "mcrl2/data/consistency.h"
#include "mcrl2/pbes/builder.h"
#include "mcrl2/pbes/traverser.h"
 
namespace mcrl2
{
 
namespace pbes_system
{
 
// \brief Visitor for checking if a pbes expression is normalized.
struct is_normalized_traverser: public pbes_expression_traverser<is_normalized_traverser>
{
  typedef pbes_expression_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 imp& /* x */)
  {
    result = false;
  }
};
 
// \brief Visitor for checking if a pbes expression is normalized.
struct normalize_builder: public pbes_expression_builder<normalize_builder>
{
  typedef pbes_expression_builder<normalize_builder> super;
  using super::apply;
 
  bool negated;
 
  normalize_builder()
    : negated(false)
  {}
 
  template <class T>
  void apply(T& result, const data::data_expression& x)
  {
    result = negated ? data::not_(x) : x;
  }
 
  template <class T>
  void apply(T& result, const not_& x)
  {
    negated = !negated;
    super::apply(result, x.operand());
    negated = !negated;
  }
 
  template <class T>
  void apply(T& result, const and_& x)
  {
    pbes_expression left;
    super::apply(left, x.left());
    pbes_expression right;
    super::apply(right, x.right());
    if (negated)
    {
      make_or_(result, left, right);
    }
    else
    {
      make_and_(result, left, right);
    }
  }
 
  template <class T>
  void apply(T& result, const or_& x)
  {
    pbes_expression left;
    super::apply(left, x.left());
    pbes_expression right;
    super::apply(right, x.right());
    if (negated)
    {
      make_and_(result, left, right);
    }
    else
    {
      make_or_(result, left, right);
    }
  }
 
  template <class T>
  void apply(T& result, const imp& x)
  {
    negated = !negated;
    pbes_expression left;
    super::apply(left, x.left());
    negated = !negated;
    pbes_expression right;
    super::apply(right, x.right());
    if (negated)
    {
      make_and_(result, left, right);
    }
    else
    {
      make_or_(result, left, right);
    }
  }
 
  template <class T>
  void apply(T& result, const forall& x)
  {
    pbes_expression body;
    super::apply(body, x.body());
    result = negated ? make_exists_(x.variables(), body) : make_forall_(x.variables(), body);
  }
 
  template <class T>
  void apply(T& result, const exists& x)
  {
    pbes_expression body;
    super::apply(body, x.body());
    result = negated ? make_forall_(x.variables(), body) : make_exists_(x.variables(), body);
  }
 
  template <class T>
  void apply(T& result, const propositional_variable_instantiation& x)
  {
    if (negated)
    {
      throw mcrl2::runtime_error(std::string("normalize error: illegal argument ") + pp(x));
    }
    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,
               typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
              )
{
  normalize_builder f;
  f.update(x);
}
 
template <typename T>
T normalize(const T& x,
            typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
           )
{
  T result;
  normalize_builder f;
  f.apply(result, x);
  return result;
}
 
} // namespace pbes_system
 
} // namespace mcrl2
 
#endif // MCRL2_PBES_NORMALIZE_H