LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes/detail - stategraph_influence.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 0 63 0.0 %
Date: 2024-03-08 02:52:28 Functions: 0 9 0.0 %
Legend: Lines: hit not hit

          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

Generated by: LCOV version 1.14