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/pbes/detail/lps2pbes_utility.h 10 : /// \brief add your file description here. 11 : 12 : #ifndef MCRL2_PBES_DETAIL_LPS2PBES_UTILITY_H 13 : #define MCRL2_PBES_DETAIL_LPS2PBES_UTILITY_H 14 : 15 : #include "mcrl2/data/substitutions/mutable_map_substitution.h" 16 : #include "mcrl2/modal_formula/state_formula.h" 17 : #include "mcrl2/pbes/pbes.h" 18 : 19 : namespace mcrl2 { 20 : 21 : namespace pbes_system { 22 : 23 : /// \cond INTERNAL_DOCS 24 : // 25 : /// \brief Concatenates two sequences of PBES equations 26 : /// \param p A sequence of PBES equations 27 : /// \param q A sequence of PBES equations 28 : /// \return The concatenation result 29 : inline 30 122 : std::vector<pbes_equation> operator+(const std::vector<pbes_equation>& p, const std::vector<pbes_equation>& q) 31 : { 32 122 : std::vector<pbes_equation> result(p); 33 122 : result.insert(result.end(), q.begin(), q.end()); 34 122 : return result; 35 0 : } 36 : /// \endcond 37 : 38 : /// \cond INTERNAL_DOCS 39 : // 40 : /// \brief Appends a PBES equation to a sequence of PBES equations 41 : /// \param p A sequence of PBES equations 42 : /// \param e A PBES equation 43 : /// \return The append result 44 : inline 45 : std::vector<pbes_equation> operator+(const std::vector<pbes_equation>& p, const pbes_equation& e) 46 : { 47 : std::vector<pbes_equation> result(p); 48 : result.push_back(e); 49 : return result; 50 : } 51 : /// \endcond 52 : 53 : namespace detail { 54 : 55 : inline 56 200 : data::variable_list lhs_variables(const data::assignment_list& l) 57 : { 58 200 : data::variable_list result; 59 209 : for (const data::assignment& a: l) 60 : { 61 9 : result.push_front(a.lhs()); 62 : } 63 400 : return atermpp::reverse(result); 64 200 : } 65 : 66 : inline 67 291 : data::data_expression_list rhs_expressions(const data::assignment_list& l) 68 : { 69 291 : data::data_expression_list result; 70 300 : for (const data::assignment& a: l) 71 : { 72 9 : result.push_front(a.rhs()); 73 : } 74 582 : return atermpp::reverse(result); 75 291 : } 76 : 77 : inline 78 141 : const core::identifier_string& mu_name(const state_formulas::state_formula& f) 79 : { 80 141 : if (state_formulas::is_mu(f)) 81 : { 82 21 : const auto& g = atermpp::down_cast<state_formulas::mu>(f); 83 21 : return g.name(); 84 : } 85 : else 86 : { 87 120 : const auto& g = atermpp::down_cast<state_formulas::nu>(f); 88 120 : return g.name(); 89 : } 90 : } 91 : 92 : /// \brief Returns the variables corresponding to ass(f) 93 : /// \param f A modal formula 94 : /// \return The variables corresponding to ass(f) 95 : inline 96 200 : data::variable_list mu_variables(const state_formulas::state_formula& f) 97 : { 98 200 : assert(state_formulas::is_mu(f) || state_formulas::is_nu(f)); 99 200 : if (state_formulas::is_mu(f)) 100 : { 101 52 : const auto& g = atermpp::down_cast<state_formulas::mu>(f); 102 52 : return lhs_variables(g.assignments()); 103 : } 104 : else 105 : { 106 148 : const auto& g = atermpp::down_cast<state_formulas::nu>(f); 107 148 : return lhs_variables(g.assignments()); 108 : } 109 : } 110 : 111 : /// \brief Returns the data expressions corresponding to ass(f) 112 : /// \param f A modal formula 113 : /// \return The data expressions corresponding to ass(f) 114 : inline 115 291 : data::data_expression_list mu_expressions(const state_formulas::state_formula& f) 116 : { 117 291 : assert(state_formulas::is_mu(f) || state_formulas::is_nu(f)); 118 291 : if (state_formulas::is_mu(f)) 119 : { 120 79 : const auto& g = atermpp::down_cast<state_formulas::mu>(f); 121 79 : return rhs_expressions(g.assignments()); 122 : } 123 : else 124 : { 125 212 : const auto& g = atermpp::down_cast<state_formulas::nu>(f); 126 212 : return rhs_expressions(g.assignments()); 127 : } 128 : } 129 : 130 : inline 131 : std::string myprint(const std::vector<pbes_equation>& v) 132 : { 133 : std::ostringstream out; 134 : out << "["; 135 : for (const pbes_equation& eqn: v) 136 : { 137 : out << "\n " << pbes_system::pp(eqn.symbol()) << " " << pbes_system::pp(eqn.variable()) << " = " << pbes_system::pp(eqn.formula()); 138 : } 139 : out << "\n]"; 140 : return out.str(); 141 : } 142 : 143 : /// \brief Generates a substitution that assigns fresh variables to the given sequence of variables. 144 : /// The identifier generator is used to assign names to the fresh variables. 145 : /// Caveat: the implementation is very inefficient. 146 : /// \param update_context If true, then generated names are added to the context 147 : inline 148 10 : data::mutable_map_substitution<> make_fresh_variable_substitution(const data::variable_list& variables, data::set_identifier_generator& id_generator, bool add_to_context = true) 149 : { 150 10 : data::mutable_map_substitution<> result; 151 20 : for (const data::variable& v: variables) 152 : { 153 10 : core::identifier_string name = id_generator(std::string(v.name())); 154 10 : result[v] = data::variable(name, v.sort()); 155 10 : if (!add_to_context) 156 : { 157 9 : id_generator.remove_identifier(name); 158 : } 159 10 : } 160 10 : return result; 161 0 : } 162 : 163 : } // namespace detail 164 : 165 : } // namespace pbes_system 166 : 167 : } // namespace mcrl2 168 : 169 : #endif // MCRL2_PBES_DETAIL_LPS2PBES_UTILITY_H