negate_variables.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_NEGATE_VARIABLES_H
#define MCRL2_MODAL_FORMULA_NEGATE_VARIABLES_H
 
#include "mcrl2/modal_formula/builder.h"
 
namespace mcrl2
{
 
namespace state_formulas
{
 
namespace detail
{
 
template <typename Derived>
struct state_variable_negator: public state_formulas::state_formula_builder<Derived>
{
  typedef state_formulas::state_formula_builder<Derived> super;
  using super::apply;
 
  core::identifier_string m_name;
  bool m_quantitative;
 
  state_variable_negator(const core::identifier_string& name, bool quantitative)
    : m_name(name),
      m_quantitative(quantitative)
  {}
 
  template <class T>
  void apply(T& result, const variable& x)
  {
    if (x.name() == m_name)
    {
      if (m_quantitative)
      {
        state_formulas::make_minus(result, x);
      }
      else
      {
        state_formulas::make_not_(result, x);
      }
      return;
    }
    result = x;
  }
};
 
} // namespace detail
 
inline
state_formula negate_variables(const core::identifier_string& name, bool quantitative, const state_formula& x)
{
  state_formula result;
  core::make_apply_builder_arg2<detail::state_variable_negator>(name, quantitative).apply(result, x);
  return result;
}
 
} // namespace state_formulas
 
} // namespace mcrl2
 
#endif // MCRL2_MODAL_FORMULA_NEGATE_VARIABLES_H