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/abstract.h 10 : /// \brief The PBES abstract algorithm. 11 : 12 : #ifndef MCRL2_PBES_ABSTRACT_H 13 : #define MCRL2_PBES_ABSTRACT_H 14 : 15 : #include "mcrl2/data/consistency.h" 16 : #include "mcrl2/pbes/builder.h" 17 : #include "mcrl2/pbes/detail/pbes_parameter_map.h" 18 : 19 : namespace mcrl2 20 : { 21 : 22 : namespace pbes_system 23 : { 24 : 25 : namespace detail 26 : { 27 : 28 : /// \brief Visitor that implements the pbes-abstract algorithm. 29 : struct pbes_abstract_builder: public pbes_expression_builder<pbes_abstract_builder> 30 : { 31 : typedef pbes_expression_builder<pbes_abstract_builder> super; 32 : using super::apply; 33 : 34 : std::vector<data::variable_list> m_quantifier_stack; 35 : const std::vector<data::variable> m_selected_variables; 36 : const data::data_expression m_value; 37 : 38 3 : pbes_abstract_builder(const std::vector<data::variable>& selected_variables, bool value_true) 39 3 : : m_selected_variables(selected_variables), 40 6 : m_value(value_true ? data::true_() : data::false_()) 41 3 : {} 42 : 43 : /// \brief Returns true if the m_quantifier_stack contains a given data variable 44 2 : bool is_bound(const data::variable& v) const 45 : { 46 2 : for (const data::variable_list& variables: m_quantifier_stack) 47 : { 48 1 : for (const data::variable& w: variables) 49 : { 50 1 : if (w == v) 51 : { 52 1 : return true; 53 : } 54 : } 55 : } 56 1 : return false; 57 : } 58 : 59 : /// \brief Adds a sequence of variables to the quantifier stack. 60 1 : void push_variables(const data::variable_list& variables) 61 : { 62 1 : m_quantifier_stack.push_back(variables); 63 1 : } 64 : 65 : /// \brief Removes the last added sequence of variables from the quantifier stack. 66 1 : void pop_variables() 67 : { 68 1 : m_quantifier_stack.pop_back(); 69 1 : } 70 : 71 : /// \brief Visit data_expression node 72 : template <class T> 73 3 : void apply(T& result, const data::data_expression& d) 74 : { 75 3 : std::set<data::variable> FV = data::find_free_variables(d); 76 5 : for (const data::variable& v: FV) 77 : { 78 3 : if (std::find(m_selected_variables.begin(), m_selected_variables.end(), v) == m_selected_variables.end()) 79 : { 80 1 : continue; 81 : } 82 2 : if (!is_bound(v)) 83 : { 84 : //std::clog << "Reducing data expression " << data::pp(d) << " to " << data::pp(m_value) << "." << std::endl; 85 1 : result = m_value; 86 1 : return; 87 : } 88 : } 89 2 : result = d; 90 3 : } 91 : 92 : /// \brief Visit forall node 93 : template <class T> 94 0 : void apply(T& result, const forall& x) 95 : { 96 0 : push_variables(x.variables()); 97 0 : pbes_expression new_expression; 98 0 : apply(new_expression, x.body()); 99 0 : pop_variables(); 100 0 : result = make_forall_(x.variables(), new_expression); 101 0 : } 102 : 103 : /// \brief Visit exists node 104 : template <class T> 105 1 : void apply(T& result, const exists& x) 106 : { 107 1 : push_variables(x.variables()); 108 1 : pbes_expression new_expression; 109 1 : apply(new_expression, x.body()); 110 1 : pop_variables(); 111 1 : result = make_exists_(x.variables(), new_expression); 112 1 : } 113 : }; 114 : 115 : } // namespace detail 116 : 117 : 118 : /// \brief Algorithm class for the abstract algorithm 119 : class pbes_abstract_algorithm 120 : { 121 : public: 122 : /// \brief Runs the algorithm. 123 : /// \param p A PBES. 124 : /// \param parameter_map A map containing the parameters that should be expanded by the algorithm. 125 : /// \param value_true An indication whether the abstraction is towards true or towards false. 126 3 : void run(pbes& p, 127 : const detail::pbes_parameter_map& parameter_map, 128 : bool value_true 129 : ) 130 : { 131 8 : for (pbes_equation& eqn: p.equations()) 132 : { 133 5 : auto j = parameter_map.find(eqn.variable().name()); 134 5 : if (j != parameter_map.end()) 135 : { 136 3 : detail::pbes_abstract_builder builder(j->second, value_true); 137 3 : pbes_expression result; 138 3 : builder.apply(result, eqn.formula()); 139 3 : eqn.formula() = result; 140 3 : } 141 : } 142 3 : } 143 : }; 144 : 145 : } // namespace pbes_system 146 : 147 : } // namespace mcrl2 148 : 149 : #endif // MCRL2_PBES_ABSTRACT_H