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/is_timed.h 10 : /// \brief add your file description here. 11 : 12 : #ifndef MCRL2_MODAL_FORMULA_IS_TIMED_H 13 : #define MCRL2_MODAL_FORMULA_IS_TIMED_H 14 : 15 : #include "mcrl2/modal_formula/traverser.h" 16 : 17 : namespace mcrl2 { 18 : 19 : namespace state_formulas { 20 : 21 : namespace detail { 22 : 23 : /// \brief Function that determines if a state formula is time dependent 24 : // \brief Visitor for checking if a state formula is timed. 25 : struct is_timed_traverser: public state_formula_traverser<is_timed_traverser> 26 : { 27 : typedef state_formula_traverser<is_timed_traverser> super; 28 : using super::enter; 29 : using super::leave; 30 : using super::apply; 31 : 32 : bool result; 33 : 34 143 : is_timed_traverser() 35 143 : : result(false) 36 143 : {} 37 : 38 4 : void enter(const delay_timed& /* x */) 39 : { 40 4 : result = true; 41 4 : } 42 : 43 4 : void enter(const yaled_timed& /* x */) 44 : { 45 4 : result = true; 46 4 : } 47 : 48 : void enter(const action_formulas::at& /* x */) 49 : { 50 : result = true; 51 : } 52 : }; 53 : 54 : } // namespace detail 55 : 56 : /// \brief Checks if a state formula is timed 57 : /// \param x A state formula 58 : /// \return True if a state formula is timed 59 : inline 60 143 : bool is_timed(const state_formula& x) 61 : { 62 143 : detail::is_timed_traverser f; 63 143 : f.apply(x); 64 143 : return f.result; 65 : } 66 : 67 : } // namespace state_formulas 68 : 69 : } // namespace mcrl2 70 : 71 : #endif // MCRL2_MODAL_FORMULA_IS_TIMED_H