LCOV - code coverage report
Current view: top level - modal_formula/include/mcrl2/modal_formula - negate_variables.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 10 10 100.0 %
Date: 2020-04-01 00:44:46 Functions: 4 4 100.0 %
Legend: Lines: hit not hit

          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/modal_formula/negate_variables.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_MODAL_FORMULA_NEGATE_VARIABLES_H
      13             : #define MCRL2_MODAL_FORMULA_NEGATE_VARIABLES_H
      14             : 
      15             : #include "mcrl2/modal_formula/builder.h"
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : 
      20             : namespace state_formulas
      21             : {
      22             : 
      23             : namespace detail
      24             : {
      25             : 
      26             : /// Visitor that negates propositional variable instantiations with a given name.
      27             : template <typename Derived>
      28          23 : struct state_variable_negator: public state_formulas::state_formula_builder<Derived>
      29             : {
      30             :   typedef state_formulas::state_formula_builder<Derived> super;
      31             :   using super::apply;
      32             : 
      33             :   core::identifier_string m_name;
      34             : 
      35          23 :   state_variable_negator(const core::identifier_string& name)
      36          23 :     : m_name(name)
      37          23 :   {}
      38             : 
      39             :   /// \brief Visit variable node.
      40             :   /// \param x A term.
      41             :   /// \return The result of visiting the node.
      42          31 :   state_formula apply(const variable& x)
      43             :   {
      44          31 :     if (x.name() == m_name)
      45             :     {
      46          21 :       return state_formulas::not_(x);
      47             :     }
      48          10 :     return x;
      49             :   }
      50             : };
      51             : 
      52             : } // namespace detail
      53             : 
      54             : inline
      55             : /// \brief Negates variable instantiations in a state formula with a given name.
      56             : /// \param name The name of the variables that should be negated.
      57             : /// \param x The state formula. 
      58          23 : state_formula negate_variables(const core::identifier_string& name, const state_formula& x)
      59             : {
      60          23 :   return core::make_apply_builder_arg1<detail::state_variable_negator>(name).apply(x);
      61             : }
      62             : 
      63             : } // namespace state_formulas
      64             : 
      65             : } // namespace mcrl2
      66             : 
      67             : #endif // MCRL2_MODAL_FORMULA_NEGATE_VARIABLES_H

Generated by: LCOV version 1.13