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 complement.h 10 : /// \brief The complement function for pbes expressions. 11 : // 12 : // Comp ( val(b) ) = val (! b) 13 : // 14 : // Comp ( X(d) ) = "ABORT, should not happen" 15 : // 16 : // Comp ( PbesAnd (f, g) ) = PbesOr (Comp (f), Comp (g) ) 17 : // 18 : // Comp ( PbesOr (f, g) ) = PbesAnd (Comp (f), Comp (g) ) 19 : // 20 : // Comp (PbesForAll (f) ) = PbesExists (Comp (f) ) 21 : // 22 : // Comp (PbesExists (f) ) = PbesForall (Comp (f) ) 23 : // 24 : // Comp (Comp (f) ) = f 25 : 26 : #ifndef MCRL2_PBES_COMPLEMENT_H 27 : #define MCRL2_PBES_COMPLEMENT_H 28 : 29 : #include "mcrl2/data/consistency.h" 30 : #include "mcrl2/pbes/builder.h" 31 : 32 : namespace mcrl2 33 : { 34 : 35 : namespace pbes_system 36 : { 37 : 38 : /// \cond INTERNAL_DOCS 39 : // \brief Visitor that pushes a negation in a PBES expression as far as possible 40 : // inwards towards a data expression. 41 : template <typename Derived> 42 : struct complement_builder: public pbes_expression_builder<Derived> 43 : { 44 : typedef pbes_expression_builder<Derived> super; 45 : using super::enter; 46 : using super::leave; 47 : using super::update; 48 : using super::apply; 49 : 50 : template <class T> 51 8 : void apply(T& result, const data::data_expression& x) 52 : { 53 8 : result = data::not_(x); 54 8 : } 55 : 56 : template <class T> 57 4 : void apply(T& result, const and_& x) 58 : { 59 4 : pbes_expression left; 60 4 : static_cast<Derived&>(*this).apply(left, x.left()); 61 4 : pbes_expression right; 62 4 : static_cast<Derived&>(*this).apply(right, x.right()); 63 4 : optimized_or(result, left, right); 64 4 : } 65 : 66 : template <class T> 67 2 : void apply(T& result, const or_& x) 68 : { 69 2 : pbes_expression left; 70 2 : static_cast<Derived&>(*this).apply(left, x.left()); 71 2 : pbes_expression right; 72 2 : static_cast<Derived&>(*this).apply(right, x.right()); 73 2 : optimized_and(result, left, right); 74 2 : } 75 : 76 : template <class T> 77 0 : void apply(T& /* result */, const propositional_variable_instantiation& x) 78 : { 79 0 : throw mcrl2::runtime_error(std::string("complement_builder error: unexpected propositional variable encountered ") + mcrl2::pbes_system::pp(x)); 80 : } 81 : }; 82 : /// \endcond 83 : 84 : /// \brief Returns the complement of a pbes expression 85 : /// \param x A PBES expression 86 : /// \return The expression obtained by pushing the negations in the pbes 87 : /// expression as far as possible inwards towards a data expression. 88 : inline 89 2 : pbes_expression complement(const pbes_expression& x) 90 : { 91 2 : pbes_expression result; 92 2 : core::make_apply_builder<complement_builder>().apply(result, x); 93 2 : return result; 94 0 : } 95 : 96 : } // namespace pbes_system 97 : 98 : } // namespace mcrl2 99 : 100 : #endif // MCRL2_PBES_COMPLEMENT_H