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/count_fixpoints.h 10 : /// \brief add your file description here. 11 : 12 : #ifndef MCRL2_MODAL_FORMULA_COUNT_FIXPOINTS_H 13 : #define MCRL2_MODAL_FORMULA_COUNT_FIXPOINTS_H 14 : 15 : #include "mcrl2/modal_formula/traverser.h" 16 : 17 : namespace mcrl2 { 18 : 19 : namespace state_formulas { 20 : 21 : /// \cond INTERNAL_DOCS 22 : // 23 : /// \brief Function that counts the number of fixpoints in a state formula 24 : namespace detail { 25 : 26 : struct count_fixpoints_traverser: public state_formula_traverser<count_fixpoints_traverser> 27 : { 28 : typedef state_formula_traverser<count_fixpoints_traverser> super; 29 : using super::enter; 30 : using super::leave; 31 : using super::apply; 32 : 33 : std::size_t result; 34 : 35 6 : count_fixpoints_traverser() 36 6 : : result(0) 37 6 : {} 38 : 39 14 : void enter(const mu& /* x */) 40 : { 41 14 : result++; 42 14 : } 43 : 44 13 : void enter(const nu& /* x */) 45 : { 46 13 : result++; 47 13 : } 48 : }; 49 : 50 : } // namespace detail 51 : /// \endcond 52 : 53 : /// \brief Counts the number of fixpoints in a state formula 54 : /// \param x A state formula 55 : /// \return The number of fixpoints in a state formula 56 : inline 57 6 : std::size_t count_fixpoints(const state_formula& x) 58 : { 59 6 : detail::count_fixpoints_traverser f; 60 6 : f.apply(x); 61 6 : return f.result; 62 : } 63 : 64 : } // namespace state_formulas 65 : 66 : } // namespace mcrl2 67 : 68 : #endif // MCRL2_MODAL_FORMULA_COUNT_FIXPOINTS_H