Line data Source code
1 : // Author(s): Aad Mathijssen 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/translate_regular_formulas.h 10 : /// \brief Translate regular formulas in terms of state and action formulas. 11 : 12 : #ifndef MCRL2_MODAL_FORMULA_TRANSLATE_REGULAR_FORMULAS_H 13 : #define MCRL2_MODAL_FORMULA_TRANSLATE_REGULAR_FORMULAS_H 14 : 15 : #include "mcrl2/modal_formula/state_formula.h" 16 : 17 : namespace mcrl2 { 18 : 19 : namespace regular_formulas { 20 : 21 : namespace detail { 22 : 23 : /** \brief Translate regular formulas in terms of state and action formulas. 24 : * \param[in] state_frm An aterm representation of a state formula according 25 : * to the internal aterm structure after the data implementation 26 : * phase. 27 : * \return state_frm in which all regular formulas are translated in 28 : * terms of state and action formulas. 29 : **/ 30 : mcrl2::state_formulas::state_formula translate_reg_frms(const mcrl2::state_formulas::state_formula& state_frm); 31 : 32 : } // namespace detail 33 : 34 : } // namespace regular_formulas 35 : 36 : namespace state_formulas { 37 : 38 : /// \brief Translates regular formulas appearing in f into action formulas. 39 : /// \param x A state formula 40 : inline 41 156 : state_formula translate_regular_formulas(const state_formula& x) 42 : { 43 156 : atermpp::aterm_appl result = regular_formulas::detail::translate_reg_frms(x); 44 156 : if (result == atermpp::aterm_appl()) 45 : { 46 0 : throw mcrl2::runtime_error("regular formula translation error"); 47 : } 48 312 : return state_formula(result); 49 156 : } 50 : 51 : } // namespace state_formulas 52 : 53 : } // namespace mcrl2 54 : 55 : #endif // MCRL2_MODAL_FORMULA_TRANSLATE_REGULAR_FORMULAS_H