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/stategraph_influence.h 10 : /// \brief add your file description here. 11 : 12 : #ifndef MCRL2_PBES_DETAIL_STATEGRAPH_INFLUENCE_H 13 : #define MCRL2_PBES_DETAIL_STATEGRAPH_INFLUENCE_H 14 : 15 : #include "mcrl2/pbes/detail/pfnf_pbes.h" 16 : #include "mcrl2/pbes/detail/stategraph_pbes.h" 17 : #include <iomanip> 18 : 19 : namespace mcrl2 { 20 : 21 : namespace pbes_system { 22 : 23 : namespace detail { 24 : 25 : /// \brief Algorithm class for the stategraph algorithm 26 : class stategraph_influence_graph_algorithm 27 : { 28 : public: 29 0 : explicit stategraph_influence_graph_algorithm(const stategraph_pbes& p) 30 0 : : m_pbes(p) 31 0 : {} 32 : 33 : // vertex of the influence graph 34 : struct influence_vertex 35 : { 36 : core::identifier_string X; 37 : data::variable v; 38 : 39 0 : std::string print() const 40 : { 41 0 : std::ostringstream out; 42 0 : out << X << ", " << v; 43 0 : return out.str(); 44 0 : } 45 : 46 0 : influence_vertex(const core::identifier_string& X_, const data::variable& v_) 47 0 : : X(X_), v(v_) 48 0 : {} 49 : }; 50 : 51 : // influence_edge of the influence graph 52 : struct influence_edge 53 : { 54 : const influence_vertex* source; 55 : const influence_vertex* target; 56 : 57 0 : std::string print() const 58 : { 59 0 : std::ostringstream out; 60 0 : out << core::pp(source->X) << " ---> " << core::pp(target->X); 61 0 : return out.str(); 62 0 : } 63 : 64 0 : influence_edge(const influence_vertex* source_, const influence_vertex* target_) 65 0 : : source(source_), target(target_) 66 0 : {} 67 : }; 68 : 69 0 : void print_influence_graph() const 70 : { 71 0 : mCRL2log(log::verbose) << "--- influence graph ---\n"; 72 0 : for (const auto& v: m_influence_vertices) 73 : { 74 0 : mCRL2log(log::verbose) << v.print() << std::endl; 75 : } 76 0 : for (const auto& e: m_influence_edges) 77 : { 78 0 : mCRL2log(log::verbose) << e.print() << std::endl; 79 : } 80 0 : } 81 : 82 : protected: 83 : // the pbes that is considered 84 : const stategraph_pbes& m_pbes; 85 : 86 : // vertices of the influence graph 87 : std::vector<influence_vertex> m_influence_vertices; 88 : 89 : // edges of the influence graph 90 : std::vector<influence_edge> m_influence_edges; 91 : 92 : // very inefficient 93 0 : std::vector<influence_vertex>::const_iterator find_vertex(const core::identifier_string& X, const data::variable& v) const 94 : { 95 0 : for (auto i = m_influence_vertices.begin(); i != m_influence_vertices.end(); ++i) 96 : { 97 0 : if (i->X == X && i->v == v) 98 : { 99 0 : return i; 100 : } 101 : } 102 0 : return m_influence_vertices.end(); 103 : } 104 : 105 0 : void compute_influence_graph() 106 : { 107 : using utilities::detail::contains; 108 : 109 : // compute the vertices 110 0 : auto const& equations = m_pbes.equations(); 111 0 : for (const stategraph_equation& equation: equations) 112 : { 113 0 : auto const& X = equation.variable().name(); 114 0 : auto const& Xparams = equation.parameters(); 115 0 : for (const auto & Xparam : Xparams) 116 : { 117 0 : m_influence_vertices.emplace_back(X, Xparam); 118 : } 119 : } 120 : 121 : // compute the edges 122 0 : for (const stategraph_equation& equation: equations) 123 : { 124 0 : const std::vector<data::variable>& d_X = equation.parameters(); 125 0 : const core::identifier_string Xname = equation.variable().name(); 126 0 : const std::vector<predicate_variable>& predvars = equation.predicate_variables(); 127 0 : for (const auto & predvar : predvars) 128 : { 129 0 : auto const& Y = predvar.variable(); 130 0 : std::vector<data::data_expression> Yparameters(Y.parameters().begin(), Y.parameters().end()); 131 0 : stategraph_equation eqn = *find_equation(m_pbes, Y.name()); 132 0 : const std::vector<data::variable>& d_Y = eqn.parameters(); 133 0 : for (std::size_t p = 0; p < Yparameters.size(); p++) 134 : { 135 0 : std::set<data::variable> freevars = data::find_free_variables(Yparameters[p]); 136 0 : for (const data::variable& v: d_X) 137 : { 138 0 : if (contains(freevars, v)) 139 : { 140 0 : auto source = find_vertex(Xname, v); 141 0 : auto target = find_vertex(Y.name(), d_Y[p]); 142 0 : influence_edge e(&(*source), &(*target)); 143 0 : m_influence_edges.push_back(e); 144 : } 145 : } 146 0 : } 147 0 : } 148 0 : } 149 0 : } 150 : 151 : public: 152 : 153 0 : void run() 154 : { 155 0 : compute_influence_graph(); 156 0 : print_influence_graph(); 157 0 : } 158 : }; 159 : 160 : } // namespace detail 161 : 162 : } // namespace pbes_system 163 : 164 : } // namespace mcrl2 165 : 166 : #endif // MCRL2_PBES_DETAIL_STATEGRAPH_INFLUENCE_H